第0章 读者须知 1
第一部份 基本概念 3
第1章 介绍 3
1.1 λ-演算概况 3
1.2 完备偏序和Scott拓扑 7
1.3 练习题 14
第2章 换位 17
2.1 λ-项和换位 17
2.2 理论的若干变种 26
2.3 第二部份概貌 32
2.4 练习题 35
第3章 归约 37
3.1 归约的概念 37
3.2 β-归约 43
3.3 η-归约 46
3.4 第三部份概貌 50
3.5 练习题 54
第4章 理论 57
4.1 λ-理论 57
4.2 第四部份概貌 62
4.3 练习题 63
第5章 模型 65
5.1 组合代数 66
5.2 λ-代数和λ-模型 69
5.3 语法模型 77
5.4 在具体笛卡尔闭范畴上的模型 79
5.5 在(任意)笛卡尔闭范畴上的模型 81
5.6 其他模型描述;范畴模型 89
5.7 第五部份概貌 93
5.8 练习题 97
第二部份 换位 100
第6章 经典λ-演算 100
6.1 不动点组合子 100
6.2 标准组合子 101
6.3 λ-可定义性 102
6.4 数系 105
6.5 再谈不动点;Godel数 106
6.6 不可判定性 108
6.7 自身表达句和递归定理 109
6.8 练习题 110
第7章 组合理论 113
7.1 组合逻辑 113
7.2 CL-归约 115
7.3 CL和λ之间的关系 116
7.4 练习题 120
第8章 经典λ-演算(续) 123
8.1 基和枚举 123
8.2 一致性;无穷序列 125
8.3 可解性;首范式 127
8.4 偏函数的可定义性 132
8.5 练习题 135
第9章 λI-演算 137
9.1 广义性 137
9.2 可定义性 138
9.3 组合子 141
9.4 可解性 145
9.5 练习题 154
第10章 Bohm树 156
10.1 基本概念 156
10.2 比较Bohm树;∧上的树拓扑 166
10.3 超Bohm技术 178
10.4 项的可分离性 185
10.5 λI-演算中的可分离性 189
10.6 练习题 197
第三部份 归约 200
第11章 基本定理 200
11.1 Church-Rosscr定理 200
11.2 展开的有限性 205
11.3 λI-守恒定理 212
11.4 标准化 214
11.5 练习题 217
第12章 强等价归约 219
12.1 归约图 219
12.2 CR和FD!的加强形式 226
12.3 标准化的加强形式 230
12.4 练习题 235
第13章 归约对策 236
13.1 对策分类 236
13.2 能行正规化和同归对策 237
13.3 递归CR对策 242
13.4 能行永久对策 245
13.5 最优对策 250
13.6 练习题 253
第14章 加标归约 256
14.1 强正规化 256
14.2 应用 261
14.3 连续性 265
14.4 序列性和稳定性 271
14.5 练习题 277
第15章 其它的一些归约 279
15.1 BH-归约 279
15.2 BHΩ-归约 282
15.3 δ-归约 292
15.4 练习题 297
第四部份 理论 300
第16章 灵敏理论 300
16.1 К—理论 300
16.2 К*—理论 304
16.3 2ψо灵敏理论 307
16.4 В—理论 310
16.5 练习题 313
第17章 其他λ理论 314
17.1 半灵敏性和r.c.理论 314
17.2 ω—理论 318
17.3 λη的ω—规则部份有效性 324
17.4 ω—规则和Кη 332
17.5 练习题 337
第五部份 模型 339
第18章 模型的构造 339
18.1 图模型Pω 339
18.2 模型D∞ 345
18.3 模型В 352
18.4 练习题 356
第19章 模型的局部结构 362
19.1 Pω的局部结构 362
19.2 D∞的局部结构 367
19.3 连续的λ-模型 370
19.4 练习题 372
第20章 模型的整体结构 374
20.1 外延性;范畴性 374
20.2 区域性质 376
20.3 不可定义性的几个结果 378
20.4 局部与整体可表示性的对比 379
20.5 模型上的树拓扑 382
20.6 练习题 385
第21章 组合群 388
21.1 组合半群 388
21.2 可逆性的特征 389
21.3 G(λη)和G(H*)群 398
21.4 练习题 402
参考文献 404