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

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

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

---

演算

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

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

表达式

其由下列符号组成：

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

定义：

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

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

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

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

应用形式表示将应用在上，类似于函数的调用。

规约

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

前置知识：

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

替换(Substitution)是规约的基本动作：表示用表达式替换在表达式中出现的自由变量。

演算的三种规约

表示归约过程：

• 变换：变换允许改变约束变量的名字。例如：通过变换改变为，记为。经过变换后的项是等价的。
• 归约：类似于函数求值过程，将替换作用于（应用）。的归约为，记为，它陈述了若所有的。
• 变换：指出，如果两个函数对于所有的参数都能给出一致的结果，那么这两个函数是等价的。

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

例子

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

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

$$\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. 一个形如的项被称为可约项。如果一个项不含有可约项，则称其为范式。若一个项P可以经过规约到Q，则称Q为P的范式。
2. 若P存在范式，那么该范式在变换下唯一。
3. 若P存在范式，那么P最左侧且最外的规约方式总能保证得到这个范式。
4. 项是否存在范式是不可判定的。