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

程序设计语言理论基础PDF格式电子书版下载

注意：本站所有压缩包均有解压码： 点击下载压缩包解压工具

第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　积极PCF61

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模型作为CCC325

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