程序设计语言理论PDF|Epub|txt|kindle电子书版本网盘下载

程序设计语言理论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