Table of Contents
Preface xi
1 Mathematical Preliminaries 1
1.1 Sets and Sequences 1
1.2 Relations and Functions 3
1.3 Operators and their Algebraic Properties 5
1.4 Set Operators 7
1.5 Strings and String Operators 8
1.6 Expressions 10
1.7 Growth Rates of Functions 13
1.8 Graphs and Trees 14
I Logic for Computer Science 17
2 Propositional Logic 21
2.1 Propositions 21
2.2 States, Operators and Semantics 25
2.3 Propositions as Functions 27
2.4 Laws of Propositional Logic 32
2.5 Two Important Operators 35
2.6 Normal Forms 38
2.7 Logic Circuits 40
3 Proofs by Deduction 49
3.1 Reasons for Wanting to Prove Things 49
3.2 Natural Deduction Proofs 50
3.3 Rules of Inference 53
3.4 Proof by Rules 57
3.5 Assumptions 59
3.6 Further Examples 64
3.7 Types of Theorems and Proof Strategies 67
3.8 Soundness and Completeness 70
4 Predicate Logic 75
4.1 Predicates and Functions 75
4.2 Predicates, English, and Sets 78
4.3 Quantifiers 80
4.4 Multiple Quantifiers 85
4.5 Logic for Data Structures 90
5 Proving with Predicates 99
5.1 Inference Rules with Predicates 99
5.2 Proof Strategies with Predicates 102
5.3 Applying Logic to Mathematics 103
5.4 Mathematical Induction 107
5.5 Examples of mathematical induction 114
5.6 Limits of Logic 116
6 Program Verification 123
6.1 The Idea of Verification 123
6.2 Definitions 124
6.3 Inference Rules 126
6.4 Loop Invariants 131
6.5 Proofs with Procedures 137
6.6 Loop Invariants and Tail Recursion 138
6.7 The Debate About Formal Verification 140
II Language Models for Computer Science 145
7 Language and Models 149
7.1 Programming Languages and Computer Science 149
7.2 Formal Languages 150
7.3 Language Operators 154
7.4 Two Views of Alphabets and Language 156
7.5 The Questions of Formal Language Theory 157
8 Generative Models of Regular Languages 165
8.1 Generative Models 165
8.2 Nondeterminism: The General Idea 168
8.3 Regular Languages 172
8.4 Regular Expressions 173
8.5 Regular Expressions and Nondeterminism 180
8.6 Grammars: The General Idea 181
8.7 Regular Grammars 184
8.8 Unifying the Approaches 190
8.9 Deterministic Regular Grammars 193
8.10 Summary 196
9 Finite Automata and Regular Languages 201
9.1 Finite Automata: The General Idea 202
9.2 Diagrams and Recognition 203
9.3 Formal Notation for Finite Automata 210
9.4 Relationship to Regular Languages 215
9.5 Nondeterministic Finite Automata 217
9.6 Properties of Regular Languages 224
9.7 Limitations of Regular Languages 226
9.8 Pattern Matching 230
9.9 Designing Finite Automata 233
10 Context-Free Grammars 241
10.1 Introduction to Context-Free Grammars 242
10.2 An Example 246
10.3 Structure, Meaning and Ambiguity 248
10.4 Chomsky Normal Form 256
10.5 Greibach Normal Form 261
10.6 Beyond Context-Free Languages 265
11 Pushdown Automata and Parsing 271
11.1 Motivating PDAs 272
11.2 Standard Notation for PDAs 276
11.3 Prom CFG to NPDA 282
11.4 Prom NPDA to CFG 283
11.5 Parsing 285
11.6 Deterministic Pushdown Automata and Parsing 287
11.7 A Variation of the Pushdown Automata Model 291
11.8 Limitations on Deterministic Pushdown Automata 292
11.9 More on Parsing 295
11.10 Notes on Memory 297
12 Turing Machines 301
12.1 Unrestricted Grammars 302
12.2 The Turing Machine Model 305
12.3 Infinite Sets 310
12.4 Universal Turing Machines 313
12.5 Limits on Turing Machines 316
12.6 Undecidability 319
12.7 Church-Turing Thesis 321
12.8 Computational Complexity 322
A Logic Programming 333
A.1 The Essence of Prolog and its Relation to Logic 333
A.2 Getting Started Using Prolog 336
A.3 An Example Related to Databases 341
A.4 The General Form and a Limitation of Prolog 346
A.5 How Prolog Works 349
A.6 Structures 355
A.7 Lists and Recursion 356
A.8 Built-in Predicates and Operators 362
A.9 Finite Automata in Prolog 368
A.10 Pushdown Automata in Prolog 372
B The AWK Language 381
B.1 Overview of AWK 381
B.2 Writing expressions 383
B.3 Writing regular expressions 384
B.4 Writing patterns 384
B.5 Writing actions 386
B.6 Using arrays 387
B.7 Sample programs 388
B.8 Using AWK in Unix 389
B.9 An example 390
C Answers to Selected Problems 393
Index 445
