函数式编程起源-Lambda演算(es2015描述)
前言
翻译自：Lambda Calculus with JavaScript
判定性问题和可计算性：
在形式化语言中，如何有效地接收并且验证一个命题的正确性？
简单来说，这是早在1928年提出的一个重要的数学问题：“判定性问题” （decision problem）。在数年之后的1936年，Alonzo Church 和 Alan Turing 证明了：为“判定性问题”设计一个通用算法这件事是不可能的。
与此同时，他们各自详细阐述了两个计算模型：Alonzo Church的Lambda演算（后文都称λ演算），Alan Turing的理论机器（之后被称作图灵机）。
冯.诺依曼结构实现了理论上的图灵机，并且用在了如今的电脑上。而Alonzo Church的计算模型，其实与图灵机一样强大，但由于一些历史原因，走了上了一条更加学术化，更不商业化的道路。
本文会借助javascript的语法（es2015）来介绍λ演算中的一些重要概念，展现λ演算对现代语言的影响和对未来编程的重要性。
Lambda演算
λ演算是一个为了表达和计算函数的形式化系统，有着自己的化简规则和语法。整个系统是基于表达式的（也叫λ项）。
一个表达式可以是一个变量（variable），一个抽象体（abstraction）或者一个应用（application）。
expression = variable || abstraction || application
下面是所有的表达式类型：
变量 X 就是一个表达式
variable = expression
如果 X 是变量，E 是表达式，则λx.E是一个抽象体
abstraction = λ(variable).(expression)
如果 E 和 A 都是表达式，则 EA 是一个应用
application = (expression)(expression)
函数抽象体
在λ演算中，函数是用λ表示的匿名函数。一个匿名函数中只存在标识符和他自己的函数体。下面的表达式定义了一个函数（也叫做λ抽象体）：
\lambda x.x\\
紧跟在λ后面的名字是参数标识符，点（.）后面的表达式是函数体。我们用javascript表示它：
function (x) {
return x
}
改写成箭头函数：
x => x
现在定义一个抽象体，它接收一个变量y，然后返回y的平方，我们可以这么写：
\lambda y.y^2 \\
函数应用
函数可以被应用在表达式上。在表达式 EA 中，E 是一个函数，它被应用到了表达式 A 上。换句话来说，表达式 A 就是表达式 E 的输入，然后输出 E(A) 。
把 E 替换成抽象体 λy.y^2，然后得到下面的式子：
EA = E(A) \\ EA = (\lambda y.y^2)(A)
const E = y => (y ** 2) // Abstraction
E(A) // Application
通过将函数体中的 y 替换成参数 y 的值，来计算这个函数应用的结果。比如：把表达式 A 替换成整数“5”：
EA = (\lambda y.y^2)(A)=y[y:=A]=A^2=5^2=25 \\
y[y:=A]意思是：在函数体中，所有出现变量 y 的地方必须都被替换成表达式 A 。
多参函数
λ 演算中的所有抽象体都只接收一个参数。如果要实现获取多个参数，就要借助多重应用了。如果有下面这样的函数：
f(x,y) = x + y \\
我们其实习惯像下面这样定义和应用它：
const F = (x,y) => (x + y)
F(5, 10)
用不同的方式，我们可以先定义一个函数，这个函数接收一个参数 x ，返回一个新的函数，这个新的函数接收一个参数 y ：
\lambda x(\lambda y.x+y) \\
const F = x => (y => (x + y))
可以通过下面两步，应用这个接收两个参数的函数：
(\lambda x.(\lambda y.x+y))(5)=x[x:5]=\lambda y.5+y \\ (λy.5+y)(10) = y[y := 10] = 5+10 = 15
const F = x => (y => (x + y))
F(5)(10)
// "x => (y => 5 + y)"
// "x => (y => 5 + 10)"
// 15
这个策略就是传说中的“柯里化”（Currying），在Haskell Curry中有介绍。
为了便于理解，想象一个计算矩形面积（A=base * height）的抽象体：
λb. (λh.b * h) \\
const RectangleArea = base => (height => (base * height))
RectangleArea(2)(4)
将 2 传进第一个函数的参数 base ，然后返回一个新的函数。将 4 传进第二个函数，作为 height 的值，最终返回这个矩形的面积。
定义数据类型
在无类型λ演算中，函数是唯一的基础类型。所以，如果要使用布尔类型，数字类型以及算数运算，就需要定义一些抽象体去表示它们。接下来我们定义一些比较简单的类型及它们的运算：布尔类型，and 与 or 操作。
如果你想深入了解，推荐看一看 The untyped Lambda Calculus
Alonzo Church 这样定义布尔类型：
true = λa. (λb.a)\\ false = λa. (λb.b)
const True = a => b => a
const False = a => b => b
可以把布尔值的逻辑运算看作是一种“抉择行为”。上面两个函数中，都有2个参数，最终返回其中一个参数。不同的是，函数 True 选择返回第一个参数，而函数 False 选择返回第二个。
基于上面的定义，可以得出 If-then-else 的结构：
if = λp.(λa. (λb. p\ a\ b)) \\
const If = Condition => Then => Else => Condition(Then)(Else)
如果 Condition 的位置接收到的是 True ，那么就会返回 Then 作为结果，因为 True 总是返回第一个参数。如果 Condition 的位置接收到的是 False ，那么就会返回 Else 作为结果，因为 False 总是返回第二个参数。
定义下面两个log函数，帮助我们查看运行结果
const isTrue = () => "it's true!"
const isFalse = () => "it's false!"
将布尔值传进 If ：
const First = If(True)(isTrue)(isFalse)
const Second = If(False)(isTrue)(isFalse)
First() // "it's true!"
Second() // "it's false!"
现在我们通过化简的过程解释这个结果。我们可以发现 a 其实就是 Then ， b 就是 Else ：
if\ true = λp.(λa.(λb. p\ a\ b))\ true = p[p := true] = true\ a\ b = λa.(λb.a) a\ b = a \\ ...\\ if\ false = λp.(λa.(λb. p\ a\ b)) false = p[p := false] = false\ a\ b = λa.(λb.b) a\ b = b \\ ...\\
在了解了 If 的定义之后，再看看 and 和 or 的定义：
and = λp.(λq. p q p)\\ or = λp.(λq. p p q)
const And = Exp1 => Exp2 => Exp1(Exp2)(Exp1)
const Or = Exp1 => Exp2 => Exp1(Exp1)(Exp2)
在数学逻辑运算中，只有当两个表达式都是 true 的时候， and 操作符才会返回 true 。 or 操作符只有当两个表达式都是 false 的时候，才会返回 false 。基于上面的结论，函数 And 始终会返回 False ，除非 And(True)(True) 这样调用它。函数 Or 始终会返回 True ，除非 Or(False)(False) 这样调用它。
只需要通过置换操作符应用中的变量，就能检验上面所定义的式子。比如像下面这样：
and\ true\ false = λp.(λq. p\ q\ p)\ true\ false = p[p := true] = q[q := false] = true\ false\ true = λa.(λb. a) false\ true = false \\ ...\\ or\ true\ false = λp.(λq. p\ p\ q) true\ false = p[p := true] = q[q := false] = true\ true\ false = λa.(λb. a) true\ false = true \\ ...
下面是所有可能的化简过程：
| Operator | Reduction | Result |
|-------------------|---------------------|-----------|
| And(True)(True) | True(True)(True) | True |
| And(True)(False) | True(False)(True) | False |
| And(False)(True) | False(True)(False) | False |
| And(False)(False) | False(False)(False) | False |
| Or(True)(True) | True(True)(True) | True |
| Or(True)(False) | True(True)(False) | True |
| Or(False)(True) | False(False)(True) | True |
| Or(False)(False) | False(False)(False) | False |
到目前为止，我们已经定义了很多结构，如： True ， False ， If ， And ， Or ，接下来通过比较简单和直观的方式检验一下：
const Result1 = If(And(True)(True))(isTrue)(isFalse)
const Result2 = If(And(True)(False))(isTrue)(isFalse)
const Result3 = If(Or(False)(True))(isTrue)(isFalse)
const Result4 = If(Or(False)(False))(isTrue)(isFalse)
Result1() // "it's true"
Result2() // "it's false"
Result3() // "it's true"
Result4() // "it's false"
最后，你需要记住的是，λ演算并不是数据类型的具体实现，只是一个形式化的系统，它并不需要代表任何计算过程，因为都可以使用函数去模拟它们。
λ演算和函数式编程
通过图灵机描述的可计算性，引出了命令式编程。通过λ演算描述的可计算性，引出了函数式编程 -- Cooper & Leeuwen（2013）
早在电子计算机诞生之前，Alonzo Church 就创造了λ演算。但它对现代编程语言却有着深远的影响。作为第二个高级编程语言的Lisp，它就是启发自λ演算。再比如说，所有支持匿名函数的语言里（像Haskell，JavaScript，Python，Ruby等等）都会有几分Alonzo Church的影子。
函数式的模式催生表达能力强的代码，因为这些模式与数学模型有着更加直接的对应关系，因此也更加合理。正因为在数学的世界里，函数式的代码具备引用透明性（给定相同的输入，始终会有相同的输出），这让它可以在多个处理器中同时运行。
λ演算影响着多种多样的现代编程语言，这不仅仅是因为它的形式化系统是图灵完备的，也是因为它的简洁性和表达能力，这些层面上的能力是对未来的编程是非常重要的。
参考资料
Henk Barendregt, Erik Barendsen (2000). Introduction to Lambda Calculus.
Raúl Rojas (1998). A Tutorial Introduction to the Lambda Calculus.
Manuel Eberl (2011). The untyped Lambda Calculus.
Barry Cooper, J. van Leeuwen (2013). Alan Turing: His Work and Impact .
