【函数语言程序设计】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 的项。

在构造类型推导树的时候，我们采用自底向上的方式，根据当前被考虑的λ 项的类型，选择并应用唯一一条规则，然后考虑规则前提中的 λ 项，继续往上推导。

如果最后运用的是无前提的规则（即公理），例如（Tv）和（Ts），那么对当前项的类型推导结束，说明我们到达推导树的一个叶子节点。

如果自底向上所有分支都到达叶子节点，则整个推导过程结束，完成这棵推导树的构造。

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中的运行截图

【学习】函数语言程序设计文章被收录于专栏

函数语言程序设计 Coq章节 Ch1 Basics【COQ中的函数编程】 Ch2 Induction【归纳法证明】 Ch3 Lists【使用结构化数据】 Ch4 Poly【多态性与高阶函数】 Ch5 Tactics【更基本的战术】 Ch6 Logic【COQ中的逻辑】 Ch7 IndProp【归纳定义命题】 Ch8 Maps【全图和局部图】 Ch9 Rel【关系的性质】