第1章 引言 1
1.1 基本概念 1
1.1.1 程序设计语言的建模 1
1.1.2 λ表示法 2
1.1.3 符号和约定 4
1.2 等式、归约和语义 4
1.2.1 公理语义 5
1.2.2 操作语义 5
1.2.3 指称语义 6
1.3 类型和类型系统 7
1.3.1 类型和类型系统 7
1.3.2 类型化语言的优点 8
1.4 归纳法 10
1.4.1 表达式上的归纳 10
1.4.2 证明上的归纳 11
1.4.3 良基归纳 14
习题 16
第2章 泛代数和代数数据类型 17
2.1 引言 17
2.2 代数、基调和项 18
2.2.1 代数 18
2.2.2 代数项的语法 19
2.2.3 代数以及项在代数中的解释 21
2.2.4 代换引理 24
2.3 等式、可靠性和完备性 25
2.3.1 等式 25
2.3.2 项代数 26
2.3.3 语义蕴涵和等式证明系统 27
2.3.4 完备性的形式 33
2.3.5 同余、商和演绎完备性 33
2.3.6 非空类别和最小模型完备性 36
2.4 同态和初始性 37
2.4.1 同态和同构 37
2.4.2 初始代数 38
2.5 代数数据类型 43
2.5.1 代数数据类型 43
2.5.2 初始代数语义和数据类型归纳 44
2.5.3 解释没有意义的项 47
2.5.4 错误值的其他解决方法 51
2.6 重写系统 51
2.6.1 基本定义 51
2.6.2 合流性和可证的相等性 54
2.6.3 终止性 54
2.6.4 临界对 59
2.6.5 左线性无重叠重写系统 63
2.6.6 局部合流、终止和合流之间的联系 65
2.6.7 代数数据类型的应用 67
习题 70
第3章 简单类型化λ演算 76
3.1 引言 76
3.2 类型和项 77
3.2.1 类型的语法 77
3.2.2 上下文有关语法 78
3.2.3 λ→项的语法 79
3.2.4 带积、和及其他类型的项 84
3.2.5 定型算法 89
3.3 证明系统 90
3.3.1 等式和理论 90
3.3.2 归约规则 95
3.3.3 有其他规则的归约 97
3.4 通用模型、可靠性和完备性 98
3.4.1 通用模型和项的含义 98
3.4.2 应用结构、外延性和框架 99
3.4.3 环境条件 100
3.4.4 类型可靠性和等式可靠性 103
3.4.5 没有空类型的完备性 106
3.4.6 有空类型的完备性 107
3.4.7 其他类型的通用模型 108
3.5 可计算函数编程语言 110
3.5.1 概述 110
3.5.2 PCF的语法 111
3.5.3 声明和语法美化 113
3.5.4 程序和结果 115
3.5.5 公理语义 115
3.5.6 操作语义 117
3.5.7 由各种形式的语义定义的等价关系 118
3.5.8 记录和n元组 120
3.6 各种归约策略 121
3.6.1 归约策略 121
3.6.2 最左归约和惰性归约 123
3.6.3 并行归约 126
3.6.4 急切归约 127
习题 128
第4章 类型化λ演算的模型 135
4.1 引言 135
4.2 递归函数和不动点算子 135
4.2.1 递归函数和不动点算子 135
4.2.2 有不动点算子的急切归约 138
4.2.3 PCF语言的编程实例 140
4.3 论域理论模型和不动点 144
4.3.1 递归定义和不动点算子 144
4.3.2 完全偏序集合、提升和笛卡儿积 145
4.3.3 连续函数 148
4.3.4 不动点和完备连续层级 151
4.3.5 PCF的CPO模型 156
4.4 不动点归纳 159
习题 162
第5章 命令式程序的语义 173
5.1 引言 173
5.2 Kernel语言 175
5.2.1 存储单元 175
5.2.2 表达式的解释 176
5.2.3 程序状态 177
5.3 操作语义 178
5.3.1 表达式的求值 178
5.3.2 命令的执行 180
5.4 指称语义 182
5.4.1 带状态的类型化λ演算 182
5.4.2 语义函数 184
5.4.3 操作语义和指称语义的等价 187
5.5 Kernel语言的Hoare逻辑 189
5.5.1 一阶断言 189
5.5.2 证明规则 191
5.5.3 可靠性 194
5.5.4 小结 195
习题 196
第6章 递归类型 201
6.1 引言 201
6.2 归纳和余归纳 202
6.2.1 余归纳现象 202
6.2.2 归纳和余归纳指南 205
6.2.3 代数和余代数 207
6.3 递归类型 210
6.3.1 递归类型总览 210
6.3.2 递归的数据结构 212
6.4 归纳类型和余归纳类型 214
6.4.1 归纳类型和余归纳类型总览 214
6.4.2 帮助理解的实例 217
习题 219
第7章 多态性 222
7.1 引言 222
7.1.1 概述 222
7.1.2 类型作为函数变元 222
7.2 直谓式多态演算 227
7.2.1 类型和项的语法 227
7.2.2 和其他形式多态性的比较 232
7.2.3 等式证明和归约 236
7.2.4 ML风格的多态声明 237
7.3 非直谓式多态演算 238
7.3.1 引言 238
7.3.2 非直谓式多态λ演算的表达力 239
7.3.3 归约的终止性 241
7.4 数据抽象和存在类型 242
7.5 类型表达式的分类 247
7.5.1 类型表达式的种类 247
7.5.2 类型表达式的定类与相等 248
7.5.3 项的定型 249
习题 250
第8章 依赖类型 254
8.1 引言 254
8.2 带依赖类型的演算 255
8.2.1 依赖积类型 255
8.2.2 依赖和类型 259
8.3 带依赖类型的程序设计 260
8.3.1 简化DML的实例 260
8.3.2 简化DML的定义 263
8.4 广义积与广义和 266
8.4.1 广义积与广义和概念 266
8.4.2 带广义积与广义和的直谓式演算 266
8.4.3 ML模块语言 270
8.4.4 用积与和来表示模块 276
8.4.5 直谓性以及两个全域之间的联系 277
习题 279
第9章 命题和类型 281
9.1 引言 281
9.2 构造逻辑 282
9.2.1 构造语义 282
9.2.2 构造逻辑 283
9.2.3 命题当作类型 286
9.3 经典逻辑 288
9.3.1 经典逻辑和构造逻辑的区别与联系 288
9.3.2 经典逻辑的规则 289
9.3.3 推导消去形式 293
9.3.4 证明的动态性 294
习题 295
第10章 子定型 296
10.1 引言 296
10.2 有子定型的简单类型化λ演算 298
10.3 记录 303
10.3.1 记录子定型的一般性质 303
10.3.2 带记录和子定型的类型化演算 304
10.4 子定型的语义模型 307
10.4.1 概述 307
10.4.2 子定型的转换解释 307
10.4.3 类型的子集解释 314
10.5 对象的递归记录模型 315
10.5.1 递归记录类型 315
10.5.2 递归类型的子定型 319
习题 322
第11章 类型推断 325
11.1 引言 325
11.2 带类型变量的λ→类型推断 328
11.2.1 语言λ→ 328
11.2.2 代换、实例与合一 329
11.2.3 主定型算法 332
11.2.4 隐式定型 336
11.2.5 定型和合一的等价 338
11.3 带多态声明的类型推断 339
11.3.1 ML类型推断和多态变量 339
11.3.2 两组隐式定型规则 341
11.3.3 类型推断算法 344
习题 349
参考文献 351