计算的数学理论PDF电子书下载

第一章　可计算性 1

引言 1

1-1　有限自动机 2

1-1.1　正则表达式 4

1-1.2　有限自动机 8

1-1.3　转换图 10

1-1.4 克林定理 12

1-1.5　等价定理 18

1-2　图林机 22

1-2.1　图林机 23

1-2.2　波斯特机 26

1-2.3　带有下推存贮器的有限机 32

1-2.4　不确定性 38

1-3　图林机作为接受器 41

1-3.1　递归可枚举集 42

1-3.2　递归集 43

1-3.3　形式语言 45

1-4　图林机作为生成器 49

1-4.1　原始递归函数 50

1-4.2　部分递归函数 57

1-5　图林机作为算法 60

1-5.1　是／否问题类的可解性 62

1-5.2　图林机的停机问题 63

1-5.3　半图厄系统的字问题 66

1-5.4　波斯特对应问题 69

1-5.5　是／否问题类的部分可解性 74

文献述评 77

参考文献 78

习题 80

第二章　谓词演算 89

引言 89

2-1 基本概念 93

2-1.1　语法 93

2-1.2　语义（解释） 99

2-1.3 有效的wff 105

2-1.4　wff的等价 112

2-1.5 wff的范式 120

2-1.6 有效性问题 124

2-2 自然演绎法 128

2-2.1 联结词规则 130

2-2.2 量词规则 137

2-2.3 运算符规则 146

2-3 分解法 150

2-3.1 子句形式 151

2-3.2 赫尔布兰德过程 156

2-3.3 一致算法 164

2-3.4 分解规则 169

文献述评 174

参考文献 175

习题 177

第三章　程序的验证 196

引言 196

3-1　框图程序 196

3-1.1　部分正确性 206

3-1.2　终止 219

3-2　带数组的框图程序 227

3-2.1　部分正确性 227

3-2.2　终止 234

3-3 类ALGOL程序 243

3-3.1　当型程序 243

3-3.2　部分正确性 246

3-3.3　全正确性 253

文献述评 261

参考文献 262

习题 265

引言 284

第四章　框图模式 284

4-1　基本概念 285

4-1.1 语法 285

4-1.2　语义（解释） 287

4-1.3　基本性质 292

4-1.4　赫尔布兰德解释 303

4-2　判定问题 306

4-2.1　基本性质的不可解性 308

4-2.2　自由模式 313

4-2.3　树模式 319

4-2.4　亚诺夫（Ianov）模式 328

4-3　用谓词演算作形式化 338

4-3.1 算法 338

4-3.2　框图程序性质的形式化 350

4-3.3　框图模式性质的形式化 355

4-4　转换问题 362

4-4.1　递归模式 364

4-4.2　框图模式与递归模式 368

文献述评 379

参考文献 380

习题 382

第五章　程序的不动点理论 401

引言 401

5-1　函数和泛函 402

5-1.1　单调函数 404

5-1.2　连续泛函 412

5-1.3　泛函的不动点 416

5-2　递归程序 421

5-2.1　计算规则 422

5-2.2　不动点计算规则 431

5-2.3　递归定义组 438

5-3　验证方法 441

5-3.1　逐步计算归纳法 441

5-3.2　完全计算归纳法 449

5-3.3　不动点归纳法 453

5-3.4　结构归纳法 459

文献述评 468

参考文献 469

习题 471

附第一篇论文：程序的逻辑分析 484

附第二篇论文：计算机程序设计的逻辑方法 534

参考文献 615