函数式编程

#00 | 初识Lambda演算
#01 | Lambda演算中的自然数
#02 | Lambda演算中的循环与递归

缘起

在学习面向对象编程的过程中，我曾第一次接触了“把函数作为一个参数传入另一个函数”这种最初看来很不可理喻的操作。后来，在C语言中遇到了“函数指针”，在C#中也遇到了“委托”和lambda表达式等内容。而促使我接触函数式编程的，一个是微软俱乐部的一道“一元函数”题目和它交给我的二面任务：初步学习F#。

对于那道题目，将会是此栏目后文中讨论的内容，不过先抛开他不管，先来聊聊什么是“Lambda演算”。

Lambda演算 #00

函数式编程——要源于1930年代的数学家Alonzo Church提出的Lambda演算。
引用一段知乎同学的话：

在介绍 $\lambda$ 演算之前，我们需要放空一下我们的大脑，忘掉C语言，忘掉冯·诺伊曼机，忘掉图灵机，甚至要忘掉0和1，加和减。我们来到一个只有符号的世界。
在这个新的世界里，只需要几条简单的定义和规则，便可以构造出与图灵机完全等价的计算模型，即它是图灵完全（Turing Complete）的。
和图灵机一样，这个计算模型可以解决任何一个可以机械计算的问题；与图灵机倾向于硬件实现不同，它更倾向于逻辑的推理。它就是 $\lambda$ 演算（Lambda演算）。

Lambda表达式

大部分人，包括我，初识编程的时候接触的语言几乎都是命令式语言，通过一步一步告诉计算机要做什么、该做什么，它与计算机的结构紧密相关，通过变量、控制流和函数等对于计算机硬件处理过程的抽象进而实现程序的编写。

到后来，接触了各种语言的“匿名函数”，也被叫做lambda表达式，他们有各种样貌：

f = lambda x: x + 1

Func<int, int> f = x => x + 1;

虽说时间顺序的确是反过来的，毕竟这些lambda表达式都是 $\lambda$ 演算出现很久之后的现代产物了，但从这里入手，也许会更好的理解一些。不过对于数学家而言，这样的写法依然可以说“繁琐”，他们利用 $\lambda$ 这一符号简化和表示这种函数的抽象。

如果用不太规范的形式表示上方的函数，大体是这样的：

$\lambda x. x+1$

Lambda项（Lambda Term）

从这里开始，便会涉及到一些较为难以理解的定义了，不过多看几遍，稍作停顿还是可以理解的。

引用一段简书的话：

哲学上一个常识，内涵越小外延越大。我们搞了那么多的假定，往往就给自己做了很大的束缚。数学家不喜欢这么玩，所以构建这个 $\lambda$ 演算的时候，更倾向于用尽可能少的原生性规则来进行限定。

于是，所有合法的Lambda项都可以用以下三条规则，或者说“语法”给出：

Variable：变量，可以是一个字符或者字符串，用来表示一个变量，它可以是数字或逻辑值等等。如果x是一个变量，那么它就是一个合法的 $\lambda$ 项。
Abstraction：如果 $t$ 是一个合法的 $\lambda$ 项，且x是一个变量，则 $(\lambda x. t)$ 是一个合法的 $\lambda$ 项。这个形式被称作抽象。
Application：如果 $t$ 和 $s$ 都是合法的 $\lambda$ 项，那么 $(t \ s)$ 也是一个合法的 $\lambda$ 项。它的意义相当于一个： $t(s)$ ，其结果就是对函数求值。这个形式被称为应用。

其实如上的规则让我们定义了变量、函数和函数调用，它们在Lambda演算中的术语分别是变量、抽象和应用。

在此基础上，有一句话私以为可以很好的描述Lambda项：
全体Lambda项构成 $\Lambda$ 空间，而Lambda项是 $\Lambda$ 空间到 $\Lambda$ 空间的函数。

这颇有中学时候语文老师所说的“循环定义”的意味， $\Lambda$ 空间用Lambda项定义，而Lambda项又要借助 $\Lambda$ 空间所定义。但细细想之，这并不矛盾，可以说是将函数这种对应关系本身作为一个对象纳入了考虑的范畴，也就是所谓的函数为第一类对象的原则。

不过，如果仅有如上几条设置，那么这玩意用起来可是着实的难受——因为括号不是一般的多，用我们目前的设定简单的实现一下平方和函数：

$(\lambda y.((\lambda x.(x * x + y * y))5)2) = 29$

当然这种写法并不算规范的写法，因为这里的+和*——甚至数字5和2——我们都没有证明其意义是什么。但已经可以很明显地看出这个表达的过程中括号实属很多，更别说定义了运算和数字之后将他们套进去之后、或者一些更复杂的Lambda项会带有多少括号了。所以，为了使它更加简洁，还有一些情况下是可以省略括号的：

Lambda项最外层的括号可以省略： $(t \ s)$ 等同于 $t \ s$
应用是左结合的：应用是从左往右依次进行“函数调用”的，这种情况下 $t \ s \ r$ 等同于 $((t \ s) \ r)$
如果没有括号约束，抽象是尽量向右扩展的：比如 $\lambda x. t \ s$ 与 $\lambda x.(t \ s)$ 等价，而不是 $(\lambda x. t) \ s$

自此，Lambda项的基本定义可以说告一段落了。但我相信读者还是会有很多的疑问，诸如如何定义运算等等，这些我们稍后再看，现在，让我们稍微休息一下大脑，看一个叫做“柯里化”的东西。

柯里化（Currying）

用一句话解释柯里化：“把接受多个参数的函数变换成接受一个单一参数（最初函数的第一个参数）的函数，并且返回接受余下的参数而且返回结果的新函数。”

初读可能觉得一头雾水，从直观上理解，它其实在说：对于一个接受很多参数的函数，每当你固定其中一个函数，你得到的将会是接受余下参数的一个全新的函数。

比如，对于二元函数 $x^2 + y^2$ ，当确定了 $y=2$ 后，那么将会得到 $x^2 + 4$ 这样一个一元函数。只要你明白了这一点，一件事情便会豁然开朗：任何“多元函数”都可以通过这样的过程由“一元函数”所构造出来。

在刚刚的Lambda项的定义中，抽象的操作可以理解为定义一元函数的过程，但同时，我们将函数作为第一类对象，在这里，函数和值已经被一视同仁，函数可以返回值，亦可以返回函数，于是，借助柯里化，表示一个多元函数便可以在Lambda项的世界里变得可行。

既然如此，我们可以采用一种简化的记法记录这些“多元函数”，还是以“加法”举例：

$\lambda \ x \ y. x + y = \lambda x. \lambda y. x + y$

布尔运算（Bool）

布尔值

好了，回过神来，知道了柯里化之后我们就要开始定义运算了。从最简单的布尔运算开始，我们采用Lambda演算的提出者：Alonzo Church的方案来构造，也就是所谓的邱奇布尔值（Church Booleans）。这个方案即：

$\begin{align*} T &= \lambda \ x \ y. x\\\\ F &= \lambda \ x \ y. y \end{align*}$

由柯里化的规则，其实展开来看它们的定义应该是：

$\begin{align*} T &= \lambda \ x. \lambda y. x\\\\ F &= \lambda \ x. \lambda y. y \end{align*}$

它表示 $T$ 是一个函数，接受第一个参数 $x$ 返回一个函数 $\lambda \ y. x$ ，这个被返回的函数接收另外一个输入 $y$ ，而不论这个输入 $y$ 是什么，它返回第一个输入的参数 $x$ 。同样， $F$ 忽略第一个参数，并且原模原样地返回第二个参数。

其实这里的 $\lambda y. y$ 被称作恒等函数，被记作 $I$ ，即SKI组合子演算中的 $I$ ，关于它的具体内容将在后文中详细讨论。

为了方便继续的讨论，我们可以用海象运算符 $:=$ 来为Lambda项命名，例如 $I := \lambda \ y. y$

而正如变量只是需要个名称，并不影响它内在的东西，这里的 $y$ 也只是一个“代号”，所以如同学习函数时，自变量的名称可以随意更换，我们一般会记 $I := \lambda x. x$ 。这其实在术语中被称为 $\alpha$ 变换，可以通过 $\alpha$ 变换为相同的Lambda项被称作 $\alpha$ 等价。它的作用显而易见：可以避免命名冲突。

同时这里前后出现的 $x$ 均表示同一个变量，所以这种变量也被称为约束变量（Bound Variable），与之对立，在 $\lambda y. x$ 这个Lambda项中，由于 $x$ 并没有被“约束”，因此被称为自由变量（Free Variable）。

布尔运算

插叙到此结束，回到刚刚的问题。我们的确用一种极其简单的方式定义出了某种意义上的“布尔值”，但毕竟脱离了运算的值一文不值。所以现在定义的“布尔值”并不算真正的“布尔值”，我们还需要用Lambda表达式定义布尔运算的算子：与、或、非，也就是 $and$ 、 $or$ 和 $not$ 三者。

先来构造 $and$ 算子，它接受两个“布尔值”，并且只有当他们都为 $T$ 时，它才为 $T$ ，所以基本形式应该是 $and := \lambda \ x \ y. (something)$ ，而关键就在于这个 $something$ 的构造。

考虑在python中构造一个会短路的 $And$ 函数：

And = lambda x,y: y if x is True else False

但问题来了，我们没有定义过类似于if-else这样的条件选择语句，那么该如何实现呢？但别忘了，我们定义的 $T$ 和 $F$ 天生就是选择语句：对于 $x \ a \ b$ ，如果 $x$ 是 $T$ ，则会选出 $a$ ，否则就会选出 $b$ 。

于是一个可以实现我们设想的算子便诞生了：

$and := \lambda \ x \ y. (x \ y \ F)$

验证一下：

$\begin{align*} and \ T \ F &= T \ F \ F = F \\\\ and \ T \ T &= T \ T \ F = T \\\\ and \ F \ F &= F \ F \ F = F \\\\ and \ F \ T &= F \ T \ F = F \end{align*}$

完美符合预期。
类似的，可以构造出 $Or$ 和 $Not$ 两个算子：

$\begin{align*} or &:= \lambda \ x \ y. x \ T \ y\\\\ not &:= \lambda \ x. x \ F \ T \end{align*}$

你甚至可以用他们从逻辑推导的公式 $x \ \text{xor} \ y = (\neg x \ \wedge \ y) \ \vee \ (x \ \wedge \ \neg y)$ 构造异或算子：

$xor := \lambda \ x \ y. Or \ And \ Not \ x \ y \ And \ x \ Not \ y$

这也许有些复杂了，或许我们可以以一种更加简化的方式，考虑异或运算的本质，相同则为假，不同则为真：

Xor = lambda x,y: not y if x is True else y

利用定义中 $T$ 和 $F$ 的选择能力，构造出如下的算子：

$xor := \lambda \ x \ y. x \ (Not \ y) \ y$

甚至更深一步，构造蕴含算子，走上数理逻辑和机器证明的道路……
然而，这仅仅定义了 $T$ 和 $F$ 两个“布尔值”。

未完待续… 下一篇：#01 | Lambda演算中的自然数

函数式编程 | #00 | 初识Lambda演算