无类型的Lambda演算

参考资料：The Lambda Calculus Its Syntax and Semantics

Lambda项

关于归纳定义，可参见从不动点定理到编程语言
Lambda演算是函数的演算
- 函数 $f$ –> 抽象 $\lambda x.f(x)$
- 求值 $f(a)$ –> 应用 $(\lambda x.f(x))(a)$
- 函数的变量可以重命名，
  $f \rightarrow \lambda x.f(x),\; \lambda y.f(y).$
- 函数的求值可以视为替换，
  $f(a) \rightarrow (\lambda x.f(x))(a) = f(x)|_{x = a}.$
- 在不同的地方， $\lambda x.f(x)$ 有不同的形式。在数学中，它可以记为 $x \mapsto f(x)$ ；在编程语言中，它可以记为fn x => f(x)
上面的演算经过形式化，可以得到无类型的Lambda演算，它可能不符合函数的特点。比如，函数应该应用于变量，但是我们允许变量应用于变量
- （变量）变量的集合 $V$
- （抽象）变量 $x$ ，表达式 $M$ –> $\lambda x. M$
- （应用）表达式 $M$ 、 $N$ –> $MN$
Lambda项，归纳定义
- （变量）如果 $x \in V$ ，那么 $x \in \Lambda$
- （抽象）如果 $x \in V$ ， $M \in \Lambda$ ，那么 $\lambda x.M \in \Lambda$
- （应用）如果 $M$ 、 $N \in \Lambda$ ，那么 $MN \in \Lambda$
的子项，归纳定义
- （变量） $Sub(x) = \{ x \}$
- （抽象） $Sub(\lambda x.M) = Sub(M) \cup \{ \lambda x.M \}$
- （应用） $Sub(MN) = Sub(M) \cup Sub(N) \cup \{ MN \}$
的自由变量，归纳定义
- （变量） $FV(x) = \{ x \}$
- （抽象） $FV(\lambda x.M) = FV(M) - \{ x \}$
- （应用） $FV(MN) = FV(M) \cup FV(N)$
- 也就是说，出现在 $\lambda$ 后面的变量是绑定变量，不出现在 $\lambda$ 后面的变量是自由变量。如果 $FV(M) = \emptyset$ ，即 $M$ 没有自由变量，那么 $M$ 称为闭的Lambda项

替换、Alpha转换、Beta化归

在Lambda项中，将其中的变量替换为另一个Lambda项，记为
$M[x \mapsto N]$
替换的规则，归纳定义
- （变量） $x[x \mapsto N] \equiv N$ ， $y[x \mapsto N] \equiv y$ （ $x \not\equiv y$ ）
- （抽象） $(\lambda y.M)[x \mapsto N] \equiv \lambda y.(M[x \mapsto N])$
- （应用） $(M_1M_2)[x \mapsto N] \equiv (M_1[x \mapsto N])(M_2[x \mapsto N])$
（Alpha转换）将函数的变量重命名为变量，这对应于Alpha转换（Alpha Conversion）
$\lambda x.M \equiv_\alpha \lambda y.M[x \mapsto y].$
我们需要避免如下的情形，比如
- （新的绑定旧的） $\lambda x.y \not\equiv_\alpha \lambda y(new).y(old)$
- （旧的绑定新的） $\lambda x.(\lambda z.(\lambda y.x)) \not\equiv_\alpha \lambda y(new).\lambda z.\lambda y(old).y(new)$
- 也就是说，重名名使用的变量 $y$ 不能是 $M$ 的自由变量，也不能是 $\lambda$ 后面的绑定变量，所以我们必须使用全新的变量，比如
  $\lambda x.y \equiv_\alpha \lambda z.y,\; \lambda x.(\lambda z.(\lambda y.x)) \equiv_\alpha \lambda w.\lambda z.\lambda y.w$
- 因为 $\equiv_\alpha$ 是一个等价关系，所以也叫做Alpha等价。以后，我们将Alpha等价的Lambda项视为恒等的，并且将 $\equiv_\alpha$ 视为 $\equiv$
（Beta化归）将函数的求值视为替换，这对应于Beta化归（Beta Reduction）
$(\lambda x.M)(N) = M[x \mapsto N].$
除了Beta化归以外，我们还有如下的关系
- （等价关系） $=$ 是一个等价关系
- （抽象）如果 $M = N$ ，那么 $\lambda x.M = \lambda x.N$
- （应用）如果 $M = N$ ，那么 $MZ = NZ$ ， $ZM = ZN$