本文是
λ演算的入门文章，希望大家看文本文能对什么是λ演算有个基本的认识。
λ演算是从数学逻辑中的形式系统（
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 // 一次 β-规约
复制代码
