简单类型 λ 演算

关于其它含义, 请参见 “简单类型论”.

简单类型 $\mathbf{\lambda }$ 演算是一种类型论, 记作 ${\lambda }_{\to }$ 或者 STλC, 一般包含函数类型、积类型, 有时也包含不交并和一些其他类型. 在仅包含函数类型和积类型的情况下,${\lambda }_{\to }$ 还是积闭范畴的内语言. 在 Alonzo Church 的 “Russell 简单类型论” [Church 1940] 里是只有函数类型的. ${\lambda }_{\to }$ 和直觉逻辑的对应关系大概如下 (又见: Curry–Howard 对应) :

直觉逻辑	${\lambda }_{\to }$	积闭范畴
命题	类型	对象
真	单位类型	终对象
假	空类型	始对象
蕴涵	函数类型	内态射
证明	实例	从终对象出发的态射
切消除	正规性

由于 ${\lambda }_{\to }$ 也有假命题和命题蕴涵, 因此命题 $p$ 的否定可以定义为 $p\to \perp$, 这样 ${\lambda }_{\to }$ 也能讨论命题的否定、定义双重否定消除和逻辑一致性等概念.

${\lambda }_{\to }$ 的简单之处在于类型和值的语法是独立定义的, 它也是纯类型论的讨论基础. 现代认为与之相对的类型论是 F 系统和依值类型论. 而在古代, 与之相反的是 Russell 简单类型论的前身分歧类型论.

1定义

${\lambda }_{\to }$ 的定义包含语法定义和类型规则, 其中类型规则会用到推导规则、语境、语境无关文法等概念.

函数类型

首先我们考虑只有函数类型的 ${\lambda }_{\to }$, 因为这是任何情况下 ${\lambda }_{\to }$ 都包含的类型. 可以说任何 ${\lambda }_{\to }$ 都是在这个类型论的基础之上扩充的.

定义 1.1 (语法). ${\lambda }_{\to }$ 的语法, 使用语境无关文法描述如下:

$$\begin{array}{rl}A,B& ::=\mathbb{V}\mid A\to B\\ M,N,u,v& ::=V\mid (MN)\mid (\lambda V.M)\end{array}$$

其中,$A,B$ 这两个符号表示类型论中的类型, 而 $M,N,u,v$ 这四个符号都表示类型论中的值 ($\lambda$ 表达式). $V$ 和 $\mathbb{V}$ 分别表示 (可数无穷多个不同的) 变量及类型变量, 一般分别以小写拉丁字母与大写拉丁字母 (强调变量这一性质时可能会倾向于用小写希腊字母) 代替.

用符号 $u$ 代表一个表达式的意思就是这个表达式满足如下三个条件之一:

•	$u\in V$,
•	$u$ 形如 $v_1{v}_2$, 其中 $v_1,v_2$ 是类似 $u$ 的表达式,
•	$u$ 形如 $\lambda x.v$, 其中 $x\in V$, 而 $v$ 是类似 $u$ 的表达式.

对 $A,B$ 等表示类型的符号的描述也类似.

注 1.2. 在 1.1 中, 表示值的符号有大写的 $M,N$ 和小写的 $u,v$. 前者一般用于讨论范畴语义的时候, 因为在这个时候小写字母可能都被用来表示态射了. 后者一般用于只讨论类型论的时候, 可能是因为大写字母看起来还是太大了.

定义 1.3. 在 1.1 中, 称用 $u$ 代表的表达式是良形式的值. 类似地, 称用 $A,B$ 代表的表达式是良形式的类型.

在 ${\lambda }_{\to }$ 中, 良形式的类型就已经是 “完美” 的了, 但良形式的值还不够 “完美”, 需要用类型规则去限制它们.

第一条类型规则是公理规则, 注意这条规则不属于函数类型, 但它却是 ${\lambda }_{\to }$ 中必要的规则:

定义 1.4 (公理规则). $$\frac{(x:\sigma )\in \Gamma }{\Gamma ⊢x:\sigma }$$

然后是函数类型的规则, 这些规则在函数类型中给出:

定义 1.5 (函数类型规则). $$\frac{\Gamma ,x:A⊢u:B}{\Gamma ⊢\lambda x.u:A\to B}\frac{\Gamma ⊢u:A\to B\Gamma ⊢v:A}{\Gamma ⊢\text{ap}(u,v):B}$$

以及值的计算规则 (来源于 $\lambda$ 演算的规约规则) , 这些规则描述了值之间的相等关系:

定义 1.6 (计算规则). $$\begin{array}{rlr}\lambda x.u& \equiv \lambda y.u[x\mapsto y]& (\alpha )\\ (\lambda x.u)v& \equiv u[x\mapsto v]& (\beta )\\ \lambda x.ux& \equiv u& (\eta )\end{array}$$

其中 $u[x\mapsto v]$ 意为将 $u$ 中所有自由 (见 1.8) 出现的变量 $x$ 替换为 $v$, 这一操作在下文中有更详细的讨论. 另外 $\eta$ 规则中要求 $x$ 在 $u$ 中是自由变量.

注 1.7 (语义正规性). 在 1.6 描述计算规则时, 使用了表示等价的符号 $\equiv$, 但在部分 (更早期的) 文献中也会使用类似 $⟶$ 等箭头符号来表示计算的过程, 这些文献往往站在 $\lambda$ 演算的视角将类型论看作是一种重写系统, 认为计算规则是在对值进行单向的、从繁到简的改写, 就像一个符号计算器一样. 现代有部分观点认为值的计算规则仅表达值的二元相等关系, 它仅用于定义一个等价类, 而这个单向的改写过程则并不存在, 或者说存在但不重要.

使用这种视角, 可以讨论正规性.

定义 1.8. 如果某个 $x$ 出现在 $\lambda x.M$ 的 $M$ 中, 就称其是绑定变量. 反之称其为自由变量.

注 1.9. 很多时候会省略 $\alpha$ 规则, 因为它想传递的思想几乎是平凡的, 但是形式化定义起来却很繁琐. 例如 $(\lambda x.\lambda y.yx)y{\equiv }^{\beta }\lambda z.zy$ 成立, 但 $(\lambda x.\lambda y.yx)y{\equiv }^{\beta }\lambda y.yy$ 不成立. 后者使一个原本自由出现的 $y$ 变成了绑定变量.

注 1.10. 有时会不采用 $\eta$ 规则.

上述三组规则构成了 ${\lambda }_{\to }$.

积类型

接下来我们对 ${\lambda }_{\to }$ 进行简单的扩展, 加入积类型.

定义 1.11 (语法). 若要添加积类型, 则需将 1.1 中的语法扩充为: $$\begin{array}{rl}\mathbb{T}& ::=\mathbb{V}\mid A\to B\mid A\times B\\ M,N,u,v& ::=V\mid (MN)\mid (\lambda V.M)\mid ⟨M,N⟩\mid M.1\mid M.2\end{array}$$

并加入积类型对应的构造与消去规则, 这些规则在积类型中有列出, 这里就略过了.

替换操作

主条目: 替换操作

在 ${\lambda }_{\to }$ 中, 我们用 $u[x\mapsto v]$ 这个记号来表示把值 $u$ 中对变量 $x$ 的引用替换成 $v$ 的操作, 这个操作被称为替换. 有时我们还会同时进行多组替换, 比如 $u[x_0\mapsto v_0,x_1\mapsto v_1]$ 等. 假设 $\Gamma ⊢u:A$, 那么如果把 $\Gamma$ 里的全部变量都替换掉 (按顺序替换为一组新值, 这一组值一般记作 $\sigma$), 得到的新值就不再会属于 $\Gamma$ 这个语境了, 而是会属于 $\sigma$ 里面的值所在的语境.

假设这个语境叫 $\Delta$, 那么我们用如下记号来描述 $\sigma$:

$$\Delta ⊢\sigma :\Gamma$$

这表示 $\sigma$ 里的值来自 $\Delta$, 并且这一组值按顺序属于 $\Gamma$ 里的类型 (这也是为什么 $\sigma$ 里的值可以用来替换掉 $\Gamma$ 里的变量, 因为它们的类型是匹配的) .

由于在讨论 $u$ 时我们已经给出了它所在的语境, 这个语境提供了我们进行替换操作时用到的变量名, 所以直接使用 $u\sigma$ 这样的语法来描述对 $u$ 的替换操作也是不会损失信息的. 我们可以用如下规则形式化描述替换操作:

$$\frac{\Delta ⊢\sigma :\Gamma \Gamma ⊢u:A}{\Delta ⊢u\sigma :A}$$

换言之, 仅观察类型的话, 替换操作是从一个特定语境里, 把任意值带到另一个语境的操作. 在这个视角下, 替换操作又叫语境态射.

2性质

在仅包含函数类型和积类型的情况下,${\lambda }_{\to }$ 拥有很多性质. 这些性质中很多在依值类型论里特别难以证明, 但在 ${\lambda }_{\to }$ 里面很简单.

•	${\lambda }_{\to }$ 的类型规则满足典范性、正规性.
•	${\lambda }_{\to }$ 的计算满足合流性, 而在 ${\lambda }_{\to }$ 里这一性质又称 Church–Rosser 定理.
•	${\lambda }_{\to }$ 满足一致性, 但实际上讨论这件事之前我们先需要给 ${\lambda }_{\to }$ 加入空类型.
•	${\lambda }_{\to }$ 里的类型和值可以分别被解释为积闭范畴里的对象和态射, 参考 Curry–Howard–Lambek 对应.

3参考文献

•	Alonzo Church (1940). “A Formulation of the Simple Theory of Types”. The Journal of Symbolic Logic 5 (2), 56–68. (web)

术语翻译

简单类型 $\lambda$ 演算 • 英文 simply typed $\lambda$ calculus • 法文 calcul lambda simplement typé

良形式 (形容词) • 英文 well-formed • 法文 bien formé • 拉丁文 beneformis • 古希腊文 εὔμορφος