简单类型λ演算

简单类型 lambda 演算()是连接词只有 (函数类型)的 有类型 lambda 演算。这使它成为规范的、在很多方面是最简单的有类型 lambda 演算的例子。

简单类型也被用来称呼对简单类型 lambda 演算的扩展比如 、 陪积或 自然数(系统 T)甚至完全的 递归(如 PCF)。相反的,介入了多态类型(如 系统F)或依赖类型(如 逻辑框架)的系统不被当作是简单类型。简单类型 lambda 演算最初由 阿隆佐·邱奇在 1940 年介入来尝试避免 无类型 lambda 演算的悖论性使用。

类型

简单类型 lambda 演算的类型构造自基本类型(或类型变量),给定类型 我们能构造 。邱奇只使用了两个基本类型, 是命题的类型, 是个体的类型。这种演算经常只有一个基本类型,通常考虑为

是右结合的: 我们读 。对每个类型 我们指派一个数字 ,它是 的阶。对于基本类型,我们设置 ,而对于函数类型我们递归的定义