1936年，图灵在论文中引入了Turing Machine的概念，与此同时他在丘奇门下攻读博士学位。

而后经Kleene证明：$\lambda$演算、Turing Machine 和 Kurt Gödel引入的general recursion 函数等价。并由此提出了一个伟大命题——即任何可计算的东西都能被这三种方式所表达。

而函数式语言起源于 丘奇提出的$\lambda$演算。

---

$\lambda$ 演算

$\lambda$演算是图灵完全的，这个计算模型可以解决任何可以机械计算的问题。

$\lambda$演算是一个形式系统，通过$\lambda$项和变换操作表达计算。

$\lambda$ 表达式

其由下列符号组成：

• 变量：字符或字符串
• Lambda：$\lambda$
• 点：.
• 括号：()

$\lambda \ Term $ 定义：

1. 一个变量是$\lambda$项，通常用小写字母表示。
2. 如果M是$\lambda$项，那么$\lambda x.M$也是，这种形式称为抽象形式。
3. 如果M和N都是$\lambda$项，那么 M N 也是，这种形式称为应用形式。

除了以上的三种方式外均不能构成$\lambda$项；并且在以下情况下（即没有歧义）可以省略括号：

• $\lambda$项最外层的括号可以省略，即$M N$与$(M N)$是等价的。
• $M N$是左结合的，即$M N P$ 与 $((M N)P)$是等价的。
• 如果没有括号约束，抽象形式是尽量向右侧拓展的，即：$\lambda x.M N$与$\lambda x.(M N)$等价。

抽象形式$\lambda x.M$定义了一个从$x$到$M$的映射；这个函数没有名称，以$x$为参数，$M$为输出。

应用形式$M N$表示将$N$应用在$M$上，类似于函数的调用$M(N)$。

规约

以上只是形式化的定义，我们需要定义相应的运动的操作,以使$\lambda$表达式实现演变。

前置知识：

• 约束变量：在抽象形式的定义中，$\lambda x.M$是将输入变量$x$绑定到$M$表达式中的$x$。则$M$中的$x$为约束变量。
• 自由变量：不存在上述关系的变量。

替换(Substitution)是规约的基本动作：$E[v:=R]$表示用表达式$R$替换在表达式$E$中出现的自由变量$v$。

$\lambda$演算的三种规约

$\rightarrow$表示归约过程：

• $\alpha$变换：$\alpha$变换允许改变约束变量的名字。例如：$\lambda x.x$通过$\alpha$变换改变为$\lambda y.y$，记为$\lambda x.x\rightarrow\lambda y.y$。经过$\alpha$变换后的$\lambda$项是等价的。
• $\beta$归约：类似于函数求值过程，将替换作用于（应用）。$(\lambda x.M) N$的$\beta$归约为$M[x:=N]$，记为$(\lambda x.M) N\rightarrow M[x:=N]$，它陈述了若所有的。
• $\eta$变换：指出，如果两个函数对于所有的参数都能给出一致的结果，那么这两个函数是等价的。

$\lambda$演算以$\beta$归约为主，因为其本质就是函数的调用，对应一组计算步骤，这个步骤重复应用$\beta$归约，直到不能再被替换。

例子

$ \lambda x.(\lambda y.(x * x + y * y)) $

表示一个以$x$为参数的函数(事实上，这种函数形式称为柯里化形式，且可以证明任何多参函数都可以转化为此种形式，即高阶函数)，返回一个以$y$为参数的函数。令$x=3,y=4$，则$\beta$规约为：

$$\begin{aligned} (\lambda x.(\lambda y.(x * x + y * y))\ 3)\ 4 \rightarrow (\lambda y.(3 * 3 + y * y))\ 4 \rightarrow 3 * 3+4*4 \end{aligned}$$

规约定理

1. 一个形如$(\lambda x.M)\ N$的$\lambda$项被称为$\beta$可约项。如果一个$\lambda$项不含有$\beta$可约项，则称其为$\beta$范式。若一个$\lambda$项P可以经过$\beta$规约到Q，则称Q为P的$\beta$范式。
2. 若P存在$\beta$范式，那么该$\beta$范式在$\alpha$变换下唯一。
3. 若P存在$\beta$范式，那么P最左侧且最外的规约方式总能保证得到这个$\beta$范式。
4. $\lambda$项是否存在$\beta$范式是不可判定的。