简单类型 λ 演算
简单类型 λ 演算是一种非常简单的类型系统。在本文中,我们将从简单类型 λ 演算的基本性质出发,介绍四个不那么平凡的结果:
- 强正则定理:简单类型 λ 演算中,不存在以有类型的项开始的无限长的 β 规约序列;
- 类型推导算法:对于 Curry 风格(变量不注明类型)的 λ 演算,存在高效的算法求出 λ 项的“主类型”;
- 组合子逻辑:一个仅用 2 个组合子和组合子应用形成的演算系统,不需要任何变量;
- Curry-Howard 同构:简单类型 λ 演算与直觉主义命题逻辑的自然演绎系统对应,简单类型组合子逻辑与直觉主义希尔伯特公理系统对应。