程序设计语言理论PDF电子书下载

目录 1

第1章　引言 1

1.1　基本概念 1

1.1.1　模型语言 1

1.1.2　λ表示法 2

1.1.3　记号和约定 3

1.2　等式、归约和语义 4

1.2.1　公理语义 5

1.2.2　操作语义 5

1.3　类型和类型系统 6

1.2.3　指称语义 6

1.3.1　类型和类型系统 7

1.3.2　类型语言的优点 8

1.4　归纳法 9

1.4.1　表达式上的归纳 9

1.4.2　证明上的归纳 11

1.4.3 良基归纳 13

习题 15

第2章　可计算函数程序设计语言 16

2.1　引言 16

2.2　语法 17

2.2.1 概述 17

2.2.2　布尔值和自然数 18

2.2.3　二元组和函数 19

2.2.4　声明和语法美化 22

2.2.5　递归函数和不动点算子 24

2.2.6　语法总结和例子 26

2.3　程序和语义 28

2.3.1　程序和结果 28

2.3.2　公理语义 29

2.3.3　指称语义 30

2.3.4　操作语义 32

2.3.5 由各种形式的语义定义的等价关系 33

2.4　归约和符号解释器 34

2.4.1　归约的合流性 35

2.4.2　归约策略 37

2.4.3　最左归约和惰性归约 38

2.4.4　并行归约 42

2.4.5　急切归约 43

2.5　程序设计实例、表达能力和局限 46

2.5.1　记录和n元组 46

2.5.2　查找自然数 47

2.5.3 迭代和尾递归 49

2.5.4　完全递归函数 51

2.5.5　部分递归函数 53

2.5.6　并行运算的不可定义性 55

2.6.1　单元类型与和类型 56

2.6　衍生和扩充 56

2.6.2　递归类型 58

习题 60

第3章　泛代数和代数数据类型 68

3.1　引言 68

3.2　代数、基调和项 69

3.2.1　代数 69

3.2.2　代数项的语法 70

3.2.3　代数以及项在代数中的解释 72

3.3　等式、可靠性和完备性 75

3.3.1 等式 75

3.2.4　代换引理 75

3.3.2　项代数 77

3.3.3　语义蕴涵和一个等式证明系统 78

3.3.4　完备性的形式 83

3.3.5　同余、商和演绎完备性 84

3.3.6　非空类别和最小模型性质 86

3.4　同态和初始性 87

3.4.1　同态和同构 87

3.4.2　初始代数 88

3.5　代数数据类型 92

3.5.1　代数数据类型 92

3.5.2　初始代数语义和数据类型归纳 94

3.5.3　解释没有意义的项 96

3.5.4　错误值的其他解决方法 101

3.6　重写系统 101

3.6.1　基本定义 101

3.6.2　合流性和可证明的相等性 103

3.6.3　终止性 104

3.6.4　临界对 108

3.6.5　左线性无重叠重写系统 112

3.6.6　局部合流、终止和合流之间的联系 114

3.6.7　代数数据类型的应用 116

习题 119

4.1　引言 125

第4章　简单类型化λ演算 125

4.2　类型 126

4.2.1　类型的语法 126

4.2.2　类型的解释 127

4.3　项 128

4.3.1 上下文有关语法 128

4.3.2　λ→项的语法 129

4.3.3　有积、和及相关类型的项 133

4.3.4　定型算法 135

4.4　证明系统 137

4.4.1　等式和理论 137

4.4.2　归约规则 141

4.4.3　有其他规则的归约 143

4.5.1　一般模型和项的含义 145

4.5　Henkin模型、可靠性和完备性 145

4.5.2　应用结构、外延性和框架 146

4.5.3　环境条件 147

4.5.4　类型可靠性和等式可靠性 150

4.5.5　没有空类型的Henkin模型的完备性 152

4.5.6　有空类型的完备性 154

4.5.7　其他类型的Henkin模型 155

习题 157

5.2　论域理论模型和不动点 160

5.2.1　递归定义和不动点算子 160

5.1　引言 160

第5章　类型化λ演算的模型 160

5.2.2　完全偏序集合、提升和笛卡儿积 163

5.2.3　连续函数 165

5.2.4　不动点和完全连续体系 168

5.2.5　PCF的CPO模型 173

5.3　不动点归纳 176

5.4　计算适当性和完全抽象 179

5.4.1　近似定理和计算的适当性 179

5.4.2　带并行运算的PCF的完全抽象 183

习题 184

第6章　命令式程序 191

6.1　引言 191

6.2.2　Kernel语言的语法 193

6.2　Kernel语言 193

6.2.1　左值和右值 193

6.3　操作语义 194

6.3.1　表达式中的基本符号的解释 194

6.3.2　存储单元和状态 194

6.3.3　表达式的计算 195

6.3.4　命令的执行 196

6.4　指称语义 199

6.4.1　带状态的类型化λ演算 199

6.4.2　语义函数 202

6.4.3　操作语义和指称语义的等价 204

6.5.1 一阶逻辑和部分正确性证明 206

6.5　Kernel程序的前后断言 206

6.5.2 明规则 208

6.5.3 可靠性 211

6.5.4　相对完备性 212

6.6　其他语言构造的语义 215

6.6.1　概述 215

6.6.2　有局部变量的程序块 215

6.6.3　过程 221

6.6.4　程序块和过程声明的组合 222

习题 223

7.1　引言 230

7.1.1　概述 230

第7章　多态性 230

7.1.2　类型作为函数变元 231

7.1.3　一般积与一般和 235

7.2　谓词式多态演算 235

7.2.1　类型和项的语法 235

7.2.2　和其他形式多态性的比较 240

7.2.3　等式证明系统和归约 243

7.2.4　ML风格的多态声明 244

7.3　非谓词式多态λ演算 247

7.3.1 引言 247

7.3.2　非谓词式多态λ演算的表达能力 248

7.3.3　归约的终止性 250

7.4　数据抽象和存在类型 252

7.5　一般积、一般和及程序模块 255

7.5.1　ML模块语言 255

7.5.2　带积与和的谓词式演算 261

7.5.3　带积与和的表示模块 265

7.5.4　谓词性和两个全域之间的联系 266

7.6　类型作为规范 268

7.6.1　公式作为类型的对应 268

7.6.2　类型作为规范 271

习题 273

第8章　子定型及有关概念 277

8.1　引言 277

8.2　有子定型的简单类型化λ演算 279

8.3　记录 284

8.3.1　记录子定型的一般性质 284

8.3.2　带记录和子定型的类型化演算 285

8.4　子定型的语义模型 287

8.4.1　概述 287

8.4.2　子定型的转换解释 287

8.4.3　类型的子集解释 294

8.5　递归类型和对象的记录模型 295

8.6　带子类型限制的多态性 302

习题 311

9.1　引言 315

第9章　类型推断 315

9.2　带类型变量的λ→类型推断 318

9.2.1　语言λ？ 318

9.2.2　代换、实例与合一 319

9.2.3　主定型算法 322

9.2.4　隐式定型 326

9.2.5　定型和合一的等价 327

9.3　带多态声明的类型推断 329

9.3.1 ML类型推断和多态变量 329

9.3.2　两组隐式定型规则 330

9.3.3　类型推断算法 333

习题 338

参考文献 340