程序设计语言理论基础

第1章 引言 1.  
1.1 模型程序设计语言    
1.2 λ记法    
1.3 等式,4归约和语义 4  
1.3.1 公理语义    
1.3.2 操作语义    
1.3.3 指称语义 5  
1.4 类型和类型系统 6  
1.5 记法和数学约定    
1.6 集合论基础知识    
1.6.1 基础 9  
1.6.2 关系和函数 12  
1.7 语法和语义 14  
1.7.1 目标语言和元语言 14  
1.7.2 文法    
1.7.3 词法分析和语法分析    
1.7.4 数学解释示例 17  
1.8 归纳法 18  
1.8.1 自然数归纳法    
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编程样例,43表达能和限度 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 代数,58基调和项 99  
3.3.1 代数 99  
3.3.2 代数项语法 99  
3.3.3 代数和项的解释 101  
3.3.4 代入引理 104  
3.4 等式,63可靠性和完备性 105  
3.4.1 等式 105  
3.4.2 项代数和代入 106  
3.4.3 语义蕴涵和等式证明系统 107  
3.4.4 完备性的形式 115  
3.4.5 同余,68商和演绎完备性 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 局部汇聚,84终止和完备性 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模型,102可靠性和完备性 186  
4.5.1 通用模型和项的含义 186  
4.5.2 作用结构,104外延性和框架 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章 类型化λ演算模型 204  
5.1 引言 204  
5.2 域论模型和不动点 204  
5.2.1 递归定义和不动点算子 204  
5.2.2 完全偏序,116提升和笛卡儿积 206  
5.2.3 连续函数 209  
5.2.4 不动点和完全连续层次 212  
5.2.5 PCF的CPO模型 218  
5.3 不动点归纳 223  
5.4 计算适当性和完全抽象 227  
5.4.1 近似原理和计算适当性 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 提升,131部分函数和递归 249  
5.6.4 递归和固有序 251  
5.6.5 有效CPO的提升,133积和函数空间 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 关于while程序的前-后断言 277  
6.5.1 一阶和部分正确性断言 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 范畴,162函子和自然变换 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 外延性,171组合子和函子范畴 331  
7.3.5 环境和项的含义 333  
7.3.6 可靠性和完备性 335  
7.3.7 Kripkecλ模型作为笛卡儿闭范畴 336  
7.4 递归类型的域模型 338  
7.4.1 一个启示性的例子 338  
7.4.2 图,177锥和极限 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 部分满射和特殊模型 385  
8.4.1 部分满射和完整的古典层次 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章 多态与模块性 407  
9.1 引言 407  
9.1.1 概述 407  
9.1.2 类型作为函数实参 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 λt→语言 516  
11.2.2 代入,253实例和合一 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