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}

. 然而, 数学家使用这样的记号来指称作为数学对象的函数 (被定义为序对的集合). 与之相对地,

λ

项是形式表达式 (字符串), 从直觉上说, 以最纯粹的形式表达了函数和函数的应用. 因此, 一个

λ

项是如下形式之一:

举个例子,

λ

项

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)$ 也是一个预项.

所有预项构成的集合记作

Λ^{-}

预项, 正如上面所定义的那样, 是完全括号化的. 如预项

(λ 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]

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

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.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$ .

[译注: 后三条是在说

=_{α}

是一个兼容关系.]

定义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.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.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.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.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.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.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.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章直觉主义逻辑

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

第2.1节 BHK解释

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

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

PV

, 我们将公式的集合

Φ

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

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

变量和

⊥

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

φ

的子公式是

φ

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

也就是说, 我们基本的联结词是: 推出

\to

, 析取

\lor

, 合取

\land

, 以及常量

⊥

(谬). 否定

\neg

和等价

\leftrightarrow

是缩略形式, 常量

⊤

(真) 也是如此:

例子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解释.

例子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$ .

第2.2节自然演绎

为了形式化直觉主义命题逻辑, 我们定义了一个被称为自然演绎的证明系统, 用

NJ (\to, ⊥, \land, \lor)

表示, 或者就简单地记作

NJ

定义2.2.1.

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

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

定义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.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.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.

定义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 ⊨ φ

, 记

ℬ ⊨ φ

显然, 这种布尔代数语义是通常二值语义的一种泛化. 的确, 一个公式

φ

是一个古典重言当且仅当

𝔹 ⊨ φ

. 实际上, 这种泛化不是本质性的.

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

ℬ

有

ℬ ⊭ φ

. 根据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代数

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

Γ

我们有:

第2.5节 Kripke语义

定义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.6节推论片段

第2.7节注记

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

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

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

第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}

一个形式为

M : τ \to σ

的类型赋予当然可以被解释为"

M

是一个以

τ

为定义域

σ

为陪域的函数". 但是我们必须明白这里对于"定义域"和"陪域"的理解不是集合论性质的. 在Curry风格的类型化演算中, 类型被更适切地描述为(由项满足的)谓词或者规格 (specification) 而不是集合论性质的函数空间. 在集合论中

f : A \to B

的含义为

f

的参数恰是

A

的元素, 而所有的值都必须属于

B

. 与之相对地,

M : τ \to σ

仅意味着将

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.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.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

我们根据归纳定义

定义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.2节组合子逻辑

定义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节古典命题逻辑

例子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.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章二阶逻辑和多态

第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 部分练习的解答和提示

参考文献

[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.

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章二阶逻辑和多态

第12章二阶算术

第13章依赖类型

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

第A.1节集合论

第A.2节代数与合一

第A.3节部分递归函数