λ 演算及其与图灵机的等价性
上级：logic
丘奇（Church）的 λ 演算（1930 年代初）是"可计算"这个概念的另一种定义——它诞生于函数，而非机器。两者能力相同，气质相反：图灵 → 通向计算机，丘奇 → 通向证明助手。
演算本身——三种构造，一条规则
项与 β-归约项： 一个变量
x；一个抽象（abstraction）λx.M（即函数x ↦ M）；一个应用（application）M N。 计算规则（β-归约）：(λx.M) N → M[x := N]——用实参替换被绑定的变量。（此外α表示绑定变量的重命名，η表示外延性。） 计算 = 反复做 β-归约，直到得到一个范式（normal form，即不再含可归约项），如果存在这样一个范式的话。
一切都是函数——没有内建的数字、布尔值或循环，它们全部都是编码出来的。
为什么它有图灵机那么强
- 丘奇数（Church numerals）：
n ≡ λf.λx. f (f (… (f x)))——"把f应用n次"。有了它，succ、+、×、exp就都可以写成 λ 项。 - 数据：
true ≡ λx.λy.x，false ≡ λx.λy.y，以及序对、列表——都可以编码。 - 不靠名字实现的递归：
Y组合子Y ≡ λf.(λx.f (x x)) (λx.f (x x))满足Y g = g (Y g)——这是一个不动点算子，由它给出无界递归。它是克莱尼（Kleene）μ-算子 /while循环在 λ 世界里的对应物——正是它把这套演算从原始递归提升到了完整的图灵能力。
手算一遍
K a b = a（这个"取第一个"组合子），一步步做——每个 ⇒ 都是一次 β-归约：
(λx.λy.x) a b ⇒ (λy.a) b ⇒ a
丘奇算术同样机械——succ 0 = 1，其中 0 ≡ λf.λx.x、succ ≡ λn.λf.λx. f (n f x)：
(λn.λf.λx. f (n f x)) (λf.λx.x)
⇒ λf.λx. f ((λf.λx.x) f x)
⇒ λf.λx. f ((λx.x) x)
⇒ λf.λx. f x = 1
写成代码——解释器小得惊人
data Term = Var String | Lam String Term | App Term Term
subst :: String -> Term -> Term -> Term -- [x := s] t (naive; closed terms only)
subst x s (Var y) = if x == y then s else Var y
subst x s (App a b) = App (subst x s a) (subst x s b)
subst x s (Lam y t) = if x == y then Lam y t else Lam y (subst x s t)
beta :: Term -> Maybe Term -- one normal-order step
beta (App (Lam x t) s) = Just (subst x s t) -- the β-redex
beta (App a b) = case beta a of
Just a' -> Just (App a' b)
Nothing -> App a <$> beta b
beta (Lam x t) = Lam x <$> beta t
beta _ = Nothing
normalize :: Term -> Term
normalize t = maybe t normalize (beta t)
整个语言就是三个构造子加一条规则——β 归约只是一次模式匹配。（真正的解释器还会加上α-重命名以避免变量捕获，这里省略了。）
等价性（丘奇、克莱尼、图灵，1936–37）
λ-可定义 = 图灵可计算 = 一般递归一个数论函数可由某个 λ 项定义（借助丘奇数）当且仅当它可被某台图灵机计算当且仅当它是一般递归的。
Proof先固定接口：一个封闭的 λ 项
F计算了f:ℕ→ℕ，是指对每个n，F ⌜n⌝都 β-归约到⌜f(n)⌝，其中⌜n⌝是对应的丘奇数。要证明的是：F-可定义的f与图灵机可计算的f是同一批函数。
TM → λ。 转移表δ是有限的，所以可以写出一个 λ 项step，它对编码后的(状态, 读到的符号)做分支判断——用到布尔值/序对/列表的编码——并返回下一个格局（写下的符号、读写头移动方向、新状态）。把整个格局也编码成一个 λ 项（纸带 = 一对列表加读写头符号加状态）。然后用Y反复迭代step，配合一个布尔的halted?判断，直到进入停机状态；读出纸带内容即得⌜f(n)⌝。于是每一个图灵机可计算的函数都是 λ-可定义的。
λ → TM。 替换M[x:=N]以及"找到最左最外层的可归约项"，都是关于项的字符串编码的原始递归操作——所以一台图灵机可以执行一步正规序（normal-order）β-归约，并不断重复。由标准化定理（standardization theorem）可知，只要范式存在，正规序归约就一定能到达它；因此当且仅当F ⌜n⌝有范式时，这台图灵机才会输出⌜f(n)⌝。两个方向的模拟都是可行的（effective），所以这两类函数相等（再由克莱尼的结果，它们也等于一般递归函数这一类）。∎
丘奇–罗瑟定理（合流性）β-归约是合流的（confluent）：如果一个项沿两条不同路径归约，其结果总能重新汇合到一起。因此范式一旦存在就是唯一的——即便归约的顺序是自由的，答案本身与顺序无关。