《计算的数学理论》

第一章　可计算性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 有效的wff105

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