第1章 引言 1
1.1 模型程序设计语言 1
1.2 λ记法 2
1.3 等式，归约和语义 4
1.3.1 公理语义 4
1.3.2 操作语义 5
1.3.3 指称语义 5
1.4 类型和类型系统 6
1.5 记法和数学约定 8
1.6 集合论基础知识 9
1.6.1 基础 9
1.6.2 关系和函数 12
1.7 语法和语义 14
1.7.1 目标语言和元语言 14
1.7.2 文法 14
1.7.3 词法分析和语法分析 15
1.7.4 数学解释示例 17
1.8 归纳法 18
1.8.1 自然数归纳法 18
1.8.2 表达式和证明上的归纳法 21
1.8.3 良基归纳法 26
第2章 PCF语言 30
2.1 引言 30
2.2 PCF语法 31
2.2.1 概述 31
2.2.2 布尔值和自然数 31
2.2.3 配对及其函数 34
2.2.4 声明和语法惯用形 37
2.2.5 递归和不动点算子 40
2.2.6 PCF语法总结和精选实例 43
2.3 PCF程序及其语义 45
2.3.1 程序和结果 45
2.3.2 公理语义 46
2.3.3 指称语义 48
2.3.4 操作语义 49
2.3.5 由各种形式语义定义的等价关系 51
2.4 PCF归约和符号解释程序 52
2.4.1 不确定性规约 52
2.4.2 归约策略 56
2.4.3 最左优先和懒归约策略 57
2.4.4 并行归约 60
2.4.5 积极PCF 61
2.5 PCF编程样例，表达能和限度 64
2.5.1 记录和n元组 64
2.5.2 搜索自然数 65
2.5.3 迭代和尾递归 67
2.5.4 完全递归函数 70
2.5.5 部分递归函数 72
2.5.6 并行操作的不可定义性 75
2.6 PCF的变体和扩展 81
2.6.1 扩展的概述 81
2.6.2 unit与求和类型 81
2.6.3 递归类型 84
2.6.4 提升类型 88
第3章 泛代数及代数数据类型 97
3.1 引言 97
3.2 代数规范概述 98
3.3 代数，基调和项 99
3.3.1 代数 99
3.3.2 代数项语法 99
3.3.3 代数和项的解释 101
3.3.4 代入引理 104
3.4 等式，可靠性和完备性 105
3.4.1 等式 105
3.4.2 项代数和代入 106
3.4.3 语义蕴涵和等式证明系统 107
3.4.4 完备性的形式 115
3.4.5 同余，商和演绎完备性 115
3.4.6 非空类子和最小模型性质 118
3.5 同态和始代数 119
3.5.1 同态和同构 119
3.5.2 始代数 121
3.6 代数数据类型 125
3.6.1 规范和数据抽象 125
3.6.2 始代数语义和数据类型归纳 127
3.6.3 例子和错误值 131
3.6.4 错误值的其他解决方法 135
3.7 重写系统 135
3.7.1 基本定义 135
3.7.2 汇聚性和可证相等性 138
3.7.3 终止性 140
3.7.4 临界对 143
3.7.5 左线性非重叠重写系统 148
3.7.6 局部汇聚，终止和完备性 151
3.7.7 代数数据类型的应用 153
第4章 简单类型化λ演算 156
4.1 引言 156
4.2 类型 157
4.2.1 语法 157
4.2.2 类型的解释 157
4.3 项 159
4.3.1 上下文相关语法 159
4.3.2 λ→项的语法 160
4.3.3 带有积、和的项及其相关类型 165
4.3.4 公式与类型的对应 166
4.3.5 类型求取算法 169
4.4 证明系统 171
4.4.1 等式和理论 171
4.4.2 归约规则 178
4.4.3 具有附加规则的归约 180
4.4.4 一致性和保持性的证明论方法 182
4.5 Henkin模型，可靠性和完备性 186
4.5.1 通用模型和项的含义 186
4.5.2 作用结构，外延性和框架 187
4.5.3 环境模型条件 188
4.5.4 类型和等式可靠性 192
4.5.5 不带空类型的Henkin模型的完备性 195
4.5.6 带有空类型的完备性 197
4.5.7 组合子和组合模型条件 198
4.5.8 组合代数和λ代数 200
4.5.9 其他类型的Henkin模型 201
5.2 域论模型和不动点 204
5.2.1 递归定义和不动点算子 204
5.1 引言 204
第5章 类型化λ演算模型 204
5.2.2 完全偏序，提升和笛卡儿积 206
5.2.3 连续函数 209
5.2.4 不动点和完全连续层次 212
5.2.5 PCF的CPO模型 218
5.3 不动点归纳 223
5.4.1 近似原理和计算适当性 227
5.4 计算适当性和完全抽象 227
5.4.2 带并行操作的PCF的完全抽象 231
5.5 递归理论模型 237
5.5.1 引言 237
5.5.2 朴素集 239
5.5.3 完全递归层次 241
5.6 部分等价关系和递归 244
5.6.1 类型的部分等价关系解释 244
5.6.2 部分组合代数的一般化 246
5.6.3 提升，部分函数和递归 249
5.6.4 递归和固有序 251
5.6.5 有效CPO的提升，积和函数空间 256
第6章 命令式程序 260
6.1 引言 260
6.2 while程序 261
6.2.1 L值和R值 261
6.2.2 while程序的语法 262
6.3 操作语义 263
6.3.1 表达式中的基本符号 263
6.3.2 位置和存储 263
6.3.3 表达式求值 264
6.3.4 命令的执行 265
6.4 指称语义 269
6.4.1 带有存储的类型化λ演算 269
6.4.2 语义函数 271
6.4.3 操作语义和指称语义的等价性 275
6.5.1 一阶和部分正确性断言 277
6.5 关于while程序的前-后断言 277
6.5.2 证明规则 278
6.5.3 可靠性 283
6.5.4 相对完备性 284
6.6 附加程序构造的语义 288
6.6.1 概述 288
6.6.2 带有局部变量的模块 288
6.6.3 过程 294
6.6.4 组合程序块和过程声明 295
第7章 范畴和递归类型 299
7.1 引言 299
7.2 笛卡儿闭范畴 299
7.2.1 范畴论与类型化语言 299
7.2.2 范畴，函子和自然变换 300
7.2.3 笛卡儿闭范畴的定义 307
7.2.4 可靠性和项的解释 314
7.2.5 Henkin模型作为CCC 325
7.2.6 含义函数的范畴刻划 327
7.3 Kripkeλ模型和函子范畴 329
7.3.1 概述 329
7.3.2 可能世界 329
7.3.3 作用结构 329
7.3.4 外延性，组合子和函子范畴 331
7.3.5 环境和项的含义 333
7.3.6 可靠性和完备性 335
7.3.7 Kripkeλ模型作为笛卡儿闭范畴 336
7.4 递归类型的域模型 338
7.4.1 一个启示性的例子 338
7.4.2 图，锥和极限 341
7.4.3 F代数 343
7.4.4 ω链和初始F代数 345
7.4.5 O范畴和嵌入 348
7.4.6 余极限和O余极限 350
7.4.7 局部连续函子 353
7.4.8 该通用方法的例子 355
第8章 逻辑关系 359
8.1 逻辑关系概述 359
8.2 作用性结构上的逻辑关系 359
8.2.1 逻辑关系的定义 359
8.2.2 基本引理 361
8.2.3 部分函数和模型的理论 365
8.2.4 逻辑部分等价关系 366
8.2.5 商和外延性 366
8.3 证明论的结果 369
8.3.1 Henkin模型的完备性 369
8.3.2 正则化 371
8.3.3 汇聚和其他归约性质 373
8.3.4 有fix和附加操作的归约 377
8.4.1 部分满射和完整的古典层次 385
8.4 部分满射和特殊模型 385
8.4.2 完整的递归层次 386
8.4.3 完整的连续层次 388
8.5 表示独立性 389
8.5.1 动机 389
8.5.2 实例语言 390
8.5.3 普通的表示独立性 392
8.6 逻辑关系的推广 393
8.6.1 引言 393
8.6.2 启示性例子：全偏序和Kripke模型 394
8.6.3 寻求原像体和关系 399
8.6.4 与逻辑关系的比较 402
8.6.5 一般情形和应用到特殊范畴 404
9.1.2 类型作为函数实参 407
9.1.1 概述 407
9.1 引言 407
第9章 多态与模块性 407
9.1.3 通积与通和 411
9.1.4 类型作为规范 412
9.2 预知多态演算 414
9.2.1 类型和项的语法 414
9.2.2 与其他多态形式比较 418
9.2.3 等式证明系统和归纳 421
9.2.4 预知多态的模型 422
9.2.5 ML风格的多态说明 425
9.3 不可预知多态 428
9.3.1 引言 428
9.3.2 理论的表达性和性质 429
9.3.3 归约的终止 441
9.3.4 语义模型总结 445
9.3.5 基于全总域的模型 447
9.3.6 部分等价关系模型 450
9.4 数据抽象与存在类型 456
9.5 通积、通和与程序模块 460
9.5.1 ML模块语言 460
9.5.2 带有积与和的预知演算 465
9.5.3 以积与和来表示模块 468
9.5.4 预知性和论域之间的关系 469
第10章 类型适应性和相关概念 472
10.1 引言 472
10.2 有类型适应性的简单类型化λ演算 474
10.3 记录 478
10.3.1 记录类型适应性的一般性质 478
10.3.2 带记录和类型适应性的类型化演算 479
10.4 类型适应性的语义模型 482
10.4.1 概述 482
10.4.2 类型适应性的转换解释 482
10.4.3 类型的子集解释 488
10.4.4 部分等价关系作为类型 493
10.5 递归类型和对象的一个记录模型 497
10.6 带衍类型约束的多态 504
第11章 类型推理 513
11.1 类型推理的介绍 513
11.2 带类型变量的λ→的类型推理 516
11.2.1 λ？语言 516
11.2.2 代入，实例和合一 517
11.2.3 主参数分离类型求取算法 521
11.2.4 隐式类型求取 524
11.2.5 类型求取和合一的等价性 526
11.3 带多态声明的类型推理 530
11.3.1 ML类型推理和多态变量 530
11.3.2 两个隐式类型求取规则集 531
11.3.3 类型推理算法 533
11.3.4 ML1和ML2的等价性 538
11.3.5 ML类型推理的复杂度 541
参考文献 548