目录 1
1．引言 1
1.1 类型论用于程序设计 3
1.2 构造数学 6
1.3 类型论的不同表述系统 7
1.4 程序逻辑的实现 8
2．集合，命题和规格说明的等同 10
2.1 命题作为集合 10
2.2 命题作为任务和程序的规格说明 12
3．表达式与定义相等性 14
3.1 作用 14
3.2 抽象 15
3.3 组合 16
3.4 选取 17
3.5 带名分部的组合 17
3.6 相关度 17
3.7 定义 20
3.8 什么是具某个相关度的表达式的定义 20
3.9 两个表达式之间相等性的定义 21
第一部分 多型集合 25
4．判断形式的语义 25
4.1 范畴判断 27
4.2 带一个前提的假设判断 29
4.3 带多个前提的假设判断 31
5．一般规则 34
5.3 相等性规则 36
5.1 前提 36
5.2 命题作为集合 36
5.4 集合规则 37
5.5 替代规则 37
6．枚举集合 40
6.1 永假与空集合 42
6.2 单元素集合与真命题 42
6.3 集合Bool 43
7．集合族的笛氏积 45
7.1 形式规则及其论证 47
7.2 另一种原始非典则形式 48
7.3 由Ⅱ集合定义的常元 51
8.1 内涵相等性 54
8．相等性集合 54
8.2 外延相等性 57
8.3 Ⅱ-集合元素的η-相等性 59
9．自然数 61
10．列表 65
11．两个集合的笛氏积 70
11.1 形式规则 70
11.2 函数的外延相等性 72
12．两个集合的不交和 75
13．集合族的不交和 77
14．小集合之集合（第一全域） 79
14.1 形式规则 79
14.2 消去规则 87
15．良序 94
15.1 用良序表示归纳定义集合 98
16．一般树 99
16.1 形式规则 100
16.2 与良序集合构造子的关系 102
16.3 树集合构造子的异体 104
16.4 不同树集合的例子 104
第二部分 子集合 111
17．基本集合理论中的子集合 111
18．子集合理论 114
18.1 无前提判断 114
18.2 假设判断 116
18.3 子集合理论中的一般规则 119
18.4 子集合理论中的命题常元 120
18.5 由概括形成子集合 122
18.6 子集合理论中单独的成集算子 124
18.7 带全域的子集合 127
第三部分 单型集合 135
19．类型 135
19.1 类型与对象 136
19.2 集合与元素的类型 137
19.3 类型族 137
19.4 一般规则 139
19.5 前提 140
19.6 函数类型 141
20.1 Ⅱ集合 144
20．用类型定义集合 144
20.2 ∑集合 146
20.3 不交和 146
20.4 相等性集合 147
20.5 有穷集合 148
20.6 自然数 148
20.7 列表 149
第四部分 例子 153
21．杂例 153
21.1 除以2 153
21.2 偶或奇 157
21.3 Boo1仅有元素true和false 159
21.4 可判定谓词 160
21.5 强消去规则 162
22．程序推导 164
22.1 程序推导方法 164
22.2 分割问题 168
23．抽象数据类型规格说明 178
23.1 参数模 181
23.2 关于带可计算相等性集合的模 181
参考文献 183
附录A 常元及其相关度 192
A.1 集合论中的原始常元 192
A.2 集合常元 193
附录B 操作语义 194
B.1 非典则常元的求值规则 194