简单类型λ演算

简单类型的 lambda 演算 ( λ → {\displaystyle \lambda {\to }} ) 是类型理论的一种形式，是对只有一个类型构造函数 ( → {\displaystyle \to } ) 构建函数类型。 它是类型化 lambda 演算的典型且最简单的示例。 简单类型的 lambda 演算最初是由 Alonzo Church 在 1940 年提出的，目的是避免矛盾地使用无类型的 lambda 演算。

术语简单类型也用于指代简单类型 lambda 演算的扩展，例如乘积、余积或自然数 (System T) 甚至完全递归（如 PCF）。 相反，引入多态类型（如系统 F）或依赖类型（如逻辑框架）的系统不被视为简单类型。 简单类型，除了完全递归，仍然被认为是简单的，因为这种结构的 Church 编码可以只使用 → {\displaystyle \to } 和合适的类型变量来完成，而多态性和依赖性则不能。

在这篇文章中，符号 σ {\displaystyle \sigma } 和 τ {\displaystyle \tau } 用于表示类型范围。 非正式地，函数类型 σ → τ {\displaystyle \sigma \to \tau } 指的是函数类型，给定 σ {\displaystyle \sigma } 类型的输入，产生类型的输出 τ {\displaystyle \tau } 。按照惯例，→ {\displaystyle \to } 关联到右边：σ → τ → ρ {\displaystyle \sigma \to \tau \to \ rho } 读作 σ → ( τ → ρ ) {\displaystyle \sigma \to (\tau \to \rho )} 。

要定义类型，必须首先定义一组基本类型 B {\displaystyle B} 。 这些有时称为原子类型或类型常量。

一组术语常量也为基本类型固定。 例如，它可能假定基类型为 nat，术语常量可以是自然数。 在最初的演示中，Church 仅使用了两种基本类型：o {\displaystyle o} 用于命题类型，ι {\displaystyle \iota } 用于个体类型。 类型 o {\displaystyle o} 没有项常数，而 ι {\displaystyle \iota } 有一个项常数。 通常只考虑一种基本类型的微积分，通常是 o {\displaystyle o} 。

简单类型 lambda 演算的语法本质上是 lambda 演算本身的语法。 术语 x : τ {\displaystyle x{\mathbin {:}}\tau } 表示变量 x {\displaystyle x} 的类型为 τ {\displaystyle \tau } 。

其中 c {\displaystyle c} 是项常量。

即变量引用、抽象、应用和常量。 如果变量引用 x {\displaystyle x} 在抽象绑定 x {\displaystyle x} 内部，则它是绑定的。 如果没有未绑定的变量，则术语是封闭的。

而在类型化 lambda 演算中，每个抽象（即函数）都必须指定其参数的类型。

要定义给定类型的类型良好的 lambda 术语集，我们将定义术语和类型之间的类型关系。

类型关系 Γ ⊢ e : σ {\displaystyle \Gamma \vdash e{\mathbin {:}}\sigma } 表示 e {\displaystyle e} 是类型为 σ {\displaystyle \sigma } 在上下文 Γ {\displaystyle \Gamma } 中。 在这种情况下，e {\displaystyle e} 被认为是类型良好的（具有类型 σ {\displaystyle \sigma } ）。 类型关系的实例称为类型判断。 类型判断的有效性通过提供使用类型规则构建的类型推导来显示（其中线上方的前提允许我们推导出线下方的结论）。