无类型 lambda 演算

无类型 $\mathbf{\lambda }$ 演算, 又名单一类型 $\mathbf{\lambda }$ 演算, 就是所有值都共用同一个类型的 $\lambda$ 演算, 这个唯一的类型常常被忽视, 因此被称为 “无类型”.

传统的 $\lambda$ 演算研究中有诸多类似于 $\alpha$ 等价、$\beta$ 规约、“避免捕获的替换” 等不必要的概念, 在现代的视角下这些概念可以通过性质更好的 De Bruijn 编号、正规性等手段消除.

1定义

参见: 变量

定义 1.1. $\mathbf{\lambda }$ 演算的语法由语境无关文法定义如下: $$M,N::=x\mid (\lambda x.M)\mid MN$$其中 $x$ 代表任意变量名, 可以规定任何一个可数无穷大的集合, 然后从这个集合中取变量名.

例子: $(\lambda x.\lambda y.(\lambda z.(\lambda x.zx)(\lambda y.zy))(xy))$. 在无歧义的情况下括号可省略.

定义 1.2. 对于 $\lambda$ 演算中的表达式 $M$, 它里面的自由变量 $FV(M)$ 定义为如下集合: $$\begin{array}{rl}FV(x)& ::=\{x\}\\ FV(MN)& ::=FV(M)\cup FV(N)\\ FV(\lambda x.M)& ::=FV(M)\setminus \{x\}(这种情况下x被称为\text{绑定变量})\end{array}$$若 $FV(M)=\varnothing$ 那么称 $M$ 为闭的.

等价关系

参见: 替换操作

$\lambda$ 演算中的表达式在如下几种情况下等价:

•	$\alpha$ 等价: 绑定变量在不影响其它绑定变量和自由变量的情况下可以任意重命名.
•	$\beta$ 等价: $(\lambda x.M)N=M[x\mapsto N]$, 见替换操作.
•	$\eta$ 等价. 对于变量 $f$, $\lambda x.fx=f$.

2语义

参见: 论域理论

无类型 $\lambda$ 演算的语义的核心就是在简单类型 $\lambda$ 演算的基础上, 加入如下类型同构关系:$$(T\to T)\simeq T$$这对于集合来说是不可能的, 因此无类型 $\lambda$ 演算里的表达式只能被解释到一些其它数学对象中. 论域就是其中一种.

范畴语义

(...)

3递归论意义

无类型 $\lambda$ 演算和 Turing 机的计算能力等价: 它可以表达自然数 (见: $\lambda$ 编码) 和带条件的循环 (见: $Y$ 组合子). 尽管如此, $\lambda$ 演算强调的是映射之间的交互, 而不是具体的计算过程.

关于无类型 $\lambda$ 演算的推广, 参见部分组合代数.

术语翻译

单一类型 $\lambda$ 演算 • 英文 unityped $\lambda$ calculus

规约 • 英文 reduction

避免捕获的替换 • 英文 capture-avoiding substitution