【函数语言程序设计】3
1.为下面这个类型判断构造一棵推导树。
解析：
我们用记号 M : A 来表示项 M 的类型是 A。
类型规则是通过类型判断（typing judgments）来表述的。
一个类型判断是下面形式的表达式：
x1 : A1, x2 : A2, ..., xn : An ⊢ M : A.
其意义是说，对于 1 和 n 之间的任何 i，假设 xi 的类型是 Ai，那么项 M 是一个良类型的（well typed）项，它的类型是 A。项 M 中出现的自由变量应该被包含在 x1, ..., xn 中。也就是说，在决定项 M 的类型之前，我们必须知道它的所有自由变量的类型。
在类型判断的左边是形如 x1 : A1, ..., xn : An 的假设，称为类型上下文（typing context），其中的每个 xi 都与其它变量不同。我们用希腊字母 Γ 代表任意的类型上下文，用 Γ, Γ′ 和 Γ, x : A 表示类型上下文的拼接，其中涉及的变量名互相不同。如果一个类型上下文 Γ 是空的，其中没有任何变量，我们把 Γ ⊢ M : A 简写为 ⊢ M : A。
下图列出简单类型 λ-演算的类型规则。
规则（Tv）不依赖于任何假设，
它是一条公理。如果在类型上下文中假设 x 的类型是 A，那么项 x 的类型就是 A。
规则（Tap）说明可以把一个类型为 A → B 的函数作用到类型为 A 的参数上，得到的结果具有类型 B。
规则（Tab）告诉我们，如果项 M 的类型是B，其中可能有 A 类型的自由变量 x，那么 λxA.M 是一个类型为 A → B 的函数。
规则（Tp）说明把类型分别为 A 和 B 的两个项组合成一个二元组以后，结果的类型为 A × B。
与之对应的是规则（Tpj1）和（Tpj2）：对类型为 A × B的项进行左投影，得到的项类型为 A，进行右投影得到类型为 B 的项。
规则（Ts）说明 ∗ 是类型为 1 的项。
2.定义一个名为Z2的类型，其中包括两个数据值：zero 和 one ，然后定义Z2上的模2加法，用记号 + 表示，最后证明下面四个等式成立。
Example testAdd1：zero + zero = zero .
Example testAdd2：zero + one = one .
Example testAdd3：one + zero = one .
Example testAdd4：one + one = zero .
Inductive z2:Type:= | zero | one. Definition reverse(x: z2):z2:= match x with | zero => one | one => zero end. Definition add2(a1 a2:z2):z2:= match a1 with | zero => a2 | one => reverse a2 end. Notation "x + y":=(add2 x y). Example testAdd1: zero + zero = zero . Proof. simpl. reflexivity. Qed. Example testAdd2: zero + one = one . Proof. simpl. reflexivity. Qed. Example testAdd3: one + zero = one . Proof. simpl. reflexivity. Qed. Example testAdd4: one + one = zero . Proof. simpl. reflexivity. Qed.
Coq中的运行截图
查看14道真题和解析