类型化算术表达式与简单类型lambda演算入门

### 类型化算术表达式与简单类型 lambda 演算入门 #### 1. 类型化算术表达式 在之前对布尔和算术表达式的研究基础上，我们为其引入静态类型。这个类型系统虽然简单，但能帮助我们引入后续会反复用到的概念。 ##### 1.1 类型 算术表达式的语法如下： ```plaintext t ::= terms: true constant true false constant false if t then t else t conditional 0 constant zero succ t successor pred t predecessor iszero t zero test ``` 值的语法为： ```plaintext v ::= values: true true value false false value nv numeric value nv ::= numeric values: 0 zero value succ nv successor value ``` 在评估表达式时，可能会得到一个值，也可能会陷入“卡住”的状态，比如遇到 `pred false` 这样没有适用评估规则的情况。为了在不实际评估的情况下判断一个表达式是否会卡住，我们引入了 `Nat` 和 `Bool` 两种类型。 说“一个项 `t` 具有类型 `T`”，意味着 `t` 显然会评估为一个合适形式的值，这里的“显然”是指我们可以在不进行评估的情况下静态地判断。例如，`if true then false else true` 具有类型 `Bool`，而 `pred (succ (pred (succ 0)))` 具有类型 `Nat`。不过，我们对项类型的分析是保守的，仅使用静态信息，所以像 `if (iszero 0) then 0 else false` 这样的项，即使评估不会卡住，我们也无法确定其类型。 ##### 1.2 类型关系 算术表达式的类型关系用 “`t : T`” 表示，由一组推理规则定义，这些规则总结在图 8 - 1 和图 8 - 2 中。 **布尔类型规则（图 8 - 1）**： | 规则 | 描述 | | ---- | ---- | | `true : Bool` (T - True) | 布尔常量 `true` 具有类型 `Bool` | | `false : Bool` (T - False) | 布尔常量 `false` 具有类型 `Bool` | | `t1 : Bool, t2 : T, t3 : T => if t1 then t2 else t3 : T` (T - If) | 条件表达式的守卫 `t1` 必须评估为布尔值，`t2` 和 `t3` 必须评估为相同类型的值，结果类型为 `T` | **数字类型规则（图 8 - 2）**： | 规则 | 描述 | | ---- | ---- | | `0 : Nat` (T - Zero) | 常量 `0` 具有类型 `Nat` | | `t1 : Nat => succ t1 : Nat` (T - Succ) | 若 `t1` 具有类型 `Nat`，则 `succ t1` 具有类型 `Nat` | | `t1 : Nat => pred t1 : Nat` (T - Pred) | 若 `t1` 具有类型 `Nat`，则 `pred t1` 具有类型 `Nat` | | `t1 : Nat => iszero t1 : Bool` (T - IsZero) | 若 `t1` 具有类型 `Nat`，则 `iszero t1` 具有类型 `Bool` | 形式上，算术表达式的类型关系是满足图 8 - 1 和图 8 - 2 中所有规则实例的项和类型之间的最小二元关系。如果存在某个 `T` 使得 `t : T`，则称项 `t` 是可类型化的（或类型良好的）。 下面是一些关于类型关系的引理： - **引理（类型关系的反转）**： 1. 如果 `true : R`，那么 `R = Bool`。 2. 如果 `false : R`，那么 `R = Bool`。 3. 如