The theory of computer science: A programming approach

Contents......Page 6
Preface......Page 10
1.1 Introduction......Page 13
1.2.1 Defining 'computable'......Page 15
1.2.3 The limitations of our intuition......Page 18
1.3 Part 2: Towards a theory of computer science......Page 20
1.3.1 Problem solving......Page 21
1.3.2 Programming languages......Page 22
1.3.3 Data structures......Page 24
1.3.5 Program termination......Page 25
1.3.7 Computers......Page 26
2.2 Basic machines and finite state machines......Page 31
2.3 Sequences of inputs; states......Page 36
2.4 The limitations of finite state machines......Page 40
2.5 Turing machines......Page 42
2.6 A universal Turing machine......Page 51
2.7 Shannon's complexity measure for Turing machines......Page 53
2.8 More computer-like abstract machines......Page 58
2.8.1 B machines......Page 59
2.8.2 Program machines......Page 60
2.8.3 RASP's......Page 62
3.1 Introduction......Page 63
3.2 A non-computable function......Page 65
3.3 Enumerability and decidability......Page 68
3.3.1 Enumerability......Page 69
3.3.2 Decidability......Page 76
3.4.1 Recursive function theory......Page 81
3.4.2 Computability results in mathematics and logic......Page 83
3.4.3 Program schemas: the work of Luckham, Park, and Paterson......Page 87
3.4.4 Formal language theory: the syntax of programming languages......Page 95
4.1 Introduction......Page 104
4.2 The general recursive functions......Page 108
4.2.1 Generalized composition......Page 109
4.2.2 Primitive recursion......Page 112
4.2.3 The GRF......Page 116
4.3.1 Ackermann's function......Page 121
5.2 A GRF simulator for Turing machines......Page 129
5.2.1 Initialize......Page 130
5.2.2 Mainloop......Page 131
5.2.3 Extractresult......Page 134
5.2.4 Ackermann's function is a GRF......Page 135
5.3 A Turing machine compiler for the GRF......Page 137
5.4 Numbers as data structures......Page 141
6.1 Introduction......Page 149
6.2 McCarthy's formalism......Page 151
6.3 S-expressions......Page 159
6.4 Application of the formalism: equivalence of programs......Page 166
6.5 Application of the formalism: the meaning of programming languages......Page 180
7.1 Introduction......Page 187
7.2 Program testing......Page 191
7.3.1 Introduction: Floyd's work......Page 198
7.3.2 Hoare's logic of programs......Page 209
7.3.3 Towards automatic proofs of correctness......Page 218
7.4.1 Introduction......Page 220
7.4.2 The correctness of flow chart programs......Page 221
7.5 Reflections......Page 226
8.1 Introduction......Page 230
8.2 The lambda calculus......Page 236
8.3.1 Observing the basic correspondence......Page 243
8.3.2 Evaluating AEs......Page 246
8.3.3 Translating ALGOL 60 into (imperative) AEs......Page 250
8.3.4 Postscript on operational semantics: VDL......Page 252
8.4 Mathematical semantics: de-emphasizing the machine......Page 253
Appendix A Mathematical Prerequisites......Page 265
Appendix B Programming Prerequisites......Page 280
References......Page 284
Author Index......Page 293
Subject Index......Page 295