Curry-Howard同构讲义

前言

Curry-Howard同构, 也被称为"命题作为类型"范式, 陈述了形式逻辑系统与计算性演算之间惊人的联系. 它自这样的观察开始, 一个推论 $A \to B$ 与一类从 $A$ 到 $B$ 的函数有关 [译注: 这里强调的是一个推论和一类有关, 一类也就是一个类型], 因为从 $A \to B$ 和 $A$ 推出 $B$ 可以被视为将第一个假设应用于第二个, 正如将一个从 $A$ 到 $B$ 的函数应用于 $A$ 的一个元素产生 $B$ 的一个元素. 类似地, 可以说通过实际从 $B$ 推出 $A$ 来证明推论 $A \to B$ 就像构造一个函数, 其将定义域 $A$ 的任意元素都映射至 $B$ 的元素.

实际上, 这是一个很老的想法了, 应该归功于Brouwer, Kolmogorov和Heyting, 即从 $A$ 到 $B$ 的推论的一个构造性证明, 是一个将 $A$ 的证明变换为 $B$ 的证明的过程. Curry-Howard同构形式化了这个想法, 例如命题直觉主义逻辑中的证明可以被表示为简单类型 $λ$ 项. 可证明的定理不外乎是非空类型.

这种类比, 最初由Haskell Brooks Curry于1930年代发现, 也适用于其他的逻辑系统. 似乎所有和证明相关的概念都可以基于计算来解释, 而各种lambda演算和相近系统的一切句法特征都可以用证明论的语言来陈述. 例如, 谓词逻辑中的量化对应于依赖积, 二阶逻辑与多态有关, 而古典逻辑中的反证法是控制运算符 (例如异常) 的近亲. 而且, 各种逻辑形式化 (Hilbert风格, 自然演绎, 相继式演算) 可由相对应的计算模型 (组合子逻辑, $λ$ 演算, 显式替换演算) 来模拟.

自William Howard的1969年的工作起人们理解到这种命题作为类型的对应不仅仅是意外得来的珍品, 而且是一种根本性的原理. 证明正规化和切消是另一种计算的模型, 等价于 $β$ 规约. 证明论和计算理论不过是一体两面而已.

第1章无类型 $λ$ 演算

$λ$ 演算是一种计算的模型, 它在另一种这样的模型Turing机器出现数年之前被发明出来. 对于后者而言, 计算被表达为读写纸带, 以及根据纸带的内容施行操作. Turing机器就像命令式语言 (比如Java或C) 的程序.
与之相对地, 在 $λ$ 演算中, 人们关心函数, 而函数可以将函数作为参数, 以及返回函数作为结果. 用编程的术语来说, $λ$ 演算是一个极其简单的高阶函数式编程语言.
本章我们只讨论无类型 $λ$ 演算, 之后我们将引入诸多变体, 其中 $λ$ 项被归为各种类型.

第1.1节温和的引入

在 $λ$ 演算之中计算以 $λ$ 项表达. 它们类似于数学中使用的匿名函数记号 $n \mapsto n^{2}$ . 然而, 数学家使用这样的记号来指称作为数学对象的函数 (被定义为序对的集合). 与之相对地, $λ$ 项是形式表达式 (字符串), 从直觉上说, 以最纯粹的形式表达了函数和函数的应用. 因此, 一个 $λ$ 项是如下形式之一:

一个变量;
一个抽象 $λ x M$ , 其中 $x$ 是一个变量, $M$ 是一个 $λ$ 项;
一个应用 $M N$ ( $M$ 应用于 $N$ ), 其中 $M$ 和 $N$ 是 $λ$ 项.

在一个抽象

λ x M

中, 变量

x

代表函数参数 (或者说形式参数), 它可能出现在函数的体

M

之中, 但不必总是如此. 在一个应用

M N

之中, 运算符

M

和参数

N

的形状没有限制, 它们都可以是任意的

λ

项.

举个例子, $λ$ 项 $I = λ x x$ 从直觉上表示了一个将任意的参数映射至自身的函数, 即恒等函数. 再举一个, $K = λ x λ y x$ 代表了这样的一个函数, 其将任意的参数 $x$ 映射至总是返回 $x$ 的常函数. 最后一个例子, $I K$ 表达了将函数 $I$ 应用于参数 $K$ .

在数学中, 我们通常将函数应用的参数写在括号里, 例如若函数是 $f$ , 参数是 $4$ , 那么就记成 $f (4)$ . 在 $λ$ 演算中, 我们则会将其记成 $f 4$ . 尽管如此, 括号的运用并不能被完全消除. 例如, 记号 $λ x x y$ 是有歧义的. 如果我们想要表达的是将 $I$ 应用于 $y$ , 那么就应该写成 $(λ x x) y$ . 或者, 可以用 $λ x (x y)$ 来表示一个 $x$ 上的抽象, 其体为 $x y$ . 后一种情况下, 按照惯例是使用点记号的, 即写作 $λ x . x y$ . 类似地, 我们也需要使用括号来消除应用的歧义. 例如, $I (K K)$ 表达了将 $I$ 应用于 $K K$ .

如果 $λ x M$ 代表一个函数, $N$ 代表一个参数, 那么应用 $(λ x M) N$ 的"值"可以通过将 $M$ 中的 $x$ 替换为 $N$ 计算得到. 这样一个替换的结果以 $M [x ≔ N]$ 表示, 而我们可以用 $β$ 规约规则来形式化这个计算: $(λ x M) N \to_{β} M [x ≔ N]$ . 例如, $(I K) z = ((λ x x) K) z \to_{β} x [x ≔ K] z = K z = (λ y λ x y) z \to_{β} λ x z .$ 这个计算表达式的值的过程与通常的数学实践是类似的. 如果 $f (n) = n^{2}$ , 那么 $f (4) = 4^{2}$ , 并且我们是通过在 $f$ 定义的体中将 $n$ 替换为 $4$ 从应用 $f (4)$ 得到结果 $4^{2}$ 的. 编程语言上的类比即按名调用的参数传递机制, 其中过程的形式参数被全部替换以实际的参数表达式.

一个 $λ$ 抽象 $λ x M$ 中的变量 $x$ 在 $M$ 中被绑定 (或者说局部于), 就非常类似于一个过程的形式参数被认为局部于该过程. 与之相对的是, 一个变量 $y$ , 若没有与其对应的抽象, 则被称为自由的 (或者全局的), 这就类似于大多数编程语言中的全局变量. 因此, 在 $λ x . x y$ 之中, $x$ 是绑定的, 而 $y$ 是自由的.

当绑定变量和自由变量重名时会引起一些混乱. 例如, 在 $x (λ x . x y)$ 中, 显然有两个不同的 $x$ : 自由的 (全局的) $x$ 和绑定的 (局部的) $x$ , 绑定的 $x$ "遮住了"体内自由的 $x$ . [译注: 换言之, 若体内的 $x$ 没有 $λ$ 绑定的包裹, 则会是一个自由变量.] 若我们转而考虑 $λ$ 项 $x (λ z . z y)$ , 那就没有歧义了. 再举另外一种引起混乱的例子, $(λ x . x y) [y ≔ x]$ 应该将 $(λ x . x y)$ 中的 $y$ 替换为自由变量 $x$ , 但是 $λ x . x x$ 并非预期的结果. 在后一个项中, 我们失去了形式参数 $x$ 和自由变量 $x$ 之间的区别 (自由变量已被lambda捕获). 如果我们使用一个绑定变量 $z$ , 那么混乱就消失了: $(λ z . z y) [y ≔ x] = λ z . z x$ .

过程的局部变量总可以被换名而不影响程序的含义. 类似地, 在 $λ$ 演算中我们也不在乎绑定变量的名字. $λ$ 项 $λ x x$ 和 $λ y y$ 都代表着恒等函数. 正因如此, 通常假定只有绑定变量不同的项是等同的. 这给了我们选取绑定变量以避免混乱 (比如说变量捕获) 的自由.

第1.2节预项和 $λ$ 项

现在我们定义预项的概念, 并将 $λ$ 项作为预项的等价类引入. 本节相当乏味, 但对于使得我们的形式化精确而言是必要的. 然而, 为了理解本书的大部分内容, 前一节对于 $λ$ 项的非形式化理解就足够了.

1.2.1. 定义. 令

Υ

代表一个可数无穷的符号集合, 之后就将其称为变量 (当其他种类的变量可能造成歧义的时候, 也将其称为对象变量或者

λ

变量). 我们通过归纳定义预项的概念如下:

每个变量都是一个预项.
如果 $M$ , $N$ 是预项, 那么 $(M N)$ 也是一个预项.
如果 $x$ 是一个变量而 $M$ 是一个预项, 那么 $(λ x M)$ 也是一个预项.

所有预项构成的集合记作

Λ^{-}

评注. 这个定义可以被总结为以下语法:

M ⩴ x | (M M) | (λ x M) .

在本书的剩余部分里, 我们将时常使用这种简短的定义风格.

预项, 正如上面所定义的那样, 是完全括号化的. 如预项 $(λ f ((λ u (f (u u))) (λ v (f (v v)))))$ 所呈现的, 括号的重度使用是相当笨拙的. 因此, 我们引入一些记号上的约定, 每当不致引起歧义时我们非正式地使用它们.

1.2.2. 约定.

一个项最外部的括号被省略.
应用向左结合: $((P Q) R)$ 被缩略为 $(P Q R)$ .
抽象向右结合: $(λ x (λ y P))$ 被缩略为 $(λ x λ y P)$ .
一个抽象的序列 $(λ x_{1} (λ x_{2} \dots (λ x_{n} P) \dots))$ 可以被记成 $(λ x_{1} x_{2} \dots x_{n} . P)$ , 在这种情形之下 $P$ 最外面的括号 (如果有的话) 通常被省略. [原注: 这个点代表了一个辖域尽可能向右延伸的左括号.]

例子.

根据i, $(λ v (v v))$ 可以被缩略为 $λ v (v v)$ .
根据i和ii, $(((λ x x) (λ y y)) (λ z z))$ 可以被缩略为 $(λ x x) (λ y y) (λ z z)$ .
根据i和iii, $(λ x (λ y (x y)))$ 被记为 $λ x λ y (x y)$ , 或者根据i和iv记作 $λ x y . x y$ .
$(λ f ((λ u (f (u u))) (λ v (f (v v)))))$ 记作 $λ f . (λ u . f (u u)) (λ v . f (v v))$ .

1.2.3. 定义. 定义

M

的自由变量的集合

FV (M)

如下.

\begin{array}{l} FV (x) & = & {x}; \\ FV (λ x P) & = & FV (P) - {x}; \\ FV (P Q) & = & FV (P) \cup FV (Q) . \end{array}

例子. 令

x, y, z

是不同的变量, 那么

FV ((λ x x) (λ y . x y z)) = {x, z}

. 这里有两种

x

的出现: 一个在

λ x

下, 一个在

λ y

下.

M

中一个

x

的出现被称为绑定的, 如果它在形状为

λ x L

的

M

的一部分中, 反之则被称为自由的. 于是,

x \in FV (M)

当且仅当

M

中存在

x

的一个自由出现.

1.2.4. 定义. 将

M

中的

x

替换为

N

, 记作

M [x ≔ N]

, 是有定义的当且仅当不存在

M

中

x

的自由出现满足其在形式为

λ y L

的

M

的一部分中, 并且

y \in FV (N)

. [译注: 直觉就是

N

中的自由变量不能被

y

捕获.] 在这样的情况下,

M [x ≔ N]

由下列等式给出:

\begin{matrix} x [x ≔ N] & = & N; \\ y [x ≔ N] & = & y, 如果 x \neq y; \\ (P Q) [x ≔ N] & = & P [x ≔ N] Q [x ≔ N]; \\ (λ x P) [x ≔ N] & = & λ x P; \\ (λ y P) [x ≔ N] & = & λ y P [x ≔ N], 如果 x \neq y . \end{matrix}

[原注: 在我们的元记号中, 替换绑定得比其他任何东西都要强, 所以说在第三行, 最右边的替换是应用于

Q

的, 而不是应用于

P [x ≔ N] Q

的. (译注: 补充说一句, 真要是后一种情况, 那这个定义是否良定都很可疑了, 因为

P [x ≔ N] Q

不比

P Q

小.)]
[译注: 读者应该注意到在这个定义里, 如果

(P Q) [x ≔ N]

有定义, 那么

P [x ≔ N]

和

Q [x ≔ N]

也就有定义, 并且如果

(λ y P) [x ≔ N]

有定义, 其中

x \neq y

, 那么

P [x ≔ N]

也就有定义. 否则的话, 替换就不是良定的了.]

评注. 在最后一行,

y \notin FV (N)

或者

x \notin FV (P)

1.2.5. 引理.

如果 $x \notin FV (M)$ , 那么 $M [x ≔ N]$ 有定义, 并且 $M [x ≔ N] = M$ .
如果 $M [x ≔ N]$ 有定义, 那么 $y \in FV (M [x ≔ N])$ 当且仅当要么 $y \in FV (M)$ 且 $x \neq y$ , 要么 $y \in FV (N)$ 且 $x \in FV (M)$ .
替换 $M [x ≔ x]$ 有定义, 且 $M [x ≔ x] = M$ .
如果 $M [x ≔ y]$ 有定义, 那么 $M [x ≔ y]$ 与 $M$ 拥有相同的长度.

证明. 在

M

上施行归纳. 作为例子, 我们细致地证明i. 显然

M [x ≔ N]

是有定义的. 为了证明

M [x ≔ N] = M

我们考虑以下情形. 如果

M

是一个变量

y

, 那么必有

y \neq x

, 并且

y [x ≔ N] = y

. 如果

M = P Q

, 那么

x \notin FV (P)

且

x \notin FV (Q)

, 于是根据归纳假设有

P [x ≔ N] = P

且

Q [x ≔ N] = Q

, 因此

(P Q) [x ≔ N] = P [x ≔ N] Q [x ≔ N] = P Q

. 最后, 如果

M

是一个抽象, 要么

M = λ x P

要么

M = λ y P

, 其中

x \neq y

. 在前一种情况下,

(λ x P) [x ≔ N] = λ x P

. 在后一种情况下, 我们有

x \notin FV (P)

, 于是根据归纳假设,

(λ y P) [x ≔ N] = λ y P [x ≔ N] = λ y P

◻

1.2.6. 引理. 假定

M [x ≔ N]

是有定义的, 并且

N [y ≔ L]

和

M [x ≔ N] [y ≔ L]

也都是有定义的, 其中

x \neq y

. 如果

x \notin FV (L)

或者

y \notin FV (M)

, 那么

M [y ≔ L]

是有定义的,

M [y ≔ L] [x ≔ N [y ≔ L]]

也是有定义的, 并且

M [x ≔ N] [y ≔ L] = M [y ≔ L] [x ≔ N [y ≔ L]] .

证明.

◻

1.2.7. 引理.

1.2.8. 定义. 关系

=_{α}

(

α

变换) 是

Λ^{-}

上满足下列条件的最小的传递自反关系:

如果 $y \notin FV (M)$ 并且 $M [x ≔ y]$ 有定义, 那么 $λ x M =_{α} λ y . M [x ≔ y]$ .
如果 $M =_{α} N$ , 那么对于所有的变量 $x$ , $λ x M =_{α} λ x N$ .
如果 $M =_{α} N$ , 那么 $M Z =_{α} N Z$ .
如果 $M =_{α} N$ , 那么 $Z M =_{α} Z N$ .

[译注: 后三条是在说

=_{α}

是一个兼容关系.]

例子. 令

x, y

是不同的变量, 那么

λ x y . x y =_{α} λ y x . y x

, 但是

λ x . x y \neq_{α} λ y . y x

1.2.9. 引理.

α

变换的关系是一个等价关系.

1.2.10. 引理. 如果

M =_{α} N

, 那么

FV (M) = FV (N)

证明.

◻

定义1.2.14. 定义

λ

项的集合

Λ

为

=_{α}

的商集:

Λ = {{[M]}_{α} | M \in Λ^{-}},

其中

{[M]}_{α} = {N \in Λ^{-} | M =_{α} N}

例子.

定义1.2.15. 一个

λ

项

M

的自由变量

FV (M)

定义如下. 令

M = {[M^{'}]}_{α}

, 那么

FV (M) = FV (M^{'}) .

如果

FV (M) = \emptyset

, 那么就称

M

是封闭的或者它是一个组合子.
引理1.2.10确保了任何对于

M^{'}

的选择都会产生相同的结果.

定义1.2.16.

记号1.2.17.

引理1.2.18. 以下等式是合理的:

\begin{array}{l} FV (x) & = & {x}; \\ FV (λ x P) & = & FV (P) - {x}; \\ FV (P Q) & = & FV (P) \cup FV (Q) . \end{array}

引理1.2.19.

引理1.2.20.

定义1.2.21.

第1.3节规约

1.3.1. 定义. 一个

Λ

上的关系

≻

是兼容的当且仅当它对于所有的

M, N, Z \in Λ

满足下列条件.

对于所有的变量 $x$ , 如果 $M ≻ N$ , 那么 $λ x M ≻ λ x N$ .
如果 $M ≻ N$ , 那么 $M Z ≻ N Z$ .
如果 $M ≻ N$ , 那么 $Z M ≻ Z N$ .

[译注: 兼容的直觉就是上下文中的关系.]

1.3.2. 定义.

Λ

上满足

(λ x . P) Q \to_{β} P [x ≔ Q]

的最小兼容关系

\to_{β}

被称为

β

规约. 具有形式

(λ x P) Q

的项被称为

β

可规约项, 而

P [x ≔ Q]

被称为是由收缩这个可规约项产生的. 一个项

M

是

β

规范形式 (记号

M \in {NF}_{β}

) 当且仅当不存在这样的

N

满足

M \to_{β} N

, 即

M

并不包含一个

β

可规约项.

1.3.3. 定义.

关系 $↠_{β}$ (多步 $β$ 规约) 是 $\to_{β}$ 的传递且自反闭包. $\to_{β}$ 的传递闭包记作 $\to_{β}^{+}$ .
关系 $=_{β}$ (被称为 $β$ 等价或者 $β$ 变换) 是包含 $\to_{β}$ 的最小等价关系.
一个 $β$ 规约序列是一个有限或无限的序列 $M_{0} \to_{β} M_{1} \to_{β} M_{2} \to_{β} \dots$

1.3.4. 评注.

例子1.3.5.

$(λ x . x x) (λ z z) \to_{β} (x x) [x ≔ λ z z] = (λ z z) (λ y y)$ .
$(λ z z) (λ y y) \to_{β} z [z ≔ λ y y] = λ y y$ .
$(λ x . x x) (λ z z) ↠_{β} λ y y$ .
$(λ x x) y z =_{β} y ((λ x x) z)$ .

例子1.3.6. (一些常见的 $λ$ 项).

令 $I = λ x x$ , $K = λ x y . x$ 以及 $S = λ x y z . x z (y z)$ , 那么 $S K K ↠_{β} I$ .
令 $ω = λ x . x x$ 以及 $Ω = ω ω$ , 那么 $Ω \to_{β} Ω \to_{β} Ω \to_{β} \dots$ .
令 $Y = λ f . (λ x . f (x x)) (λ x . f (x x))$ , 那么 $Y \to_{β} Y^{'} \to_{β} Y^{″} \to_{β} \dots$ , 其中 $Y, Y^{'}, Y^{″}, \dots$ 各不相同.

评注1.3.7.

引理1.3.8.

定义1.3.9.

命题1.3.10. 令

=_{ext}

是满足下列条件的最小关系:

如果 $M =_{β} N$ , 那么 $M =_{ext} N$ ;
如果 $M x =_{ext} N x$ 且 $x \notin FV (M) \cup FV (N)$ , 那么 $M =_{ext} N$ ;
如果 $P =_{ext} Q$ , 那么 $P Z =_{ext} Q Z$ 且 $Z P =_{ext} Q P$ .

那么,

M =_{ext} N

当且仅当

M =_{β η} N

. [译注:

=_{ext}

即所谓的外延相等的概念.]

证明.

◻

引理1.3.11.

第1.4节 Church-Rosser定理

既然一个 $λ$ 项 $M$ 可能包含数个 $β$ 可规约项, 那么可能存在多个 $N$ 满足 $M \to_{β} N$ . 例如, $K (I I) \to_{β} λ x . I I$ 和 $K (I I) \to_{β} K I$ .

定义1.4.1. 令

\Rightarrow_{β}

是满足下列条件的

Λ

上的最小关系:

对于所有变量 $x$ , $x \Rightarrow_{β} x$ .
如果 $P \Rightarrow_{β} Q$ , 那么 $λ x . P \Rightarrow_{β} λ x . Q$ .
如果 $P_{1} \Rightarrow_{β} Q_{1}$ 且 $P_{2} \Rightarrow_{β} Q_{2}$ , 那么 $P_{1} P_{2} \Rightarrow_{β} Q_{1} Q_{2}$ .
如果 $P_{1} \Rightarrow_{β} Q_{1}$ 且 $P_{2} \Rightarrow_{β} Q_{2}$ , 那么 $(λ x . P_{1}) P_{2} \Rightarrow_{β} Q_{1} [x ≔ Q_{2}]$ .

引理1.4.2.

如果 $M \to_{β} N$ , 那么 $M \Rightarrow_{β} N$ .

证明.

◻

定义1.4.3. 令

M^{⁎}

(

M

的complete development) 定义为:

\begin{array}{l} x^{⁎} & = & x; \\ {(λ x M)}^{⁎} & = & λ x M^{⁎}; \\ {(M N)}^{⁎} & = & M^{⁎} N^{⁎}, 如果 M 不是一个抽象; \\ {((λ x M) N)}^{⁎} & = & M^{⁎} [x ≔ N^{⁎}] . \end{array}

第1.5节最左规约是正规化

定义1.5.1. 一个项

M

是正规化的 (记号

M \in {WN}_{β}

) 当且仅当存在一个从

M

开始的规约序列终于正规形式

N

, 那么我们称

M

有正规形式

N

. 一个项

M

是强正规化的 (

M \in {SN}_{β}

或者仅仅

M \in SN

) 如果从

M

开始的规约序列都是有限的. 如果

M \notin {SN}_{β}

, 那么我们记

M \in \infty_{β}

. 类似的记号也用于其他规约概念.

任何强正规化的项也是正规化的, 反之则不然, 如 $K I Ω$ . 但是, 定理1.5.8陈述了一个正规形式, 如果存在的话, 总是可由重复规约最左可规约项得到, 最左可规约项即其 $λ$ 向左走得最远的可规约项. 以下记号和定义对于证明定理1.5.8而言是方便的.

向量记号. 令 $n \geq 0$ . 如果 $\vec{P} = P_{1}, \dots, P_{n}$ , 那么我们记 $M P_{1} \dots P_{n}$ 为 $M \vec{P}$ . 特别地, 如果 $n = 0$ , 即 $\vec{P}$ 为空, 那么 $M \vec{P}$ 就是 $M$ . 类似地, 如果 $\vec{z} = z_{1}, \dots, z_{n}$ , 那么我们记 $λ z_{1} \dots z_{n} . M$ 为 $λ \vec{z} . M$ . 又一次, 如果 $n = 0$ , 即 $\vec{z}$ 为空, 那么 $λ \vec{z} . M$ 就是 $M$ .

评注. 任何项都恰具有以下两种形式之中的一种:

λ \vec{z} . x \vec{R}

或者

λ \vec{z} . (λ x P) Q \vec{R}

, 在后一种情况下

(λ x P) Q

被称为头部可规约项 (在前一种情况下, 不存在头部可规约项).

定义1.5.2. 对于不是正规形式的项

M

, 我们记

$M {\overset{l}{\to}}_{β} N$ 如果 $N$ 是通过 $M$ 收缩最左可规约项得到的.
$M {\overset{h}{\to}}_{β} N$ 如果 $N$ 是通过 $M$ 收缩头部可规约项得到的.
$M {\overset{i}{\to}}_{β} N$ 如果 $N$ 是通过 $M$ 收缩内部可规约项得到的.

引理1.5.3.

如果 $M {\overset{h}{\to}}_{β} N$ , 那么 $λ x M {\overset{h}{\to}}_{β} λ x N$ .

定义1.5.4.

第1.6节永恒规约和守恒定理

第1.7节可表达性和不可判定性

无类型 $λ$ 演算是如此之简单, 以至于它的强大是令人惊讶的. 本节我们将展示实际上 $λ$ 演算可以被视为递归论的另一种形式化.

我们可以使用 $λ$ 项表示各种各样的构造, 例如真值: $true = λ x y . x; false = λ x y . y; if P then Q else R = P Q R .$ 很容易看出来 $if true then P else Q ↠_{β} P; if false then P else Q ↠_{β} Q .$ 另一种有用的构造是序对 $\begin{matrix} ⟨ M, N ⟩ & = & λ x . x M N \\ π_{1} & = & λ p . p (λ x y . x) \\ π_{2} & = & λ p . p (λ x y . y) \end{matrix}$ 正如所期望的我们有 $π_{i} ⟨ M_{1}, M_{2} ⟩ ↠_{β} M_{i}$

定义1.7.1. 在

λ

中我们可以将自然数表示为Church数码:

c_{n} = λ f x . f^{n} (x)

其中

f^{n} (x)

是

f (f (\dots (x) \dots))

的缩略形式,

f

出现了

n

次. 有时我们将

c_{n}

记成

n

, 于是

\begin{matrix} 0 & = & λ f x . x \\ 1 & = & λ f x . f x \\ 2 & = & λ f x . f (f x) \end{matrix}

定义1.7.2. 一个部分函数

f : ℕ^{k} \to ℕ

是

λ

可定义的当且仅当存在

F \in Λ

满足:

如果 $f (n_{1}, \dots, n_{k}) = m$ , 那么 $F c_{n_{1}} \dots c_{n_{k}} =_{β} c_{m}$ .
如果 $f (n_{1}, \dots, n_{k})$ 是未定义的, 那么 $F c_{n_{1}} \dots c_{n_{k}}$ 没有规范形式.

我们称项

F

定义了函数

f

例子1.7.3. 下列项定义了一些常见函数.

后继: $succ = λ n f x . f (n f x)$ .
加法: $add = λ m n f x . m f (n f x)$ .
乘法: $mult = λ m n f x . m (n f) x$ .
幂: $\exp = λ m n f x . m n f x$ . [注记: 不知是笔误还是有意为之, 实际上这里的幂的定义的参数顺序与通行认知相反. 并且, 其实 $f$ 和 $x$ 也可以不用写出来即可定义幂.]
常零函数: $zero = λ m . 0$ .
$k$ 元参数的第 $i$ 投影: $Π_{i}^{k} = λ m_{1} \dots m_{k} . m_{i}$ .

命题1.7.4. 原始递归函数是

λ

可定义的.

第1.8节注记

$λ$ 演算和与之相关的组合子逻辑是在1930年左右分别由Alonzo Church [9, 10]和Haskell B. Curry引入的. 起初, 这种演算是某意图作为逻辑基础的系统的一部分. 不幸的是, Church的学生Kleene和Rosser发现原始的系统是不一致的, 而Curry简化了这个结果, 其现在被称为Curry悖论. 最终, 仅处理 $λ$ 项, 规约以及变换的子系统, 也就是我们称之为 $λ$ 演算的东西, 被单独进行研究.

$λ$ 绑定和 $α$ 变换的概念在直觉上是非常清晰的, 然而在第1.2节我们看到为了正确地处理它们, 许多技术性的困难必须被克服. 当人们遇到实际实现的问题时, 这个事情就变得尤为重要了. 一种古典的解决方案是使用变量的匿名表示 (所谓的de Bruijn索引). 想要了解更多此方面内容和相关主题, 见例如[18, 19, 24].

第1.9节练习

练习1.2. 修改定义1.2.4以使得操作

M [x ≔ N]

对于所有的

M

N

和

x

都有定义, 然后证明

M [x ≔ N] =_{α} M^{'} [x ≔ N^{'}]

对于所有的

M =_{α} M^{'}

和

N =_{α} N^{'}

均成立 (参照引理1.2.11).

第2章直觉主义逻辑

"逻辑"一词具有多种含义, 从日常推理到复杂的形式系统. 在大多数情况下, 逻辑被用来将陈述划分为"真"和"假". 也就是说, 人们所说的逻辑通常指的是二值古典逻辑的诸多变种之一.

的确, 古典逻辑在需要精确推理的情况下不论如何都可以被视为一种标准, 特别是在数学和计算机科学领域. 古典逻辑的原则作为工具是极其有用的, 其可以用来对于日常生活或者数学中出现的推理模式进行描述和分类.

然而, 明白以下事实也是重要的. 首先, 没有任何规则系统可以捕获丰富而又繁杂的人类思想世界, 因此每种逻辑都只能用作受限目的的工具, 而不可能是面对一切问题的终极神谕.

而且, 古典逻辑的原则, 尽管很容易为我们的直觉所接受, 并不是唯一可能的推理原则(集). 从特定的角度而言 (特别是对于拥有计算机科学背景的读者), 实际上使用别的原则(集)可能是更好的. 让我们稍微仔细地检视一下.

古典逻辑基于真性的基础概念. 陈述的真性是一种绝对性质, 在于其独立于任何的推理, 理解, 或者动作. 一个良形式且无歧义的声明陈述要么是真要么是假, 不论我们 (或者任何其他人) 是否以任何方式知道它, 证明它, 或者验证它. 在这种情况下, 假的含义实际上等于不真, 而这是由排中律表达的, 其断言不论 $p$ 的意义为何, $p \lor \neg p$ 总是成立. (排中律也被称为tertium non datur.)

无需多言, $p \lor \neg p$ 中所包含的信息是相当有限的. 例如, 请看以下句子:

在数字 $π$ 的十进制表示中, 存在七个 $7$ 连成一排.

可能没人能够确定这个句子是真是假, 然而我们却被迫接受要么这个声明成立, 要么其否定成立. 另一个有名的例子是:

存在无理数 $x$ 和 $y$ 使得 $x^{y}$ 是有理数.

这个事实的证明非常简单: 如果

{\sqrt{2}}^{\sqrt{2}}

是有理数, 那么我们取

x = y = \sqrt{2}

; 否则的话, 取

x = {\sqrt{2}}^{\sqrt{2}}

而

y = \sqrt{2}

这个证明的问题在于我们并不知道哪一种可能性是正确的. 但是还有另外一种不同的论证: 对于 $x = \sqrt{2}$ 和 $y = 2 \log_{2} 3$ , 我们有 $x^{y} = 3 \in ℚ$ . 我们称后一个证明是构造性的, 而前者不是.

这样的例子刻画了古典逻辑的某些缺陷. 诚然如此, 在许多应用中, 我们想要寻求问题的实际解, 而不仅仅是知道某个解存在. 因此, 我们想要将能提供实际解的证明方法和不能提供的方法区分开来. 于是, 从非常实际的角度来看, 考虑逻辑的构造性方法也是有意义的.

满足我们的期望并且只接受构造性推理的逻辑在传统上被称为直觉主义逻辑. 为了解释这个名字, 我们需要回忆直觉主义逻辑的哲学基础, 其可以被精确和简单地表述为以下原则: 不存在绝对的真性, 只存在理想化数学家 (创造性主体) 的知识和直觉性构造. 一个逻辑判断只有在创造性主体可以验证其正确性时才能被认为是真. 接受这种观念不可避免地拒绝了排中律这个一致的原则. 正如我们从高贵的Houyhnhnms [464]中学到的 [译注: 出自格列佛游记]:

(...) 理性教导我们只有在确定时才肯定或者否定; 若是超出了我们的知识, 则两者皆不可行.

第2.1节 BHK解释

直觉主义命题逻辑, 也被称为直觉主义命题演算 (缩写为IPC), 其语言和古典命题逻辑相同 [译注: 即句法相同].

2.1.1. 定义. 给定一个命题变量的无限集合

PV

, 我们将公式的集合

Φ

定义为满足下列条件的最小集合:

每个命题变量和常量 $⊥$ 都在 $Φ$ 中;
如果 $φ, ψ \in Φ$ , 那么 $(φ \to ψ), (φ \lor ψ), (φ \land ψ) \in Φ$ .

变量和

⊥

被称为原子公式. 一个公式

φ

的子公式是

φ

的一部分 (未必proper), 其自身是也是一个公式.

也就是说, 我们基本的联结词是: 推出 $\to$ , 析取 $\lor$ , 合取 $\land$ , 以及常量 $⊥$ (谬). 否定 $\neg$ 和等价 $\leftrightarrow$ 是缩略形式, 常量 $⊤$ (真) 也是如此:

$\neg φ$ 是 $φ \to ⊥$ 的缩略;
$φ \leftrightarrow ψ$ 是 $(φ \to ψ) \land (ψ \to φ)$ 的缩略;
$⊤$ 是 $⊥ \to ⊥$ 的缩略.

2.1.2. 约定.

我们往往默认推出是右结合的, 例如我们可以记 $φ \to ψ \to ϑ$ 而不是 $φ \to (ψ \to ϑ)$ .
我们假定否定具有最高的优先级, 推出则是最低的, $\lor$ 和 $\land$ 之间平行. 也就是说, $\neg p \land q \to r$ 的意思是 $((\neg p) \land q) \to r$ .
当然, 我们省略最外面的括号.

为了理解直觉主义逻辑, 我们应该忘掉真性的古典概念. 现在我们关于一个逻辑陈述的判断不再是基于任何赋予该陈述的真值了, 而是在于我们通过显式证明或者说构造澄清该陈述的能力. 其影响在于, 我们不应该试图通过真值表来定义逻辑联结词 (古典逻辑中一般是这样做的), 而是应该基于它们的构造来解释复合公式的意义.

这样的解释经常由所谓的Brouwer-Heyting-Kolmogorov解释给出, 简写为BHK解释. 我们可以将BHK解释阐述为以下一集规则, 而其算法性的风味之后会将我们引至Curry-Howard同构.

$φ_{1} \land φ_{2}$ 的一个构造由 $φ_{1}$ 的一个构造和 $φ_{2}$ 的一个构造构成;
$φ_{1} \lor φ_{2}$ 的一个构造由一个指示子 $i \in {1, 2}$ 和 $φ_{i}$ 的一个构造构成;
$φ_{1} \to φ_{2}$ 的一个构造是一个将每个 $φ_{1}$ 的构造转换为 $φ_{2}$ 的一个构造的方法 (函数);
不存在 $⊥$ 的构造.

我们并不刻画命题变量的构造是什么, 这是因为命题变量的意义只有在其被一个具体的陈述替换时才能得知, 然后我们可以提出关于那个陈述的构造的问题. 与之相对的是, $⊥$ 代表了一个压根没有可能构造的陈述.

否定 $\neg φ$ 被理解为 $φ \to ⊥$ , 即我们可以在假定 $φ$ 会导致谬时断言 $\neg φ$ . 换言之, 则是

$\neg φ$ 的构造是一个将每个 $φ$ 的构造转换为一个并不存在的对象的方法.

\neg φ

和

φ \to ⊥

的等价当然也在古典逻辑中成立, 但是应该注意到直觉主义的

\neg φ

要强于只是不存在

φ

的构造.

读者应该意识到BHK解释远非意图作为构造性语义的精确而又完整的描述. 特别是构造的概念, 其是非形式化的, 可以按照各种各样的方式理解.

2.1.3. 例子. 考虑以下公式:

$⊥ \to p$ ;
$p \to q \to p$ ;
$(p \to q \to r) \to (p \to q) \to p \to r$ ;
$p \to \neg \neg p$ ;
$\neg \neg \neg p \to \neg p$ ;
$(p \to q) \to (\neg q \to \neg p)$ ;
$\neg (p \lor q) \leftrightarrow (\neg p \land \neg q)$ ;
$((p \land q) \to r) \leftrightarrow (p \to (q \to r))$ ;
$\neg \neg (p \lor \neg p)$ ;
$(p \lor \neg p) \to \neg \neg p \to p$ .

以上公式都可被赋予一个BHK解释. 例如, 公式i的构造在于可以安全地认为

⊥

的构造是不可能的. (与之对比的是, 我们没有

q \to p

的构造, 因为我们不能一般地排除

q

的构造的存在.) 公式iv的构造, 即对于

p \to ((p \to ⊥) \to ⊥)

的构造, 如下:

给定 $p$ 的一个构造, 现在给出 $((p \to ⊥) \to ⊥)$ 的一个构造:
取 $p \to ⊥$ 的一个构造, 这是将 $p$ 的构造转换为 $⊥$ 的构造的方法. 既然我们已经有了 $p$ 的构造, 那么我们就可以用这个方法得到 $⊥$ 的构造.

读者应该能够自行发现其他公式的BHK解释 (练习2.2).

2.1.4. 例子. 以下每个公式都是一个古典重言, 但是并不存在一个构造, 尽管其中一些与前一个例子中的公式类似或者对偶.

$((p \to q) \to p) \to p$ ;
$p \lor \neg p$ ;
$\neg \neg p \to p$ ;
$(\neg q \to \neg p) \to (p \to q)$ ;
$\neg (p \land q) \leftrightarrow (\neg p \lor \neg q)$ ;
$(p \to q) \to (\neg p \to q) \to q$ ;
$((p \leftrightarrow q) \leftrightarrow r) \leftrightarrow (p \leftrightarrow (q \leftrightarrow r))$ ;
$(p \to q) \leftrightarrow (\neg p \lor q)$ ;
$(p \lor q \to p) \lor (p \lor q \to q)$ ;
$(\neg \neg p \to p) \to p \lor \neg p$ .

例如, 公式iii似乎和例子2.1.3的iv表达了相同的原则. 类似地, 公式iv和例子2.1.3的vi经常被视为反证法的两种模式. 公式v和例子2.1.3的vii都被称为De Morgan律, 表达了合取与析取之间的古典对偶.

这些例子表明古典逻辑的某种对称在我们转向构造性语义时消失了, 例如否定不再是对合了, 即 $φ$ 和 $\neg \neg φ$ 不能被视为等同的了. 然而, 我们也应该注意到iii表达了一个比ii弱的性质, 因为我们没有x的构造.

并不那么令人意外的是, 分类讨论证明这一原则vi并非构造性的. 实际上, 这只是不能用排中律的一个简单后果而已, 即我们不能先验地将一个论证划分为不同的情形. 但是, 不仅是否定或者假可能造成困难, 这可能有点令人意外. 比如说, 公式i (称为Peirce律) 是纯粹推论性的, 但是我们仍然不能找到其构造. 另一个例子是公式vii, 其表达了等价的古典结合律. 我们可以使用真值表验证它, 但是从构造性的角度来看, 这个结合性质似乎纯粹是意外而已.

公式viii可以被视为基于否定和析取的对于古典推出的定义. 从构造性角度而言, 这个定义并不可行. 我们还可以说更多: $\to, ⊥, \lor, \land$ 中的每一个都不可由其他联结词定义 (见练习2.26).

第2.2节自然演绎

为了形式化直觉主义命题逻辑, 我们定义了一个被称为自然演绎的证明系统, 用 $NJ (\to, ⊥, \land, \lor)$ 表示, 或者就简单地记作 $NJ$ . 自然演绎的规则精确地表达了第2.1节的非形式化语义的想法.

2.2.1. 定义.

自然演绎中的一个判断是一个序对, 被记作 $Γ ⊢ φ$ (读作" $Γ$ 证明了 $φ$ "), 其由一个有限的公式集合 $Γ$ 和一个公式 $φ$ 构成.
我们在书写判断的时候使用了多种简化, 例如记 $φ_{1}, φ_{2} ⊢ ψ$ 而不是 ${φ_{1}, φ_{2}} ⊢ ψ$ , 记 $Γ, Δ$ 而不是 $Γ \cup Δ$ , 记 $Γ, φ$ 而不是 $Γ \cup {φ}$ . 特别地, 记号 $⊢ φ$ 代表 $\emptyset ⊢ φ$ .
Γ⊢φ的一个形式证明或推导是一个有限的判断的树, 满足以下条件:
- 根标签是 $Γ ⊢ φ$ ;
- 所有的叶子都是公理, 即具有形式 $Γ, φ ⊢ φ$ 的判断;
- 每个母结点的标签都由其女之标签由图2.1的规则得到.
如果这样一个证明存在, 那么我们称Γ⊢φ是可证明的或可推导的, 记作Γ⊢Nφ. 对于无限的Γ, Γ⊢Nφ的意思是对于某个Γ的有限子集Γ0有Γ0⊢Nφ.
通常我们省略 $⊢_{N}$ 中的标记 $_{N}$ . 注意到若是如此那么记号 $Γ ⊢ φ$ 就过载了. 它既表达一个判断的可证明性, 也代表判断本身. 然而, 其用意在上下文中总是明确的.
如果 $⊢ φ$ , 那么我们称 $φ$ 是一个定理. [原注: 一般而言, 定理指的是在某个逻辑系统中可证明的公式.]

这个证明系统由一个公理模式 (axiom scheme) 和一些规则构成. 对于每个逻辑联结词 (除了

⊥

) 我们有一或两个引入规则和一或两个消去规则. 对于某个联结词

\circ

的引入规则刻画了形式为

φ \circ ψ

的结论是如何被推导出来的. 消去规则刻画了

φ \circ ψ

是怎样用来推导其他公式的. 观察到自然演绎的规则可以被视为对于BHK解释的形式化, 其中构造应该被读作证明. 的确如此, 例如考虑推出的情况. 规则

(\to I)

的前提

Γ, φ ⊢ ψ

可以被理解为在提供

φ

的一个证明的情况下从

Γ

推出

ψ

的能力. 这就足以导出这条规则里的推论了. 消去规则

(\to E)

对应于相同的想法: 如果我们有一个

φ \to ψ

的证明, 那么我们可以将

φ

的一个证明转换为

ψ

的一个证明. 在某种意义上, 规则

(\to E)

可以被视为规则

(\to I)

的逆. 类似的观察 (称为反转原理, 见Prawitz [25]) 也可应用于其他联结词. 规则

(⊥ E)

(称为ex falso sequitur quodlibet, 或者就ex falso) 是其中的一个例外, 因为并不存在与之匹配的引入规则. [译注: ex falso也被称为爆炸原理.]

\begin{matrix} Γ, φ ⊢ φ (Ax) \\ \frac{Γ, φ ⊢ ψ}{Γ ⊢ φ \to ψ} (\to I) & \frac{Γ ⊢ φ \to ψ Γ ⊢ φ}{Γ ⊢ ψ} (\to E) \\ \frac{Γ ⊢ φ Γ ⊢ ψ}{Γ ⊢ φ \land ψ} (\land I) & \frac{Γ ⊢ φ \land ψ}{Γ ⊢ φ} (\land E) \frac{Γ ⊢ φ \land ψ}{Γ ⊢ ψ} \\ \frac{Γ ⊢ φ}{Γ ⊢ φ \lor ψ} (\lor I) \frac{Γ ⊢ ψ}{Γ ⊢ φ \lor ψ} & \frac{Γ, φ ⊢ ϑ Γ, ψ ⊢ ϑ Γ ⊢ φ \lor ψ}{Γ ⊢ ϑ} (\lor E) \\ \frac{Γ ⊢ ⊥}{Γ ⊢ φ} (⊥ E) \end{matrix}

图2.1: 直觉主义自然演绎

NJ

2.2.2. 记号. 有时考虑命题逻辑的片段也是有用的, 其中一些联结词并不出现. 例如, 在第2.6节, 我们讨论了直觉主义命题逻辑的推论片段

IPC (\to)

NJ

的仅有公理模式和关于推论的规则构成的子系统记作

NJ (\to)

. 这种约定也可以应用于其他片段, 例如

IPC (\to, \land, \lor)

是所谓的正片段 (positive fragment), 也被称为极小逻辑,

NJ (\to, \land, \lor)

则代表

NJ

的与之相配的子系统.

2.2.3. 例子. 我们给出对于我们最喜欢的公式的样例证明. 以下, 公式

φ, ψ, ϑ

可以是任意的:

$\frac{φ ⊢ φ}{⊢ φ \to φ} (\to I)$
$\frac{\frac{φ, ψ ⊢ φ}{φ ⊢ ψ \to φ} (\to I)}{⊢ φ \to (ψ \to φ)} (\to I)$
这里, $Γ$ 是 ${φ \to (ψ \to ϑ), φ \to ψ, φ}$ 的缩略. $\frac{\frac{\frac{\frac{\frac{Γ ⊢ φ \to (ψ \to ϑ) Γ ⊢ φ}{Γ ⊢ ψ \to ϑ} (\to E) \frac{Γ ⊢ φ \to ψ Γ ⊢ φ}{Γ ⊢ ψ} (\to E)}{Γ ⊢ ϑ} (\to E)}{φ \to (ψ \to ϑ), φ \to ψ ⊢ φ \to ϑ} (\to I)}{φ \to (ψ \to ϑ) ⊢ (φ \to ψ) \to (φ \to ϑ)} (\to I)}{⊢ (φ \to (ψ \to ϑ)) \to (φ \to ψ) \to (φ \to ϑ)} (\to I)$

2.2.4. 引理. 直觉主义命题逻辑在弱化和替换下封闭, 即

Γ ⊢ φ

可以推出

Γ, ψ ⊢ φ

并且

Γ [p ≔ ψ] ⊢ φ [p ≔ ψ]

, 其中

[p ≔ ψ]

代表将命题变量

p

的全部出现替换以

ψ

. [译注: 因为没有绑定结构, 所以对于替换的描述非常简单.]

证明. 对于证明的大小进行归纳 (练习2.3).

◻

以上的结果有时也被描述为以下是直觉主义命题逻辑的导出 (或者说兼容) 规则: $\frac{Γ ⊢ φ}{Γ, ψ ⊢ φ} \frac{Γ ⊢ φ}{Γ [p ≔ ψ] ⊢ φ [p ≔ ψ]}$

第2.3节古典逻辑的代数语义

在这接下来的一节中我们将要引入直觉主义逻辑的一种代数语义. 为了帮助读者更好地理解, 我们从古典逻辑开始. 通常来说, 古典命题公式的语义被定义成这样, 其使得每个联结词都可以被视为施行于真值的集合 $𝔹 = {0, 1}$ 上的操作. 也就是说, 我们实际上是在处理一个代数系统 $⟨ 𝔹, \lor, \land, \to, -, 0, 1 ⟩$ 其中 $0 \lor 1 = 1$ , $0 \land 1 = 0$ , $0 \to 1 = 1$ , 等等. 如果我们为该系统赋予一个序使得 $0 < 1$ , 那么我们有以下性质: $a \leq b 当且仅当 a \to b = 1 .$ 真值的代数和集合的代数之间存在显见的相似之处. 逻辑运算 $\lor$ 和 $\land$ 表现得就非常类似于集合论的 $\cup$ 和 $\cap$ . 等式 $A \cup B = {x | (x \in A) \lor (x \in B)}$ 陈述了诸多类同中的一例. 以类似的方式, 否定对应于补 $- A$ (相对于某个固定的论域) 而推论对应于 $- A \cup B$ .

我们现在即将引入的布尔代数的概念是真值的代数和集合的代数的泛化. 我们先从一个更弱因而也更宽泛的概念格开始.

2.3.1. 定义. 一个格是一个偏序

⟨ A, \leq ⟩

, 其满足对于每个

A

的二元素子集

{a, b}

A

中存在它的最小上界和最大下界. 我们记

\sup_{A} {a, b}

为

a ⊔ b

\inf_{A} {a, b}

为

a ⊓ b

. 与集合论的运算相类比, 我们称

⊔

为并 (或者join),

⊓

为交 (或者meet). 格的top (相应地, bottom) 若存在, 通常被记为

1

(相应地,

0

2.3.2. 引理. 在一个格中, 以下条件等价:

$a \leq b$ ;
$a ⊓ b = a$ ;
$a ⊔ b = b$ .

证明. 即得.

◻

2.3.3. 例子. 每个线序, 例如真值的集合

𝔹

, 是一个格. 每个在集合的并与交下封闭的集族也是一个格. 但是, 相对于

\cup

和

\cap

的封闭性并不是集族成为格的必要条件. 一个例子是Euclid平面的所有凸子集的族. (一个集合

A

是凸的当且仅当对于所有的

a, b \in A

, 连接

a

与

b

的线段被包含在

A

中.)

2.3.4. 引理. 以下等式在每个格中都是成立的:

$a ⊔ a = a$ 和 $a ⊓ a = a$ ;
$a ⊔ b = b ⊔ a$ 和 $a ⊓ b = b ⊓ a$ ;
$(a ⊔ b) ⊔ c = a ⊔ (b ⊔ c)$ 和 $(a ⊓ b) ⊓ c = a ⊓ (b ⊓ c)$ ;
$(a ⊔ b) ⊓ a = a$ 和 $(a ⊓ b) ⊔ a = a$ .

证明. 常规的应用定义而已. [译注: 这四条性质分别被称为幂等律, 交换律, 结合律, 吸收律.]

◻

2.3.5. 定义.

格A被称为分配的, 如果以下等式在A中成立:
1. $(a ⊔ b) ⊓ c = (a ⊓ c) ⊔ (b ⊓ c)$ ;
2. $(a ⊓ b) ⊔ c = (a ⊔ c) ⊓ (b ⊔ c)$ .
假定格 $A$ 拥有top元素 $1$ 和bottom元素 $0$ , 我们称 $b$ 是 $a$ 的补当且仅当 $a ⊔ b = 1$ 且 $a ⊓ b = 0$ .

2.3.6. 引理. 令

b

是

a

在某分配格

A

中的补, 那么

b

是

A

中满足

a ⊓ b = 0

的最大元素. 特别地,

a

最多只有一个补.

证明. 设

a ⊓ c = 0

, 那么

c \leq b

, 因为

c = 1 ⊓ c = (a ⊔ b) ⊓ c = (a ⊓ c) ⊔ (b ⊓ c) = 0 ⊔ (b ⊓ c) = b ⊓ c .

◻

2.3.7. 定义. 一个布尔代数是一个带有top和bottom元素的分配格

B

, 其满足每个

B

的元素

a

都有一个补 (记作

- a

布尔代数经常以形式为 $ℬ = ⟨ B, ⊔, ⊓, -, 0, 1 ⟩$ 的代数结构呈现. 在这种情况下, 偏序可以在 $a \leq b$ 和 $a ⊓ b = a$ 的等价性 (见引理2.3.2) 的帮助之下被重新构造出来.

2.3.8. 例子. 令

X

是任意的集合. 一个集合域 (

X

上的) 是一个非空的

X

的子集族

ℛ

, 其在集合论的并, 交, 补 (相对于

X

) 下封闭. 每个集合域都是一个布尔代数. 集合域的例子如下:

$𝒫 (X)$ , $X$ 的幂集;
${\emptyset, X}$ ;
${A \subseteq X | A 有限或者 X - A 有限}$ .

注意到真值的代数

𝔹

(暂时忘却

\to

) 同构于ii.

以下的结果被称为Stone表示定理.

2.3.9. 定理. 每个布尔代数同构于一个集合域.

我们省略了Stone定理的证明, 因为其会让我们离题太远. 读者在闲暇之余可以花些时间做做练习2.15, 但是现在让我们转向古典命题逻辑的布尔代数语义.

2.3.10. 定义. 布尔代数

ℬ = ⟨ B, ⊔, ⊓, -, 0, 1 ⟩

中的一个赋值是任意的从命题变量

PV

到

B

的映射

v

. 一个公式

φ

相对于赋值

v

(在

ℬ

中) 的值由归纳定义.

\begin{array}{l} {⟦ p ⟧}_{v} & = & v (p), 对于 p \in PV; \\ {⟦ ⊥ ⟧}_{v} & = & 0; \\ {⟦ φ \lor ψ ⟧}_{v} & = & {⟦ φ ⟧}_{v} ⊔ {⟦ ψ ⟧}_{v}; \\ {⟦ φ \land ψ ⟧}_{v} & = & {⟦ φ ⟧}_{v} ⊓ {⟦ ψ ⟧}_{v}; \\ {⟦ φ \to ψ ⟧}_{v} & = & - {⟦ φ ⟧}_{v} ⊔ {⟦ ψ ⟧}_{v} . \end{array}

当

{⟦ φ ⟧}_{v} = 1

时, 记

ℬ, v ⊨ φ

. 若对于所有的

v

有

ℬ, v ⊨ φ

, 记

ℬ ⊨ φ

显然, 这种布尔代数语义是通常二值语义的一种泛化. 的确, 一个公式 $φ$ 是一个古典重言当且仅当 $𝔹 ⊨ φ$ . 实际上, 这种泛化不是本质性的.

2.3.11. 定理. 一个命题公式

φ

是一个古典重言当且仅当对于所有的布尔代数

ℬ

有

ℬ ⊨ φ

证明. 自右向左是即得的. 为了证明另一个方向, 我们假设对于某个

ℬ

有

ℬ ⊭ φ

. 根据Stone表示定理我们不妨设

ℬ

是某个

X

上的一个集合域.
既然

ℬ ⊭ φ

, 那么存在某个

ℬ

中的赋值

v

满足

{⟦ φ ⟧}_{v} \neq X

. 因此, 存在

x \in X

满足

x \notin {⟦ φ ⟧}_{v}

. 定义一个二元赋值

w

(即

𝔹

中的一个赋值) 满足

w (p) = 1

当且仅当

x \in {⟦ p ⟧}_{v}

. 根据归纳, 可以证明对于所有的公式

ψ

{⟦ ψ ⟧}_{w} = 1 当且仅当 x \in {⟦ ψ ⟧}_{v} .

那么,

{⟦ φ ⟧}_{w} \neq 1

◻

第2.4节 Heyting代数

现在我们将建立直觉主义命题逻辑的一种语义. 出于这样的目的我们检视了公式相对于可证明性的代数性质. 我们首先观察到可证明的推论表现得几乎就像公式上的一个序关系, 即它是自反的和传递的. 更确切地说, 对于每个 $Γ$ 我们有:

$Γ ⊢ φ \to φ$ ;
如果 $Γ ⊢ φ \to ψ$ 且 $Γ ⊢ ψ \to ϑ$ , 那么 $Γ ⊢ φ \to ϑ$ .

然而, 这个关系并不是反对称的. 但是, 我们可以通过将等价的公式视为等同的来将其转化为一个偏序关系. [译注: 这实际上是格论的一个标准技巧, 其可以从预序中导出一个偏序.] 为了使之精确, 我们令

Γ

是一个固定的命题公式集合 (特别地,

Γ

可以为空). 我们按照以下方式定义一个关系

\sim_{Γ}

φ \sim_{Γ} ψ 当且仅当 Γ ⊢ φ \to ψ 且 Γ ⊢ ψ \to φ .

不难看出

\sim_{Γ}

是所有公式构成的集合

Φ

上的一个等价关系, 并且有 (我们省略

\sim_{Γ}

中的下标

_{Γ}

{[⊥]}_{\sim} = {φ | Γ ⊢ \neg φ} 且 {[⊤]}_{\sim} = {φ | Γ ⊢ φ} .

令

L_{Γ} = Φ / \sim = {{[φ]}_{\sim} | φ \in Φ}

, 那么显然由

{[φ]}_{\sim} \leq_{Γ} {[ψ]}_{\sim} 当且仅当 Γ ⊢ φ \to ψ

定义的关系

\leq_{Γ}

是

L_{Γ}

上一个良定的偏序. 我们有以下等价:

{[φ]}_{\sim} = {[ψ]}_{\sim} 当且仅当 {[φ]}_{\sim} \leq_{Γ} {[ψ]}_{\sim} 且 {[ψ]}_{\sim} \leq_{Γ} {[φ]}_{\sim} .

我们接下来的步骤是发现偏序

⟨ L_{Γ}, \leq_{Γ} ⟩

是一个格. 定义

{[φ]}_{\sim} ⊔ {[ψ]}_{\sim} = {[φ \lor ψ]}_{\sim}; {[φ]}_{\sim} ⊓ {[ψ]}_{\sim} = {[φ \land ψ]}_{\sim} .

运算

⊔

和

⊓

是良定义的, 因为以下是可证明的:

(φ \leftrightarrow φ^{'}) \to (ψ \leftrightarrow ψ^{'}) \to ((φ \lor ψ) \leftrightarrow (φ^{'} \lor ψ^{'}));

(φ \leftrightarrow φ^{'}) \to (ψ \leftrightarrow ψ^{'}) \to ((φ \land ψ) \leftrightarrow (φ^{'} \land ψ^{'})) .

读者应该很容易验证

第2.5节 Kripke语义

我们现在引入直觉主义命题逻辑的另一种语义. 这种语义反映了以下想法. 从构造性的角度来看, 我们只能断言我们已经确定了的命题的真性. 但是, 通过学到新的事实, 我们获得了更多的信息, 并且我们可以为我们的现有知识 (state of knowledge) 添加新的命题. 然而, 我们不应该失去我们的知识. 换言之, 现在为真的将永远保持为真, 但是今天还没能确定为真的明天就可能变成真的了. 因此, 我们不得不小心, 只在我们全然不可能断言 $A$ 时才断言 $A$ 的否定.

2.5.1. 定义. 一个Kripke模型是一个具有形式

𝒞 = ⟨ C, \leq, ⊩ ⟩

的三元组, 其中

C

是一个非空集合, 它的元素被称为状态或者可能世界,

\leq

是一个

C

中的偏序, 而

⊩

是

C

的元素和命题变量之间的一个二元关系. 关系

⊩

(读作"力迫") 必须满足以下单调性条件.

如果 c \leq c^{'} 且 c ⊩ p 那么 c^{'} ⊩ p .

直觉在于模型的元素代表了知识状态. 关系

\leq

与通过获得更多知识来扩展状态有关. 关系

⊩

决定了在一个给定的状态下哪些命题变量被认为是真的. 我们按照以下方式延拓这个关系来为命题公式提供含义.

2.5.2. 定义. 如果

𝒞 = ⟨ C, \leq, ⊩ ⟩

是一个Kripke模型, 那么

$c ⊩ φ \lor ψ$ 当且仅当 $c ⊩ φ$ 或 $c ⊩ ψ$ ;
$c ⊩ φ \land ψ$ 当且仅当 $c ⊩ φ$ 且 $c ⊩ ψ$ ;
$c ⊩ φ \to ψ$ 当且仅当对于所有满足 $c^{'} ⊩ φ$ 的 $c^{'} \geq c$ 有 $c^{'} ⊩ ψ$ ;
$c ⊩ ⊥$ 并不成立.

注意到上述定义推出了以下否定的法则:

$c ⊩ \neg φ$ 当且仅当对于所有的 $c^{'} \geq c$ 有 $c^{'} ⊮ φ$ .

记号

⊩

可以按照多种方式运用. 有时我们记

𝒞, c ⊩ φ

以明确使用了哪个模型. 当对于所有的

c \in C

有

c ⊩ φ

时, 我们记

𝒞 ⊩ φ

. 记号

c ⊩ Γ

的意思是对于所有的

φ \in Γ

有

c ⊩ φ

, 对于记号

𝒞 ⊩ Γ

也是类似的. 最后, 若对于每个Kripke模型

𝒞

和每个

𝒞

的状态

c

, 条件

𝒞, c ⊩ Γ

能够推出

𝒞, c ⊩ φ

, 那么记

Γ ⊩ φ

2.5.3. 引理. 如果

c \leq c^{'}

且

c ⊩ φ

那么

c^{'} ⊩ φ

2.5.4. 例子. 令

C = {c, c^{'}, c^{″}}

, 其中

c \leq c^{'}

而

c^{'}

和

c^{″}

是不可比较的. 一个Kripke模型

𝒞 = ⟨ C, \leq, ⊩ ⟩

, 其中

第2.6节推论片段

最重要的联结词就是推出了. 因此, 研究推出性公式是有意义的, 也就是仅由这种联结词构成的公式. 这种受限演算的自然演绎系统 $NJ (\to)$ 由规则 $(\to E)$ 和 $(\to I)$ 以及公理模式 $(Ax)$ 构成.

2.6.1. 定理. 自然演绎系统

NJ (\to)

相对于Kripke模型是完备的, 即如果

\to

是唯一出现在

Γ

和

φ

中的联结词, 那么条件

Γ ⊢ φ

和

Γ ⊩ φ

是等价的.

证明.

◻

第2.7节注记

数学中的构造主义深深地根植于19世纪, 甚至是更加遥远的过去. 例如, 直觉主义者他们自己也承认受到Immanuel Kant (1724-1804) 的哲学的启发. 根据Kant, 数学认知的领域诸如时间和空间可直达人类的直觉而并非经验上所"观察"到的. 因此, 数学可被视为纯粹的心灵上的构造.

Leopold Kronecker (1823-1891) 通常被引为第一个显式将构造主义的想法应用于数学的作者. 根据Kronecker, 一个数字的正确定义, 可在有限步骤之内被验证. 而一个存在性陈述的证明, 应该提供一个能够见证这个陈述的显式对象.

为了寻找数学的坚实基础, 许多其他人也加入了Kronecker. 19世纪下半叶, 数学正发生着相当重要的改变. 随着新分支的发展, 包括数理逻辑, 数学研究的主题变得愈发抽象而与现实经验无关. 数学家的活动从探索"真实"世界的性质转移到了创造一个抽象世界. 这引发了关于数学基础的重要问题. 随着悖论的发现, 特别是Russell发现的知名悖论, 这些问题变得紧急起来.

19世纪末和20世纪初, 许多思想和流派得以建立和竞争, 它们意在解释现代数学的概念基础.

第2.8节练习

第3章简单类型 $λ$ 演算

在逻辑学中, 判断一个公式相对于某个特定的语义是否有效 (valid) 总是核心议题. 或者, 更一般地, 一集假设是否在所有模型中都蕴涵一个公式. 在古典逻辑的"语义传统"之中, 这种问题总是最重要的主题, 而可靠 (sound) 且完备 (complete) 的证明系统的构造主要被视为判断有效性的工具. 在这种情况下, 公式和判断的可证明性是和证明相关的问题之中唯一令人感兴趣的. 人们会问证明是否存在, 但是不必问是哪一个证明.

在证明论中, 视角变得有所不同. 我们想要研究证明的结构, 比较各种证明, 从中选出一些, 以与其他的证明进行区分. 这对于构造性逻辑而言是尤为重要的, 其中证明 (构造) 而不是语义是最终的标准.

因此, 寻求一种简便的证明记号是非常自然的. 例如, 我们可以用 $M : φ$ 来表示 $M$ 是 $φ$ 的一个证明. 若有额外假设 $Γ$ , 那么我们或许可以扩展这个记号为 $Γ ⊢ M : φ$ 现在, 如果 $M$ 和 $N$ 分别是 $φ \to ψ$ 和 $φ$ 的证明, 那么由 $(\to E)$ 得到的 $ψ$ 的证明可以表示为 $@ (M, N) : ψ$ , 或者就简单地记作 $M N : ψ$ . 这给出了一种"带注解的" $(\to E)$ 规则 $\frac{Γ ⊢ M : φ \to ψ Γ ⊢ N : φ}{Γ ⊢ M N : ψ}$ 当试着为 $(Ax)$ 设计一种带注解的版本时, 读者或许会发现给假设命名也是很方便的事情, 例如 $x : φ, y : ψ ⊢ x : φ$ 代表使用第一个假设. 这个想法在我们想要注解 $(\to I)$ 规则时也派得上用场, 那么discharge一个证明 $M$ 中的假设 $x$ 可以被记成诸如 $♯ x M$ , $ξ x M$ , ... 我们为什么不试试lambda呢? $\frac{Γ, x : φ ⊢ M : ψ}{Γ ⊢ λ x M : φ \to ψ}$ 是的, 我们得到的就是lambda记号. 用一位著名作家的话来说, 虽然是在完全不同的上下文中, 那就是相似并非刻意也并非偶然, 而是不可避免的. 的确, 一个推论的一个证明代表了一个构造, 而根据BHK解释, 一个推论的一个构造是一个函数.

然而, 不是每个lambda项都可以被用作证明的记号. 例如, 自应用 $x x$ 似乎并不代表任何命题的证明, 不论由 $x$ 注解的假设为何. 所以, 在我们探索证明和项的类似之处 (第4章的事情) 之前, 我们必须寻找合适的lambda演算的子系统.

正如我们所说, BHK解释将推论的构造和函数视为等同的. 在数学中, 一个函数 $f$ 总是定义在一个特定的定义域 (domain) $A$ 上, 而值落在一个陪域 (codomain) $B$ 中. 这被记作 $f : A \to B$ . 类似地, 一个公式 $φ \to ψ$ 的一个构造也只能被应用于指定的参数上来, 也就是前提 (premise) 的构造. 那么, 其结果是结论 (conclusion) 的构造, 它当然也只能具有特定的类型.

在lambda演算中, 我们可以引入类型来描述项的函数行为. 一个应用 $M N$ 只有当 $M$ 具有形式为 $σ \to τ$ 的函数类型而 $N$ 具有类型 $σ$ 时才是可能的. 其结果具有类型 $τ$ . 这是一种相当类似于严格定型的编程语言所具有的类型原则.

几乎从一开始表达项的函数性的类型赋予的概念就被纳入了组合子逻辑和lambda演算之中, 自那时起各种类型化演算就得到了全面的研究. 本章我们将引入对于类型概念最基本的形式化: 系统 $λ_{\to}$ .

第3.1节 Curry风格的简单类型 $λ$ 演算

我们从Curry风格的简单类型 $λ$ 演算开始, 其中我们处理和第1章相同的通常的lambda项.

定义3.1.1.

一个推论命题公式被称为一个简单类型. 所有简单类型构成的集合记作 $Φ_{\to}$ .
一个环境是具有形式 ${x_{1} : τ_{1}, \dots, x_{n} : τ_{n}}$ 的一个有限的序对集合, 其中 $x_{i}$ 是不同的 $λ$ 变量, $τ_{i}$ 是类型. 也就是说, 环境是从变量到类型的有限的部分函数. 因此, 如果 $(x : τ) \in Γ$ , 我们也可以将其写成 $Γ (x) = τ$ . 我们也定义: $dom (Γ) = {x \in Υ | (x : τ) \in Γ, 对于某个 τ}; rg (Γ) = {τ \in Φ_{\to} | (x : τ) \in Γ, 对于某个 x} .$

在其他文献中, 考虑简单类型lambda演算的一种变体是相当常见的, 其中所有的类型都从唯一的一个类型变量构造而来 (因而其被称为类型常量). 这样一种lambda演算的计算性质类似于我们的 $λ_{\to}$ . 但是, 从"逻辑"角度而言这种限制于一个类型常量的情况并不是同样有趣的, 参见练习4.10.

记号.

τ \to \dots \to τ \to σ

被缩略为

τ^{n} \to σ

, 其中

τ

出现了

n

次. 环境

{x_{1} : τ_{1}, \dots, x_{n} : τ_{n}}

经常被简记作

x_{1} : τ_{1}, \dots, x_{n} : τ_{n}

. 如果

dom (Γ) \cap dom (Γ^{'}) = \emptyset

, 那么我们也将

Γ \cup Γ^{'}

记作

Γ, Γ^{'}

. 特别地,

Γ, x : τ

代表

Γ \cup {x : τ}

, 其中假定

x \notin dom (Γ)

. 类似的约定也适用于之后的章节.

定义3.1.2. 一个判断由一个环境, 一个lambda项和一个类型构成, 记作

Γ ⊢ M : τ

. 图3.1中的规则定义了系统

λ_{\to}

的可推导的规则的概念. (读者必须记住规则

(Var)

和

(Abs)

中变量

x

不在

Γ

的定义域之中.) 如果

Γ ⊢ M : τ

是可推导的, 那么我们称

M

在

Γ

中具有类型

τ

, 记作

Γ ⊢_{λ_{\to}} M : τ

或者就记成

Γ ⊢ M : τ

(参考定义2.2.1).

\begin{matrix} (Var) & Γ, x : τ ⊢ x : τ \\ (Abs) & \frac{Γ, x : σ ⊢ M : τ}{Γ ⊢ (λ x M) : σ \to τ} \\ (App) & \frac{Γ ⊢ M : σ \to τ Γ ⊢ N : σ}{Γ ⊢ (M N) : τ} \end{matrix}

图3.1: 简单类型lambda演算

λ_{\to}

例子3.1.3. 令

σ, τ, ρ

是任意的类型, 那么:

$⊢ I : σ \to σ$ ;
$⊢ K : σ \to τ \to σ$ ;
$⊢ S : (σ \to τ \to ρ) \to (σ \to τ) \to σ \to ρ$ .

一个形式为 $M : τ \to σ$ 的类型赋予当然可以被解释为" $M$ 是一个以 $τ$ 为定义域 $σ$ 为陪域的函数". 但是我们必须明白这里对于"定义域"和"陪域"的理解不是集合论性质的. 在Curry风格的类型化演算中, 类型被更适切地描述为(由项满足的)谓词或者规格 (specification) 而不是集合论性质的函数空间. 在集合论中 $f : A \to B$ 的含义为 $f$ 的参数恰是 $A$ 的元素, 而所有的值都必须属于 $B$ . 与之相对地, $M : τ \to σ$ 仅意味着将 $M$ 应用于一个类型为 $τ$ 的参数必须产生一个类型为 $σ$ 的结果.

本节我们以系统 $λ_{\to}$ 的一些基本性质作结.

引理3.1.4.

如果 $Γ ⊢ M : τ$ , 那么 $FV (M) \subseteq dom (Γ)$ .
如果 $Γ, x : τ ⊢ M : σ$ 并且 $y \notin dom (Γ) \cup {x}$ , 那么 $Γ, y : τ ⊢ M [x ≔ y] : σ$ .

证明. 这两个都可以通过对于

M

的长度进行归纳来证明. 作为一个例子, 我们处理ii的抽象的情形.
设

M = λ z M^{'}

和

σ = σ^{″} \to σ^{'}

, 并且我们从

Γ, x : τ, z : σ^{″} ⊢ M^{'} : σ^{'}

推导出了

Γ, x : τ ⊢ M : σ

. 如果

z \neq y

, 那么根据归纳假设, 我们知道

Γ, y : τ, z : σ^{″} ⊢ M^{'} [x ≔ y] : σ^{'}

, 因而

Γ, y : τ ⊢ λ z M^{'} [x ≔ y] : σ

. [译注: 根据前面的约定, 这个记号的含义是对于

M^{'}

进行替换, 而不是整个项.] 现在注意到

λ z M^{'} [x ≔ y] = (λ z M^{'}) [x ≔ y]

.
如果

z = y

并且

Γ, x : τ, z : σ^{″} ⊢ M^{'} : σ^{'}

, 那么我们可以

◻

引理3.1.5. (Generation lemma). 设

Γ ⊢ M : τ

如果 $M$ 是一个变量 $x$ , 那么 $Γ (x) = τ$ .
如果 $M$ 是一个应用 $P Q$ , 那么对于某个 $σ$ , $Γ ⊢ P : σ \to τ$ 且 $Γ ⊢ Q : σ$ .
如果 $M$ 是一个抽象 $λ x N$ 并且 $x \notin dom (Γ)$ , 那么 $τ = τ_{1} \to τ_{2}$ , 其中 $Γ, x : τ_{1} ⊢ N : τ_{2}$ .

证明.

◻

引理3.1.6.

如果 $Γ ⊢ M : σ$ 并且对于所有的 $x \in FV (M)$ 有 $Γ (x) = Γ^{'} (x)$ , 那么 $Γ^{'} ⊢ M : σ$ .
如果 $Γ, x : τ ⊢ M : σ$ 并且 $Γ ⊢ N : τ$ , 那么 $Γ ⊢ M [x ≔ N] : σ$ .

证明. 我们对于

M

的大小进行归纳.

◻

定理3.1.7. (Subject reduction). 如果

Γ ⊢ M : σ

并且

M ↠_{β} N

, 那么

Γ ⊢ N : σ

证明.

◻

定义3.1.8. 将类型

σ

中的类型变量

p

替换为类型

τ

, 记作

σ [p ≔ τ]

, 被定义为:

\begin{matrix} p [p ≔ τ] & = & τ; \\ q [p ≔ τ] & = & q, 如果 q \neq p; \\ (σ_{1} \to σ_{2}) [p ≔ τ] & = & σ_{1} [p ≔ τ] \to σ_{2} [p ≔ τ] . \end{matrix}

记号

Γ [p ≔ τ]

代表

{(x : σ [p ≔ τ]) | (x : τ) \in Γ}

, 类似的记号还可应用于等式, 等式的集合, 诸如此类.

命题3.1.9. 如果

Γ ⊢ M : σ

, 那么

Γ [p ≔ τ] ⊢ M : σ [p ≔ τ]

第3.2节类型重构算法

一个项 $M \in Λ$ 是可定型的, 如果存在 $Γ$ 和 $σ$ 满足 $Γ ⊢ M : σ$ . 可定型项的集合是所有 $λ$ 项的集合的一个真子集. 因此, 判断系统 $λ_{\to}$ 中到底哪些项可被赋予类型以及如何有效地找出这些类型成了根本性的问题. 实际上, 从对于三元谓词" $Γ ⊢ M : τ$ "的分析之中我们可以提出许多判定问题. 以下的定义对于每个能够导出具有这种形式的判断的类型赋予系统都是有意义的.

定义3.2.1.

类型检查问题指的是对于一个给定的环境 $Γ$ , 一个项 $M$ 和一个类型 $τ$ , 判断 $Γ ⊢ M : τ$ 是否成立.
可定型问题, 又称类型重构问题, 指的是判断一个给定项 $M$ 是否是可定型的.
类型居留问题, 又称类型是否为空问题, 指的是对于一个给定的类型 $τ$ , 判断是否存在一个封闭项 $M$ 满足 $⊢ M : τ$ 成立. (那么, 我们称 $τ$ 是非空的, 并拥有居民 $M$ .)

类型居留问题将在第4章讨论, 本节我们先考虑可定型问题和类型检查问题. 第一眼看上去, 似乎判断一个给定项在一个给定环境之中是否拥有一个给定的类型可能要比判断它到底是否拥有类型来得容易. 然而, 这种印象一般而言是错误的. 对于许多类型赋予系统而言, 可定型问题很容易被规约为类型检查问题. 的确, 为了判断一个项 $M$ 是否是可定型的, 其中 $FV (M) = {x_{1}, \dots, x_{n}}$ , 我们可以问是否有 $x_{0} : p ⊢ K x_{0} (λ x_{1} \dots x_{n} . M) : p$ 而这就将可定型问题化为了类型检查问题. 实际上, 在简单类型的情况下, 这两者是等价的 (练习3.11), 尽管将后一个问题规约为前一个问题就不那么简单了. 但是, 对于某些类型赋予系统, 这两个问题并非等价: 比较一下命题13.4.3和定理13.4.4.

现在我们展示可定型问题是如何能够被规约为仅包含二元函数符号 $\to$ 的签名上的合一 (unification) 的. 这个签名上的项被视为与简单类型是等同的. 对于每个项 $M$ 我们根据归纳定义

一个方程组 $E_{M}$ ;
一个类型 $τ_{M}$ .

想法如下:

E_{M}

有解当且仅当

M

是可定型的, 而

τ_{M}

是

M

的 (非形式化的) 类型的模式. 出现在

E_{M}

中的类型变量 (未知元) 分为两种: 其中一些对应于

M

的自由变量

x

的类型, 记作

p_{x}

, 而其他变量是辅助性的.

定义3.2.2.

如果 $M$ 是一个变量 $x$ , 那么 $E_{M} = \emptyset$ 且 $τ_{M} = p_{x}$ , 其中 $p_{x}$ 是一个新鲜 (fresh) 的类型变量.
令 $M$ 是一个应用 $P Q$ . 首先,

第3.3节 Church风格的简单类型 $λ$ 演算

定义3.3.5.

\begin{matrix} (Var) & Γ, x : τ ⊢ x : τ \\ (Abs) & \frac{Γ, x : σ ⊢ M : τ}{Γ ⊢ (λ x : σ M) : σ \to τ} \\ (App) & \frac{Γ ⊢ M : σ \to τ Γ ⊢ N : σ}{Γ ⊢ (M N) : τ} \end{matrix}

图3.2: Church风格的简单类型lambda演算

第3.4节 Church定型 vs Curry定型

第3.5节正规化

第3.6节 Church-Rosser性质

第3.7节可表达性

第3.8节注记

类型经常被视为一种避免无类型世界中因各种各样的自应用而产生的悖论的方法. 无疑, 悖论给予了20世纪之初创造各种类型理论的动力. 然而, 正如[11, 12]所指出的那样, 在数学中将对象划分为不同的范畴或者"类型"是自然的, 并且远在这些悖论被发现之前.

形式类型论的历史起源于Russell. Chwistek, Ramsey, Hilbert等其他人的工作对于该主题的建立做出了贡献. 对于简单类型论的一份有影响力的呈现由1940年Church的论文[13]给出. 为此Church引入了简单类型lambda演算, 其为他的类型论的核心语言.

组合子逻辑的类型化版本在数年之前由Curry提出, 在1934年的论文[14]中, 尽管Curry肯定在1928年就已经有想法了, 见[20, 21]. Curry完整的"theory of functionality"后来被证明是不一致的[15]但是随即就由[16]修正. 很快类型就成为组合子理论和lambda演算中的标准概念.

之后类型被证明在编程语言中很有用. 就像无类型的 $λ$ 演算为无类型的编程语言提供了基础, 各种类型化的 $λ$ 演算为带有类型的编程语言提供了基础. 实际上, 诸如ML [23]等语言的设计启发了类型检查问题和可定型问题的研究. 然而, 正如[22, pp. 103-104]所指出的那样, 类型重构算法的主要想法可以追溯至1920年代.

第3.9节练习

第4章 Curry-Howard同构

既已在第2章讨论了直觉主义逻辑, 在第3章讨论了带类型的lambda演算, 现在开始我们将关注这二者之间的关系, 也就是Curry-Howard同构.

第4.1节证明和项

第4.2节类型居留

第4.3节并非确切的同构

第4.4节证明正规化

第4.5节和与积

第4.6节证明者怀疑者对话

回忆一下第2章的BHK解释. 我们可以将一个公式的构造的建立过程想象成一个证明者和一个怀疑者之间的对话, 证明者产生构造, 而怀疑者质疑构造是否存在.

证明者1: 我断言 $((p \to p) \to (q \to r \to q) \to s) \to s$ 成立.
怀疑者1: 真的吗? 让我们假设我给了你一个 $(p \to p) \to (q \to r \to q) \to s$ 的构造, 那么你能给我一个 $s$ 的构造吗?
证明者2: 通过将你的构造应用于 $p \to p$ 的一个构造, 然后再将结果应用于 $q \to r \to q$ 的一个构造, 我就能得到你想要的东西.
怀疑者2: 嗯...你做出了两个新的断言. 我最怀疑第一个. 你确定你有 $p \to p$ 的一个构造吗? 假设我给你一个 $p$ 的构造, 你能回我一个 $p$ 的构造吗?
证明者3: 用相同的构造就可以了!

对话自证明者作出断言开始.

第4.7节带有谬的证明者怀疑者对话

第4.8节注记

第4.9节练习

第5章证明作为组合子

之前的章节中我们重点关注了自然演绎证明和 $λ$ 项之间的Curry-Howard同构. 正如我们所看到的, 这个同构联系起了两个世界的许多概念. 本章我们呈现一个相关的另外两种基础概念之间的对应, 即Hilbert风格的证明和组合子逻辑的项.

第5.1节 Hilbert风格的证明

自然演绎在历史上并非形式化证明概念的第一种方式, 它也不是得到最广泛使用的一种. 许多数理逻辑的古典呈现, 例如[], 使用了更传统的Hilbert风格的证明的概念. 通常一个Hilbert风格的证明系统由一集公式 (被称为逻辑公理) 和寥寥几条证明规则构成. 而且, Hilbert风格的证明系统中的形式证明在传统上被定义为公式的序列, 而不是树结构的推导.

本章我们考虑的系统, 正如其他大部分命题逻辑的系统, 仅包含一条证明规则, 其被称为modus ponens或者分离规则: $\frac{φ φ \to ψ}{ψ}$ 因此, 一个Hilbert风格的证明系统可以被视为与其逻辑公理的集合等同. 以下的定义适用于所有这样的命题系统.

定义5.1.1. 一个公式

φ

的一个证明序列 (或者说一个Hilbert风格的证明) 是一个公式的有限序列

ψ_{1}, ψ_{2}, \dots, ψ_{n}

满足

ψ_{n} = φ

, 并且对于所有的

i = 1, \dots, n

要么 $ψ_{i}$ 是一条公理,
要么存在 $j, l < i$ 满足 $ψ_{j} = ψ_{l} \to ψ_{i}$ (即 $ψ_{i}$ 是由 $ψ_{j}$ 和 $ψ_{l}$ 通过modus ponens得到的).

如果存在这样一个证明, 那么公式

φ

就被称为一个定理.

定义5.1.2.

定义5.1.5.

\begin{array}{l} (Id) & Γ, φ ⊢ φ \\ (Ax) & Γ ⊢ φ, 如果 φ 是一条逻辑公理 \\ (MP) & \frac{Γ_{1} ⊢ α Γ_{2} ⊢ α \to β}{Γ_{1}, Γ_{2} ⊢ β} \end{array}

图5.1: Hilbert风格系统的树变体

第5.2节组合子逻辑

Hilbert风格的Curry-Howard等价物该是什么呢?

定义5.2.1. 组合子项的集合

𝒞

定义如下:

所有的对象变量都在 $𝒞$ 之中, 即 $Υ \subseteq 𝒞$ .
常量 $K$ 和 $S$ 都在 $𝒞$ 中.
如果 $G$ 和 $H$ 在 $𝒞$ 中, 那么应用 $(G H)$ 也在 $𝒞$ 中.

第5.3节带类型的组合子

第5.4节组合子 vs lambda项

第5.5节外延性

第5.6节

第5.7节

第5.8节

第6章古典逻辑和控制运算符

在之前的章节中, 我们已经遇到了化身为各种面目的Curry-Howard同构. 每一种都陈述了某个计算性演算和一个形式逻辑系统之间的对应. 到目前为止, 这些形式逻辑系统都是直觉主义的. 例如, 没有一个能够推导在古典的逻辑中可以看到的双重否定消去原理 $\neg \neg φ \to φ$ .
这并非巧合. 事实上, 到大约1990年为止, 许多人相信"并不存在古典逻辑的Curry-Howard同构". 然而, 那个时候Timothy Griffin发现了双重否定消除原理对应于编程语言理论中众所周知的一个控制运算符的定型. 很快这个想法就经由Chet Murthy得到了推广和完善.
本章呈现了这个发现以及它的一些推论, 例如Kolmogorov从古典逻辑到直觉主义逻辑的双重否定嵌入对应于延续传递风格转换.

第6.1节古典命题逻辑

\begin{matrix} Γ, φ ⊢ φ (Ax) \\ \frac{Γ, φ ⊢ ψ}{Γ ⊢ φ \to ψ} (\to I) \frac{Γ ⊢ φ \to ψ Γ ⊢ φ}{Γ ⊢ ψ} (\to E) \\ \frac{Γ, φ \to ⊥ ⊢ ⊥}{Γ ⊢ φ} (\neg E) \end{matrix}

图6.1: 古典命题演算

例子6.1.2.

以下是公式 $(φ \to ψ) \to (\neg φ \to ψ) \to ψ$ ("分类讨论证明") 的一个推导, 令 $Γ = {φ \to ψ, \neg φ \to ψ, \neg ψ}$ . $\frac{\frac{\frac{\frac{Γ ⊢ \neg ψ \frac{Γ ⊢ \neg φ \to ψ \frac{\frac{Γ, φ ⊢ \neg ψ \frac{Γ, φ ⊢ φ \to ψ Γ, φ ⊢ φ}{Γ, φ ⊢ ψ}}{Γ, φ ⊢ ⊥}}{Γ ⊢ \neg φ}}{Γ ⊢ ψ}}{Γ ⊢ ⊥}}{φ \to ψ, \neg φ \to ψ ⊢ ψ}}{φ \to ψ ⊢ (\neg φ \to ψ) \to ψ}}{⊢ (φ \to ψ) \to (\neg φ \to ψ) \to ψ}$
以下是Peirce律的推导, 令 $Γ = {(φ \to ψ) \to φ}$ . $\frac{\frac{\frac{Γ, \neg φ ⊢ \neg φ \frac{Γ, \neg φ ⊢ (φ \to ψ) \to φ \frac{\frac{\frac{Γ, \neg φ, φ, \neg ψ ⊢ \neg φ Γ, \neg φ, φ, \neg ψ ⊢ φ}{Γ, \neg φ, φ, \neg ψ ⊢ ⊥}}{Γ, \neg φ, φ ⊢ ψ}}{Γ, \neg φ ⊢ φ \to ψ}}{Γ, \neg φ ⊢ φ}}{Γ, \neg φ ⊢ ⊥}}{Γ ⊢ φ}}{⊢ ((φ \to ψ) \to φ) \to φ}$

第6.2节 $λ μ$ 演算

第6.3节

第6.4节逻辑嵌入和CPS转换

在直觉主义逻辑之中解释古典逻辑, 被称为逻辑嵌入, 自1920年代已被研究. 本节我们研究这样一个嵌入, 其被称为Kolmogorov双重否定转换, 它有一个有趣的计算性解释.

定义6.4.1. (Kolmogorov转换). 按如下方式定义一个转换, 其中

α

遍历原子命题:

\begin{array}{l} k (α) & = & \neg \neg α \\ k (φ \to ψ) & = & \neg \neg (k (φ) \to k (ψ)) \end{array}

而且,

k (Γ) = {k (φ) | φ \in Γ}

第6.5节古典证明者怀疑者对话

第6.6节纯推论片段

第6.7节合取与析取

第6.8节注记

第6.9节练习

第7章相继式演算

第7.1节 Gentzen的相继式演算LK

第7.2节 LK的片段 vs 自然演绎

第7.3节 Gentzen的Hauptsatz

第7.4节切消 vs 正规化

第7.5节 Lorenzen对话

第7.6节注记

第7.7节练习

第8章一阶逻辑

第8.1节一阶逻辑的句法

8.1.1. 定义.

原子公式要么是逻辑常量 $⊥$ , 要么是具有形式 $(r t_{1} \dots t_{n})$ 的表达式, 其中 $r$ 是 $Σ$ 中一个 $n$ 元关系符号, 而 $t_{1}, \dots, t_{n}$ 是 $Σ$ 上的代数项. 特别地, 每个零元关系符号都构成了一个原子公式.
Σ上的一阶公式的集合ΦΣ是满足以下条件的最小集合:
- 所有的原子公式都在 $Φ_{Σ}$ 中;
- 如果 $φ, ψ \in Φ_{Σ}$ , 那么 $(φ \to ψ), (φ \lor ψ), (φ \land ψ) \in Φ_{Σ}$ ;
- 如果 $φ \in Φ_{Σ}$ 并且 $a$ 是一个独立变量, 那么 $\Rightarrow a φ, \exists a φ \in Φ_{Σ}$ .
和通常一样, ¬φ是φ→⊥的缩略, φ↔ψ是(φ→ψ)∧(ψ→φ)的缩略.
公式φ的自由变量集FV⁡(φ)的定义如下:
- $FV (r t_{1} \dots t_{n}) = FV (t_{1}) \cup \dots \cup FV (t_{n})$ ;
- $FV (φ \to ψ) = FV (φ \lor ψ) = FV (φ \land ψ) = FV (φ) \cup FV (ψ)$ ;
- $FV (\Rightarrow a φ) = FV (\exists a φ) = FV (φ) - {a}$ .
也就是说, 量化符号⇒a和∃a绑定了其作用域之中的a. 仅是绑定变量不同的公式是等同的. 如果Γ是一集公式, 那么FV⁡(Γ)=⋃{FV⁡(γ)|γ∈Γ}.
一个公式是开的当且仅当其不含有量化符号. 一个句子, 也被称为封闭公式, 是不含有自由变量的公式. 如果 $a_{1}, \dots, a_{k}$ 是 $φ$ 的(以某种固定顺序列出的)自由变量, 那么句子 $\Rightarrow a_{1} \dots \Rightarrow a_{k} φ$ 被称为 $φ$ 的全称闭包.

从以上定义可以看出一个公式不仅仅是一个表达式, 而是一个表达式的

α

等价类, 非常类似于lambda项, 见第1.2节. 我们处理公式上的

α

变换的方式为简单性而妥协了精确性. 为了给出这个定义的一个更加准确的陈述, 我们需要类似于第1.2节的讨论, 诸如预公式的概念需要进行刻画. 我们相信读者能够在必要时重构形式化的缺失部分.

实际上, 在逻辑学中将alpha等价的一阶公式视为等同并非惯例. 典型的情况是, 这样的公式被认为是不同的, 尽管相对于任何合理的语义而言它们应该是等价的, 并且在任何合理的证明系统中我们应该能够从一个推出另一个. 但是, 为了呈现的一致性, 我们更愿意在本书讨论的所有逻辑和lambda演算中都默认相对于各种变量绑定的alpha等价性.

8.1.2. 约定. 用于避免括号的

8.1.3. 定义. 替换一个独立变量以一个项, 记作

φ [a ≔ t]

, 定义如下:

$⊥ [a ≔ t] = ⊥$ ;
$(r t_{1} \dots t_{n}) [a ≔ t] = (r t_{1} [a ≔ t] \dots t_{n} [a ≔ t])$ ;
$(φ \circ ψ) [a ≔ t] = (φ [a ≔ t] \circ ψ [a ≔ t])$ , 其中 $\circ \in {\to, \lor, \land}$ ;
$(\nabla b φ) [a ≔ t] = (\nabla b φ [a ≔ t])$ , 其中 $\nabla \in {\Rightarrow, \exists}$ , $b \neq a$ , $b \notin FV (t)$ .

同时替换也可定义, 记作

φ [a_{1}, \dots, a_{n} ≔ t_{1}, \dots, t_{n}]

, 其方式类似于我们对于lambda项所做的 (见定义1.2.21).

8.1.4. 约定.

第8.2节非形式化的语义

命题公式的Brouwer-Heyting-Kolmogorov解释 (第2章) 也可被扩展至一阶逻辑. 对此, 我们需要假定独立变量和代数项在特定的对象的论域中被解释. 既然谓词逻辑表达了这样的对象的性质, 假定解释域非空是很自然的, 即至少存在一个这样的对象. [原注: 在其他牵涉量化的逻辑系统之中, 这种假设并非先验. 如果我们量化于复合对象 (例如证明) 之上, 那么期望某些量化的论域为空也是合理的. 见评注13.5.1.]

和第2章一样, 原子的解释未加刻画.

第8.3节证明系统

第8.4节古典语义

第8.5节直觉主义逻辑的代数语义

第8.6节 Kripke语义

第8.7节 lambda演算

第8.8节不可判定性

第8.9节注记

第8.10节练习

第9章一阶算术

第9.1节算术的语言

第9.2节 Peano算术

第9.3节 Gödel的定理

第9.4节

第9.5节 Heyting算术

第9.6节 Kleene的可实现性解释

第9.7节注记

第9.8节练习

第10章 Gödel的系统T

第10.1节从Heyting算术到系统T

第10.2节句法

第10.3节

第10.4节

第10.5节

第10.6节

第11章二阶逻辑和多态

第11.1节二阶命题逻辑

第11.2节多态lambda演算 (系统F)

第11.3节表达力

第11.4节 Curry风格的多态

第11.5节强规范化

第11.6节居留问题

第11.7节高阶多态

第11.8节注记

第11.9节练习

第12章二阶算术

第13章依赖类型

第14章纯类型系统和 $λ$ 立方

附录A 数学背景

第A.1节集合论

第A.2节代数与合一

一个签名是一族函数与关系符号, 其中每个都拥有固定的元数 (可能为零). 零元符号被称为常量. 若不加另外说明, 签名则被认为是有限的.

假定有一个固定的独立变量的无限集合 ${a_{0}, a_{1}, \dots}$ . 一个签名 $Σ$ 上的一个代数项 (或者就称为项) 要么是一个独立变量, 要么是具有形式 $(f t_{1} \dots t_{n})$ 的表达式, 其中 $f$ 是一个 $n$ 元函数符号, 而 $t_{1}, \dots, t_{n}$ 是项. 当书写项的时候, 我们经常省略最外面的括号. 符号 $FV (t)$ 代表了所有出现在项 $t$ 中的独立变量的集合. 项 $t$ 是封闭的当且仅当 $FV (t) = \emptyset$ .

一个代数项的形式定义牵扯函数符号的前缀应用. 当然, 从传统上来说一些二元函数符号是以中缀风格书写的, 正常情况下我们就这么做. 我们最喜爱的签名仅包含(中缀)箭头作为唯一的符号. 不难看出这个签名上的代数项可以被视为与简单类型等同, 或者你喜欢的话也可以说是与推论公式等同.

本节我们仅考虑代数签名, 即不包含关系符号的签名. 这样一个签名 $Σ = {f_{1}, \dots, f_{n}}$ (其中 $f_{i}$ 的元数是 $r_{i}$ ) 上的一个代数是一个集合 $A$ 以及函数 $f_{i}^{A} : A^{r_{i}} \to A$ , 即一个系统 $𝒜 = ⟨ A, f_{1}^{A}, \dots, f_{n}^{A} ⟩$ .

第A.3节部分递归函数

附录B 部分练习的解答和提示

参考文献

[1] M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. Levy. Explicit substitutions. Journal of Functional Programming, 1(4):375-416, 1991.

[2] A. Abel and T. Altenkirch. A predicative strong normalisation proof for a

λ

-calculus with interleaving inductive types. In T. Coquand, P. Dybjer, B. Nordström, and J. Smith, editors, Types for Proofs and Programs, International Workshop TYPES'99, volume 1956 of Lecture Notes in Computer Science, pages 21-40. Springer-Verlag, 2000.

[3] H. Abelson and G.J. Sussman with J. Sussman. The Structure and Interpretation of Computer Programs. MIT Press, second edition, 1996.

[4] S. Abramsky. Computational interpretations of linear logic. Theoretical Computer Science, lll(l-2):3-57, 1993.

[5] S. Abramsky and R. Jagadeesan. Games and full completeness for multiplicative linear logic. Journal of Symbolic Logic, 59(2):543-574, 1994.

[6] Z. Adamowicz and P. Zbierski. Logic of Mathematics. A Modern Course of Classical Logic. John Wiley & Sons, 1997.

[7] A. Appel. Compiling with Continuations. Cambridge University Press, 1992.

[8] H. Barendregt and T. Nipkow, editors. Types for Proofs and Programs, International Workshop TYPES'93, volume 806 of Lecture Notes in Computer Science. Springer-Verlag, 1994.

[9] A. Church. A set of postulates for the foundation of logic. Annals of Mathematics, 33(2):346-366, 1932.

[10] A. Church. A set of postulates for the foundation of logic. (Second paper.) Annals of Mathematics, 34(4):839-864, 1933.

[11] R.O. Gandy. The simple theory of types. In R.O. Gandy and J.M.E. Hyland, editors, Logic Colloquium 76, volume 87 of Studies in Logic and the Foundations of Mathematics, pages 173-181. North-Holland, 1977.

[12] F. Kamareddine, T. Laan, and R. Nederpelt. Types in logic and mathematics before 1940. Bulletin of Symbolic Logic, 8(2):185-245, 2002.

[13] A. Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5(2):56-68, 1940.

[14] H.B. Curry. Functionality in combinatory logic. Proceedings of the National Academy of Science USA, 20(ll):584-590, 1934.

[15] H.B. Curry. The inconsistency of the full theory of combinatory functionality. Journal of Symbolic Logic, 20(1):91, 1955.

[16] H.B. Curry. Consistency of the theory of functionality. Journal of Symbolic Logic, 21(1):110, 1956.

[17] P. Graham. ANSI Common Lisp. Prentice-Hall, 1995.

[18] F. Pfenning and C. Elliot. Higher-order abstract syntax. In Programming Language Design and Implementation, pages 199-208. ACM Press, 1988.

[19] A. Pitts. Nominal logic: A first order theory of names and binding. Information and Computation, 186(2):165-193, 2003.

[20] J.P. Seldin. Curry's anticipation of the types used in programming languages. In Proceedings of the Annual Meeting of the Canadian Society for History and Philosophy of Mathematics, Toronto, 24-26 May 2002, pages 148-163, 2003.

[21] J.P. Seldin. Church and Curry: The lambda calculus and combinatory logic. In Gabbay and Woods [159]. To appear.

[22] J.R. Hindley. Basic Simple Type Theory, volume 42 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1997.

[23] L.C. Paulson. ML for the Working Programmer. Cambridge University Press, second edition, 1996.

[24] R. Pollack. Closure under alpha-conversion. In Barendregt and Nipkow [8], pages 313-332.

[25] D. Prawitz. Natural Deduction. A Proof Theoretical Study. Almqvist & Wiksell, 1965.

Curry-Howard同构讲义

前言

第1章 无类型λ演算

第1.1节 温和的引入

第1.2节 预项和λ项

第1.3节 规约

第1.4节 Church-Rosser定理

第1.5节 最左规约是正规化

第1.6节 永恒规约和守恒定理

第1.7节 可表达性和不可判定性

第1.8节 注记

第1.9节 练习

第2章 直觉主义逻辑

第2.1节 BHK解释

第2.2节 自然演绎

第2.3节 古典逻辑的代数语义

第2.4节 Heyting代数

第2.5节 Kripke语义

第2.6节 推论片段

第2.7节 注记

第2.8节 练习

第3章 简单类型λ演算

第3.1节 Curry风格的简单类型λ演算

第3.2节 类型重构算法

第3.3节 Church风格的简单类型λ演算

第3.4节 Church定型 vs Curry定型

第3.5节 正规化

第3.6节 Church-Rosser性质

第3.7节 可表达性

第3.8节 注记

第3.9节 练习

第4章 Curry-Howard同构

第4.1节 证明和项

第4.2节 类型居留

第4.3节 并非确切的同构

第4.4节 证明正规化

第4.5节 和与积

第4.6节 证明者怀疑者对话

第4.7节 带有谬的证明者怀疑者对话

第4.8节 注记

第4.9节 练习

第5章 证明作为组合子

第5.1节 Hilbert风格的证明

第5.2节 组合子逻辑

第5.3节 带类型的组合子

第5.4节 组合子 vs lambda项

第5.5节 外延性

第5.6节

第5.7节

第5.8节

第6章 古典逻辑和控制运算符

第6.1节 古典命题逻辑

第6.2节 λμ演算

第6.3节

第6.4节 逻辑嵌入和CPS转换

第6.5节 古典证明者怀疑者对话

第6.6节 纯推论片段

第6.7节 合取与析取

第6.8节 注记

第6.9节 练习

第7章 相继式演算

第7.1节 Gentzen的相继式演算LK

第7.2节 LK的片段 vs 自然演绎

第7.3节 Gentzen的Hauptsatz

第7.4节 切消 vs 正规化

第7.5节 Lorenzen对话

第7.6节 注记

第7.7节 练习

第8章 一阶逻辑

第8.1节 一阶逻辑的句法

第8.2节 非形式化的语义

第8.3节 证明系统

第8.4节 古典语义

第8.5节 直觉主义逻辑的代数语义

第8.6节 Kripke语义

第8.7节 lambda演算

第8.8节 不可判定性

第8.9节 注记

第8.10节 练习

第9章 一阶算术

第1章无类型 $λ$ 演算

第1.1节温和的引入

第1.2节预项和 $λ$ 项

第1.3节规约

第1.5节最左规约是正规化

第1.6节永恒规约和守恒定理

第1.7节可表达性和不可判定性

第1.8节注记

第1.9节练习

第2章直觉主义逻辑

第2.2节自然演绎

第2.3节古典逻辑的代数语义

第2.6节推论片段

第2.7节注记

第2.8节练习

第3章简单类型 $λ$ 演算

第3.1节 Curry风格的简单类型 $λ$ 演算

第3.2节类型重构算法

第3.3节 Church风格的简单类型 $λ$ 演算

第3.5节正规化

第3.7节可表达性

第3.8节注记

第3.9节练习

第4.1节证明和项

第4.2节类型居留

第4.3节并非确切的同构

第4.4节证明正规化

第4.5节和与积

第4.6节证明者怀疑者对话

第4.7节带有谬的证明者怀疑者对话

第4.8节注记

第4.9节练习

第5章证明作为组合子

第5.2节组合子逻辑

第5.3节带类型的组合子

第5.4节组合子 vs lambda项

第5.5节外延性

第6章古典逻辑和控制运算符

第6.1节古典命题逻辑

第6.2节 $λ μ$ 演算

第6.4节逻辑嵌入和CPS转换

第6.5节古典证明者怀疑者对话

第6.6节纯推论片段

第6.7节合取与析取

第6.8节注记

第6.9节练习

第7章相继式演算

第7.4节切消 vs 正规化

第7.6节注记

第7.7节练习

第8章一阶逻辑

第8.1节一阶逻辑的句法

第8.2节非形式化的语义

第8.3节证明系统

第8.4节古典语义

第8.5节直觉主义逻辑的代数语义

第8.8节不可判定性

第8.9节注记

第8.10节练习

第9章一阶算术

第9.1节算术的语言

第9.7节注记

第9.8节练习

第10.1节从Heyting算术到系统T

第10.2节句法

第11章二阶逻辑和多态

第11.1节二阶命题逻辑

第11.2节多态lambda演算 (系统F)

第11.3节表达力

第11.5节强规范化

第11.6节居留问题

第11.7节高阶多态

第11.8节注记

第11.9节练习

第12章二阶算术

第13章依赖类型

第14章纯类型系统和 $λ$ 立方

第A.1节集合论

第A.2节代数与合一

第A.3节部分递归函数