本文是
λ演算的入门文章，希望大家看文本文能对什么是λ演算有个基本的认识。
λ演算是从数学逻辑中的形式系统（formal system）。它以变量绑定和替换的原则，研究如何使用函数抽象和应用来表示计算。
所谓 形式系统 ：这是数学中的东西，它包含了形式语言和推导规则。我们可以从公理出发，通过推导规则推导证明出定理、推论和猜想，从而形成一整套完整的体系，那么这套体系就是一个形式系统。而 形式语言 就是用于表示定理、推导过程的语法。
由来
希尔伯特第十问题（判定问题，Entscheidungsproblem）：是否能找到一种普遍的算法 ， 可用来判定一个任意形式的丢番图方程（即整系数代数多项式方程）是否有整数解， 从而一劳永逸地解决这类问题？
如果要解决这个问题，从问题的描述看需要先解决两个问题：1、什么是算法，2、有限次该怎么具体描述。为了解决这些问题，Alan Turing和Alonzo Church各自从不同角度给出了两种计算模型，也就是将计算过程形式化，通过这两个模型能够精确的表示出过程并给出有限次计算的定义。
关于这个问题的历史研究请参考：Hilbert 第十问题漫谈 (上)
图灵机
图灵在 1936年发表了《On Computale Number，with an Application to the Entscheidungsproblem》，该论文主要研究了什么样的运算可以用抽象计算机来实现，并提出了一种数学模型 — 图灵机，并证明了不存在解决停机问题的通用算法。此外论文描述了什么是图灵机，并证明了只要实现了图灵机，就可以计算任何可计算问题。
这里有一个很关键的名词：可计算问题。首先，我们知道的是在计算机领域，我们所研究的一切问题都是**计算问题，而计算问题就是指一切与计算相关**的问题。比如：
- 给定一个正整数n，判断它是否是素数。
在计算问题中，有些问题是可以解决的，有些问题是不可解决的，而这就引出了计算问题的可计算性。它可以理解为，是否存在一个算法，能解决在任何输入下的此计算问题。比如上述例子，我们可以找到一个算法，并判断其是否是一个素数。所以这是一个可计算问题。
而有些问题是不可计算的，比如著名的停机问题，它的表述是这样的：给定一个程序的描述和一个有效的输入，运行程序后，请判断该程序是否能在有限时间内结束，亦或是说陷入了死循环。
此外还有不可判定理论，这就不属于本文的内容了。
图灵的论文证明了对于一个问题，对于任何输入，只要人类可以保证算出结果，那么图灵机就可以保证算出结果。
所以说，图灵清晰地定义了什么是可计算并给出了通用机（图灵机），同时还有计算模型的极限（不存在解决停机问题的通用方法）。所以人们使用物理有段实现了图灵机就能实现机器计算，比如冯诺依曼架构的计算机。
参考：什么是图灵完备？ - Ran C的回答 - 知乎 www.zhihu.com/question/20…
λ演算
事实上，在图灵机提出之前，数学家阿隆佐·邱奇就提出了λ演算来解决希尔伯特的第十问题 。λ 演算是从数学的角度进行抽象，不关心运算的机械过程而只关心运算的抽象性质，只用最简洁的几条公理便建立起了与图灵机完全等价的计算模型，其体现出来的数学抽象美开出了函数式编程语言，Lisp、Scheme、Haskell… 这些以抽象性和简洁美为特点的语言至今仍然活跃在计算机科学界。
虽然由于其本质上源于 λ 演算的抽象方式不符合人的思维习惯从而注定无法成为主流的编程语言，然而这仍然无法妨碍它们成为编程理论乃至计算机学科的最佳教本。而诞生于函数式编程语言的神奇的Y combinator至今仍然让人们陷入深沉的震撼和反思当中…
λ演算是图灵完全的，所以说使用纯函数可以模拟图灵机，也就是说纯函数可以模拟所有的面向对象程序。
λ演算基础
表示方法
我们先来看一下 λ演算的表示方式，其表示方式非常简单，只有三种：变量、函数抽象和应用。
| 名称 | 语法 | 示例 | 解释 |
|---|---|---|---|
| 变量 | <variable> |
x |
定义一个名为 x 的变量 |
| 函数抽象 | λ<name>.<expr> |
λx.x |
定义一个参数为x，返回x的变量 |
| 应用 | (<func> variable) |
(λx.x)a |
将变量a的值作用于函数λx.x |
这里举的函数例子就是
I组合子— 恒等函数。
λ演算 的三种表达式也可以这样表示：
<expression> := <variable>
<expression> := λ <variable>.<expression>
<expression> := (<function> <expression>)
值得注意的是： λ演算 只有函数，而且是一个参数函数，返回值也是函数的单参函数。所以虽然说这里 <variable> 和 (<function> <expression>) 最终代表是还是函数 λ <variable>.<expression>。
运算法则
α-转换（alpha）
α-转换 规则告诉我们在函数中，变量名称一点也不重要，重要的是变量的位置和括号，比如 λab.ab 和 λxy.xy 其实是同一个函数，而 λab.ab 和 λab.ba 则不是同一个函数。
我们将通过 α-转换 变换函数参数名称（如 x 变成 y ）记为 α[x / y] 。
β-规约（beta）
β-规约 这条规则是指把实参作用到函数的过程，相当于求值的过程。比如：
(λx.x)a的β-规约结果为:a;(λx.y)a的β-规约结果为:y;
柯里化
λ演算 的函数都是一个参数函数，返回值也是函数的单参函数。比如 λx.(λy.plus x y)，我们就可以用多参函数表示： λxy.plus x y，而将多参函数转换为单参函数的方法就是**柯里化**。
柯里化的过程就是接受一个多个参数函数，然后返回一个参数为原函数的第一个参数，返回值为原函数剩余参数及其函数体组成的函数（若返回函数仍是多参函数，则继续柯里化）。比如：
一个多参函数：λxyz.plus x y z，进行柯里化之后为： λx.(λy.(λz.plus x y z))。
再举个 js 的例子：
const add = (x, y, z) => (x + y +z)
// 调用过程为 : add(1, 2, 3)
// 则进行柯里化之后为：
const add_curry = x => y => z => (x + y +z)
// 调用过程为 : add(1)(2)(3)
自由标识符 和 约束变量
- 函数
λx.x中x被称为约束变量，因为它既在函数体中又是形参。 - 函数
λx.x y中y被称为自由变量，因为它没有在参数中出现。
λ演算的整数--邱齐整数
在 λ 演算中只有函数，甚至没有整数、字符串，整数是可以由函数表示。
0 : λfx.x
1 : λfx.f x
2 : λfx.f (f x)
3 : λfx.f (f (f x))
...
在这里，整数的含义是传入的第一个函数 f 被作用的次数。比如 0 就是 f 被调用了 0 次，而 3 则是 f 被调用了3 次。
以此类推。直观地说，λ演算中的数字 n 就是一个把函数 f 作为参数并以 f 的 n 次幂为返回值的函数。
邱奇整数是一个高阶函数 -- 以单一参数函数
f为参数，返回另一个单一参数的函数。
后继函数
后继函数实际上就是 n + 1 的作用：
SUCC : λn.λf.λx. f(n f x)
从邱齐整数的定义我们可以看出，后一个整数比前一个整数多了一次 f 的调用。所以想要进行 n+1 操作，只需要为 n 多调用一次 f 即可构建出整数 n+1。
为了更好的理解 SUCC 函数，让我们把 SUCC 函数看成 λn.(λf.λx. f(n f x))，这样是不是就更清晰了，这是一个接受整数 n，且返回一个整数函数的单参函数。在让我们看函数的 body 部分，body 中的 (n f x) 部分实际上就是一个需要 β-规约 的部分，因为整数 n 实际上是一个接受 f 和 x 的函数，所以分别应用了 f，x 后，就求值了。
让我们进行一个计算：SUCC 3
SUCC 3 = λn.λf.λx.f(n f x) (3)
= λn.λf.λx.f(n f x)(λfx.f (f (f x))) // 将整数 3 替换成对应的函数
= λn.λf.λx.f(n f x)(λfa.f (f (f a))) // 对后者函数进行 α-转换， x->a
= λf.λx.f((λfx.f (f (f x))) f x) // 进行 β-规约，应用f
= λf.λx.f((λx.f (f (f x))) x) // 进行 β-规约，应用x
= λf.λx.f(f (f (f x)))
= 4
加法
PLUS : λm.λn.λf.λx. m f(n f x)
从上述表示方式，我们可以看出，加法函数比后继函数仅仅多了一个参数m。所以整体上的思路是和上面一样的。
让我们进行一个计算：PLUS 3 2
PULS 3 2 = λm.λn.λf.λx.m f(n f x) (3 2)
= λf.λx.3 f(2 f x)
= λf.λx.(λfx.f (f (f x))) f(2 f x)
= λf.λx.f (f (f (2(f x)))
= λf.λx.f (f (f (λfx.f (f x)(f x)))
= λf.λx.f (f (f (f (f x))))
= 5
还有乘法等算术运算请自行查询...
逻辑与谓语
首先，我们先看一下邱齐布尔值：
TRUE : λxy.x
FLASE : λxy.y
事实上，
FLASE就是之前所看到的 邱齐整数 0。
逻辑运算：
AND : λxy. x y TURE
OR : λxy. x FLASE y
NOT : λx. x FLASE TRUE
有了这些之后，我们可以做一些逻辑运算了，比如 AND TRUE FALSE
AND TRUE FALSE = (λxy. x y TURE)(TRUE FALSE)
= (λy. TRUE y TRUE)(FALSE) // 一次 β-规约
= TRUE FALSE TRUE // 一次 β-规约
= (λxy.x)(FLASE TRUE) // 把第一个 TURE 对应的函数代进来
= (λy. FLASE)(TRUE) // 一次 β-规约
= FALSE // 一次 β-规约
熟练了的话，这里2、3 两步可以合成一步完成。
Y组合子
至此，我们的 λ演算 已经完成正常的算术运算和逻辑运算了，但是还存在一点缺陷，那就是递归。
但是本章的标题是 Y组合子，和这里说的递归有什么关系？慢慢来，在说Y组合子和递归之前，我们先看下什么是不动点。
不动点
在数学中，不动点就是 f(x)=x，注意，这里的 f(x)=x 不是一个函数，而是指对于任意函数，存在一个值使得函数 f 的计算结果等于值本身。比如函数 f(x) = x^2^ -3x + 4 的不动点就是 2。所以说，数学中的不动点就是函数映射到本身的那些点。
如何理解不动点定理，请看知乎的回答：www.zhihu.com/question/21…
不动点组合子 就是用来计算其他函数的一个不动点的高阶函数。
Y组合子
首先，我们看一下什么是组合子？
引用ajoo的话:
组合子，英文叫combinator，是函数式编程里面的重要思想。如果说OO是归纳法（分析归纳需求，然后根据需求分解问题，解决问题），那么 “面向组合子”就是“演绎法”。通过定义最基本的原子操作，定义基本的组合规则，然后把这些原子以各种方法组合起来。
引用另外一位函数式领域的大师的说法：
A combinator is a function which builds program fragments from program fragments.
强烈推荐: ajoo的面向组合子程序设计方法系列文章(推荐一下)：论面向组合子程序设计方法
Y组合子是Haskell B. Curry在研究 λ 演算时发现的，它可以得到任意函数的不动点。
正是因为它可以得到任意函数的不动点，所以它可以找出任意递归函数的匿名表示方法，具体推导请参见下一节。
Y组合子的表示方法：λf.(λx.f(x x))(λx.f(x x)) 。
让我们看一下 Y 组合子是如何找到任意函数的不动点的，这里我们尝试使用 Y组合子去找任意函数 G 的不动点：
Y G = λf.(λx.f(x x))(λx.f(x x)) (G)
= (λx.G(x x))(λx.G(x x))
= G((λx.G(x x)) (λx.G(x x)))
= G(Y G)
我们推导 YG 得到了 G (YG)， 即 YG=G(YG)，所以，我们就得到了任意函数G的不动点 YG。
递归
其实大家对递归函数都非常熟悉，比如我们非常常见的求阶乘函数就是通过递归实现的：
let fact(n) = if n === 0 then 1 else n * fact(n-1)
这是一个语义化的表达方式，让我们转换成
λ表示式
let F = λn.IsZero n 1 (Mult n (F (Pred n)))
// 其中:
// IsZero 函数判断接受的n是否等于0，接受三个参数：n、1和 Mult函数；
// Mult 函数表示乘法操作，接受两个参数；
// Pred 函数表示减一操作，接受一个参数
让我们仔细观察上面这个定义，它比起我们之前的 λ 表达式多了 let F = 这一部分，即定义了一个标识符来表示该函数，也就是我们强行给这个函数起了一个函数名。但是我们须知道的一点是：λ 符号的引入就是为了去掉函数名这个冗余，使定义匿名函数成为可能。 也就是说，在 λ 演算中，函数其实是没有名字的，这里函数的名字只是用来表示函数的本体，让我们少写一点字而已。所以在 λ 演算中，我们可以全用匿名函数来表示递归函数。
但是从直觉来看，这又怎么可能呢，递归函数调用了函数本身，你连函数本身的名字都没有，怎么做到递归？所以，这就是Y组合子的强大之处，因为它做到了。
还是上面的函数 λn.IsZero n 1 (Mult n (F (Pred n)))，我们把它想象成是另一个函数 G 传入参数 F 后的规约结果，那么这个函数 G 是怎么样子的呢：
G : λf.λn.IsZero n 1 (Mult n (f (Pred n)))
然后，我们对 G 做 β-规约 （传入 F，就可以得到） ：
G(F) = λf.λn.IsZero n 1 (Mult n (f (Pred n))) (F)
= λn.IsZero n 1 (Mult n (F (Pred n))) // 做一次 β-规约
= F
看到了吗，这里是不是有个上面出现过的东西：G(F) = F，这个不就是不动点（f(x)=x）嘛，所以，现在这个F 是什么，就是函数 G 的不动点啊，那么现在求函数 F 的这个问题就被巧妙的转换成了求函数 G 的不动点了。
那么怎么得到函数 G 的不动点呢，上一节我们就提到了，当然是 Y 组合子了，Y 组合子很方便地帮我们找到了函数G 的不动点 — YG，也就是说，我们已经找到了 F 的匿名表示方式。让我们验证下，这个YG 是不是正确的，我们计算下 Fact 3：
Fact 3 = YG 3
= G (YG) 3 // YG = G (YG)
= (λf.λn.IsZero n 1 (Mult n (f (Pred n)))) (YG) (3) // 将 G 的函数本体代入
= λn.IsZero n 1 (Mult n ((YG) (Pred n))) 3 // 进行一次 β-规约 (YG代入)
= IsZero 3 1 (Mult 3 ((YG) (Pred 3))) // 进行一次 β-规约 (3 代入)
= 3 * ((Y G) 2) // 根据函数定义计算一下结果
= 3 * 2 * ((Y G) 1) // 再求一次 YG 2
= 3 * 2 * 1 *((Y G) 0) // 再求一次 YG 1
= 3 * 2 * 1 * 1 // 再求一次 YG 0
所以可以看到，YG 确确实实就是函数Fact的匿名表示方式。
这就是强大的 Y组合子，它可以在 λ 演算中找出任意递归函数的匿名表示的方法，而且形式及其简单，就是 YG，其中 G: λf.Sf，这里的 S 表示递归函数的函数本体。
参考：
Y 组合子的推导
本部分内容参考
g9yuayon大佬的博文： Lambda算子5b：How of Y，代码以JS展示。如果在阅读过程中遇到了看不懂的地方，请前往
g9yuayon大佬的博文继续理解。
我们知道 Y 组合子是用来可以找出任意递归函数的匿名表示方法，那么反过来，我们也可以在推导匿名递归函数的过程中重新抽象出Y组合子来。
首先，我们用 JS 写出上一节的求阶乘函数：
const fact = n => (n < 2 ? 1 : n * fact(n - 1))
这是一个规规矩矩的递归函数，为了去除函数体中 fact 函数，让我们对函数进行一层抽象，把fact当成参数。
const G = self => n => (n < 2 ? 1 : n * self(n - 1))
console.log(G(fact)(3)) // => 6
// 实际上 G(fact) = fact
虽然函数G中是没有 fact 函数的字样了，但是实际上这只是在函数外部套了一层函数，因为 G(fact) = fact。虽然这层抽象很重要，但是这并不是我们眼前要的结果，我们想要的是什么？匿名递归函数！即函数体内去除定义的函数名称，这怎么办呢？答案就是：让函数去调用自身！即把函数本身作为参数传递给自己。
const fact2 = self => n => (n < 2 ? 1 : n * self(self)(n - 1))
console.log(fact2(fact2)(3)) // => 6
这里的 fact2 变量只是函数 self => n => (n < 2 ? 1 : n * self(self)(n - 1)) 的一个代号而已了，因为函数体内不再包含这个名词。所以说，至此，我们已经实现了匿名的递归函数。
但是这是只是这个特定函数的匿名表示，所以，现在我们需要基于这个特定的匿名表示，去推导出一个通用的求递归函数匿名表示的函数，也就是 Y组合子。
那么就让我们先把本函数的特定逻辑（也就是求阶乘的逻辑）提取出来吧：
const fact3 = self => n => {
// 提取出来的求阶乘部分的特定逻辑
const g = h => n => (n < 2 ? 1 : n * h(n - 1))
return g(self(self))(n)
}
const fact = fact3(fact3)
console.log(fact(3)) // => 6
可以看到 fact3 函数的内联函数 g 是一个独立的纯函数，所以，我们可以将其提取到函数外面。
让我们再看一下这个内联函数
g，你是不是有种似曾相识的感觉，没错，这就是上面的函数G。
const G = self => n => (n < 2 ? 1 : n * self(n - 1))
// 提取出来的求阶乘部分的特定逻辑
const fact3 = self => n => G(self(self))(n)
const fact = fact3(fact3)
console.log(fact(3)) // => 6
还记得上一节中的 F = YG 吗，Y 组合子就是接受了递归函数 F 抽象后的函数，然后得到了递归函数 F 匿名表示方式。
其实上面的代码已经和 Y组合子很接近了，把上面代码和 F = YG 一一对应一下，F 就是 fact，G就是G，那么 Y组合子 就是第4行到第8行的表示了。让我们将其写成函数表示：
const G = self => n => (n < 2 ? 1 : n * self(n - 1))
const Y = g => {
const f = self => n => g(self(self))(n)
return f(f)
}
const fact = Y(G)
console.log(fact(3)) // => 6
// 我们做个验证：
// fact4(3) => Y(G)(3) => f(f)(3)
// f(f)(3) => x => f(f(f))(x) => (n => (n < 2 ? 1 : n * g(g)(n - 1)))(x) => 传入 3：3 * f(f)(2)
// f(f)(2) => x => f(f(f)(x))
看到了吗，我们什么都没有做，仅仅是将4~8行代码放到了一个新的函数中，该函数接受G，返回f(f)，这个新函数就是Y组合子:
const Y = g => {
const f = h => n => g(h(h))(n)
return f(f)
}
让我们将这个 JS 版的 Y 组合子和 λ 演算中的 Y组合子对比一下是不是一致的。
其中， λ 演算中的 Y组合子：λf.(λx.f(x x))(λx.f(x x))，为了便于对应，我们将 λ 演算中的 Y组合子进行 α-转换，将 f 转换成 t：λt.(λx.t(x x))(λx.t(x x))。
// 参数 g 就是 t
const Y = g => {
// 内联函数 f 就是 (λx.t(x x))
// x 就是 n => g(h(h))(n) 这个函数，这里的 n 是任意东西，可不是单单表示一个数，还可以是数组等...
const f = h => n => g(h(h))(n)
// 这里的 return f(f) 就是 (λx.t(x x))(λx.t(x x))
return f(f)
}
总结
λ演算还是很有意思的，作为函数式编程的基础，还是要对其有个基本的了解。同时在学习的过程中，还了解了图灵机和λ演算由来的历史：希尔伯特第十问题、康托尔的对角线方法和哥德尔的不完备性定理等数学家们的伟大发现。
