Mathematical Theory of Computation Book

	Preface	ix
Chapter 1	Computability	1
	Introduction	1
1-1	Finite Automata	2
1-1.1	Regular Expressions	3
1-1.2	Finite Automata	7
1-1.3	Transition Graphs	9
1-1.4	Kleene's Theorem	11
1-1.5	The Equivalence Theorem	17
1-2	Turing Machines	20
1-2.1	Turing Machines	21
1-2.2	Post Machines	24
1-2.3	Finite Machines with Pushdown Stores	29
1-2.4	Nondeterminism	35
1-3	Turing Machines as Acceptors	37
1-3.1	Recursively Enumerable Sets	38
1-3.2	Recursive Sets	39
1-3.3	Formal Languages	41
1-4	Turing Machines as Generators	43
1-4.1	Primitive Recursive Functions	45
1-4.2	Partial Recursive Functions	50
1-5	Turing Machines as Algorithms	53
1-5.1	Solvability of Classes of Yes/No Problems	54
1-5.2	The Halting Problem of Turing Machines	56
1-5.3	The Word Problem of Semi-Thue Systems	58
1-5.4	Post Correspondence Problem	60
1-5.5	Partial Solvability of Classes of Yes/No Problems	64
	Bibliographic Remarks	67
	References	68
	Problems	70
Chapter 2	Predicate Calculus	77
	Introduction	77
2-1	Basic Notions	81
2-1.1	Syntax	81
2-1.2	Semantics (Interpretations)	85
2-1.3	Valid Wffs	90
2-1.4	Equivalence of Wffs	95
2-1.5	Normal Forms of Wffs	101
2-1.6	The Validity Problem	105
2-2	Natural Deduction	108
2-2.1	Rules for the Connectives	110
2-2.2	Rules for the Quantifiers	115
2-2.3	Rules for the Operators	122
2-3	The Resolution Method	125
2-3.1	Clause Form	125
2-3.2	Herbrand's Procedures	130
2-3.3	The Unification Algorithm	136
2-3.4	The Resolution Rule	140
	Bibliographic Remarks	145
	References	146
	Problems	147
Chapter 3	Verification of Programs	161
	Introduction	161
3-1	Flowchart Programs	161
3-1.1	Partial Correctness	170
3-1.2	Termination	182
3-2	Flowchart Programs with Arrays	189
3-2.1	Partial Correctness	189
3-2.2	Termination	195
3-3	Algol-Like Programs	202
3-3.1	While Programs	203
3-3.2	Partial Correctness	205
3-3.3	Total Correctness	211
	Bibliographic Remarks	218
	References	220
	Problems	223
Chapter 4	Flowchart Schemas	241
	Introduction	241
4-1	Basic Notions	242
4-1.1	Syntax	242
4-1.2	Semantics (Interpretations)	244
4-1.3	Basic Properties	248
4-1.4	Herbrand Interpretations	260
4-2	Decision Problems	262
4-2.1	Unsolvability of the Basic Properties	264
4-2.2	Free Schemas	268
4-2.3	Tree Schemas	274
4-2.4	Ianov Schemas	284
4-3	Formalization in Predicate Calculus	294
4-3.1	The Algorithm	295
4-3.2	Formalization of Properties of Flowchart Programs	307
4-3.3	Formalization of Properties of Flowchart Schemas	311
4-4	Translation Problems	317
4-4.1	Recursive Schemas	319
4-4.2	Flowchart Schemas versus Recursive Schemas	322
	Bibliographic Remarks	334
	References	335
	Problems	337
Chapter 5	The Fixpoint Theory of Programs	356
	Introduction	356
5-1	Functions and Functionals	357
5-1.1	Monotonic Functions	359
5-1.2	Continuous Functionals	366
5-1.3	Fixpoints of Functionals	369
5-2	Recursive Programs	374
5-2.1	Computation Rules	375
5-2.2	Fixpoint Computation Rules	384
5-2.3	Systems of Recursive Defintions	389
5-3	Verification Methods	392
5-3.1	Stepwise Computational Induction	393
5-3.2	Complete Computational Induction	400
5-3.3	Fixpoint Induction	403
5-3.4	Structural Induction	408
	Bibliographic Remarks	415
	References	416
	Problems	418
	Indexes	431
	Name Index
	Subject Index