Programming-Based Formal Languages and Automata Theory: Design, Implement, Validate, and Prove (Texts in Computer Science)

✍ Scribed by Marco T. Morazán

• Publisher: Springer
• Year: 2024
• Tongue: English
• Leaves: 530
• Edition: 1
• Category: Library

✦ Synopsis

This textbook introduces formal languages and automata theory for upper-level undergraduate or beginning graduate students. While it contains the traditional mathematical development usually employed in computational theory courses, it is also quite different from many of them. Machines, grammars, and algorithms developed as part of a constructive proof are intended to be rendered as programs.

The book is divided into four parts that build on each other. Part I reviews fundamental concepts. It introduces programming in FSM and reviews program design. In addition, it reviews essential mathematical background on sets, relations, and reasoning about infinite sets. Part II starts the study of formal languages and automata theory in earnest with regular languages. It first introduces regular expressions and shows how they are used to write programs that generate words in a regular language. Given that regular expressions generate words, it is only natural to ask how a machine can recognize words in a regular language. This leads to the study of deterministic and nondeterministic finite-state machines. Part III starts the exploration of languages that are not regular with context-free languages. It begins with context-free grammars and pushdown automata to generate and recognize context-free languages, and it ends with a discussion of deterministic pushdown automata and illustrates why these automatons are fundamentally different from nondeterministic pushdown automata. Part IV eventually explores languages that are not context-free, known as context-sensitive languages. It starts by discussing the most powerful automaton known to mankind: the Turing machine. It then moves to grammars for context-sensitive languages, and their equivalence with Turing machines is explored. The book ends with a brief chapter introducing complexity theory and explores the question of determining if a solution to a problem is practical.

✦ Table of Contents

Preface
1 To Students
2 To Instructors
3 FSM
3.1 Installing
3.1.1 DrRacket
3.1.2 FSM
3.2 Writing FSM Programs
3.3 Bug Reporting
4 The Parts of the Book
5 Acknowledgments
Contents
Part I Fundamental Concepts
1 Introduction to FSM
6 FSM Syntax
6.1 Boilerplate Code
6.2 Value Expressions
6.3 Primitive Functions and Application Expressions
6.4 Lists
6.5 List Abbreviations
6.6 Conditional Expressions
6.7 Defining Local Variables
6.8 Functions as Values
6.8.1 Lambda Expressions
6.8.2 Higher-Order Functions
6.9 For Loops
6.10 Writing Unit Tests
6.11 Definitions
7 Designing Functions
7.1 The Design Recipe
7.2 Scaling a Binary Tree
7.2.1 Representation
7.2.2 Design Idea
7.2.3 Signature, Purpose, and Function Header
7.2.4 Tests
7.2.5 Function Body
7.2.6 Running the Tests
8 FSM Basics
8.1 FSM Constants
8.2 FSM Data Definitions
2 Essential Background
9 Some Fundamental Questions
10 Automata Theory
11 Essential Mathematical Background
11.1 Sets
11.1.1 Set Notation
11.2 Set Operations
11.2.1 Set Laws
11.3 Relations and Functions
11.4 Countable and Uncountable
3 Types of Proofs
12 Formal Logic Proofs
13 Mathematical Induction Proofs
13.1 Computing n2
13.2 Computing n!
14 Pigeonhole Principle Proofs
15 Proofs by Contradiction
16 Diagonalization Proofs
Part II Regular Languages
4 Regular Expressions
17 Defining Languages Using Union and Concatenation
17.1 Constructors
17.2 Error Messages
17.3 Regular Expression Selectors and Predicates
17.4 Observers
18 Programming with Regular Expressions
18.1 All Words Ending with an a
18.2 Binary Numbers
18.2.1 Implementing a Regular Expression
18.2.2 Generating BIN-NUMS Words
19 Generating Words in the Language Defined by a Regular Expression
19.1 Design Idea
19.2 Signature, Purpose, and Function Header
19.3 Tests
19.4 Function Body
19.5 Running the Tests
20 Regular Expression Applications
20.1 Data Definitions
20.2 Design Idea
20.3 Function Definition
20.4 Tests
20.5 Auxiliary Functions
20.6 Running the Tests
5 Deterministic Finite-State Machines
21 Deterministic Finite-State Machine Definition
21.1 The dfa Constructor
21.2 FSM Machine Observers
21.3 FSM Machine Testers
21.4 FSM Machine Visualization
22 A First Example
22.1 Designing the Machine
22.2 Writing dfa State Invariant Predicates
22.3 Proving L(NO-ABAA) = L
22.3.1 Proving Invariants Hold for NO-ABAA
22.3.2 Proving L(NO-ABAA) = L
23 A Design Recipe for State Machines
24 The State Machine Design Recipe in Action
24.1 Name and Alphabet
24.2 Unit Tests
24.3 States
24.4 The Transition Function
24.5 Implementation and Testing
24.6 State Invariant Predicates
24.7 Correctness Proof
24.7.1 Proof That Invariants Hold
24.7.2 Proof the L = L(EVEN-A-ODD-B)
25 Applications
25.1 Finding a Pattern
25.2 Generalizing Pattern Detection
25.2.1 Design Idea
25.2.2 The contains-pattern? Predicate
25.2.3 The build-pattern-dfa Constructor
25.2.4 The gen-state-trans Function
6 Nondeterministic Finite-State Machines
26 Nondeterministic Finite-State Machines
27 Designing an ndfa
27.1 Name, Alphabet, and Tests
27.2 Design Idea and Conditions
27.3 Transition Relation
27.4 Implementation and Testing
27.5 State Invariant Predicates
27.6 Correctness
27.6.1 Proving State Invariants Hold
27.6.2 L = L(AT-LEAST-ONE-MISSING)
28 Equivalence of dfa and ndfa
28.1 Building a dfa from an ndfa
28.2 Implementation
28.2.1 Main Function: ndfa2dfa
28.2.2 The convert Function
28.2.3 Computing the Empties Table
28.2.4 Computing the Super State Transition Function
28.2.5 Computing the Super State Name Table
28.3 Correctness Proof
28.3.1 Proof That D Simulates All ND Computations and Vice Versa
28.3.2 L(ND) = L(D) Proof
29 Concluding Remarks
7 Finite-State Automatons and Regular Expressions
30 Closure Properties
30.1 Union
30.1.1 Construction Algorithm
30.1.2 Algorithm Correctness Proof
30.2 Concatenation
30.2.1 Implementation
30.2.2 Algorithm Correctness Proof
30.3 Kleene Star
30.3.1 Implementation
30.3.2 Algorithm Correctness Proof
30.4 Complement
30.4.1 Implementation
30.4.2 Algorithm Correctness Proof
30.5 Intersection
30.5.1 Implementation
30.5.2 Algorithm Correctness Proof
31 Equivalence of Finite-State Machinesand Regular Expressions
31.1 Creating an ndfa from a Regular Expression
31.1.1 Construction Algorithm
31.1.2 Implementation
31.1.3 Correctness Proof
31.2 Creating a Regular Expression from an ndfa
31.2.1 Implementation
31.2.2 Correctness Proof
8 Regular Grammars
32 Regular Grammars
33 The Design Recipe for Grammars
34 The Design Recipe in Action
34.1 Grammar Name and Alphabet
34.2 Syntactic Categories
34.3 The Production Rules
34.4 Unit Tests
34.5 Grammar Implementation
34.6 Run the Tests
35 Regular Grammars and Regular Languages
35.1 Constructing a Regular Grammar from a dfa
35.1.1 Implementation
35.1.2 Correctness Proof
35.2 Constructing an ndfa from a Regular Grammar
35.2.1 Implementation
35.2.2 Correctness Proof
9 Languages That Are Not Regular
36 The Pumping Theorem for Regular Languages
37 Proving a Language Is Not Regular
37.1 Using the Pumping Theoremfor Regular Languages
37.1.1 L = {anbn | n≥0} Is Not Regular
37.1.2 Revisiting L = {anbn | n≥0}
37.1.3 Sometimes It Is Useful to Pump Down
37.2 Using Closure Properties
Part III Context-Free Languages
10 Context-Free Grammars
38 Context-Free Grammar Definition
39 L = {anbn | n≥0} Is a Context-Free Language
39.1 Steps 1 and 2: Name, Alphabet, and Syntactic Categories
39.2 Step 3: The Production Rules
39.3 Step 4: Tests
39.4 Steps 5 and 6: Implementation and Testing
40 Practice Designing a cfg
40.1 Steps 1 and 2: Name, Alphabet, and Syntactic Categories
40.2 Step 3: The Production Rules
40.3 Step 4: Tests
40.4 Steps 5 and 6: Implementation and Testing
41 All Regular Languages Are Context-Free
42 Parse Trees
42.1 Similar Derivations
42.2 Ambiguity
11 Pushdown Automata
43 Pushdown Automata Definition
44 A pda for L = anbn
44.1 Name and Alphabets
44.2 Unit Tests
44.3 Conditions and States
44.4 The Transition Relation
44.5 Machine Implementation and Testing
44.6 State Invariant Predicates
44.7 Correctness
44.7.1 Proving State Invariants Hold
44.7.2 Proving L = L(P)
45 A pda for L = {wcwR | w(a b)}
45.1 Name and Alphabets
45.2 Unit Tests
45.3 Conditions and States
45.4 The Transition Relation
45.5 Machine Implementation and Testing
45.6 State Invariant Predicates
45.7 Correctness
45.7.1 Proving State Invariants Hold
45.7.2 Proving L = L(M)
46 ndfas and pdas
46.1 Design Idea
46.2 Implementation
12 Equivalence of pdas and cfgs
47 Building a pda from a cfg
47.1 Design Idea
47.2 Implementation
47.3 Proof
48 Building a cfg from a pda
48.1 Simple pda
48.1.1 Eliminating |β|≥2 Rules
48.1.2 Eliminating |β|= 0 Rules
48.1.3 Eliminating |θ|>2 Rules
48.1.4 Auxiliary Functions
48.2 Building a cfg from a Simple pda
48.2.1 Design Idea and Data Representation
48.2.2 Implementation
13 Properties of Context-Free Languages
49 Union
49.1 Design Idea
49.2 Implementation
49.3 Proof
50 Concatenation
50.1 Design Idea
50.2 Implementation
50.3 Proof
51 Kleene Star
51.1 Design Idea
51.2 Implementation
51.3 Proof
52 The Pumping Theorem for Context-Free Languages
52.1 Yield Length
52.2 The Pumping Theorem
52.3 Applying the Pumping Theorem for Context-Free Languages
53 Context-Free Languages Are Not Closed Under Intersection nor Complement
54 Intersection of a Context-Free Language and a Regular Language
54.1 Design Idea
54.2 Implementation
54.3 Proof
14 Deterministic PDAs
55 A Deterministic pda for wcwR
55.1 Design Idea
55.2 Name, Alphabets, and Unit Tests
55.3 Condition, States, Transition Function, and Implementation
55.4 State Invariant Predicates
55.5 Correctness
55.5.1 Proving State Invariants Hold
55.5.2 Proving L = L(M)
56 A Deterministic pda for L = {ambncp | m≠n m,n,p>0}
56.1 Design Idea
56.2 Name, Alphabets, and Unit Tests
56.3 Conditions, States, Transition Function, and Implementation
56.4 State Invariant Predicates
56.5 Correctness
56.5.1 Proving State Invariants Hold
56.5.2 Proving L = L(P)
57 Are All Context-Free Languages Deterministic?
58 Closure Properties of DeterministicContext-Free Languages
58.1 Union
58.2 Intersection
Part IV Context-Sensitive Languages
15 Turing Machines
59 Turing Machine Definition
60 A Turing Machine for L = a
60.1 Name, Alphabet, and Tests
60.2 Conditions and States
60.3 Transition Function, Implementation, and Testing
60.4 Invariant Predicates
60.5 Correctness
61 Nondeterministic Turing Machines
61.1 Name, Alphabet, and Tests
61.2 Conditions and States
61.3 Transition Function, Implementation, and Testing
61.4 Invariant Predicates
61.5 Correctness
62 Turing Machines Decide Regular Languages
62.1 Design Idea
62.2 Implementation
62.3 Correctness
63 A Turing Machine for anbncn
63.1 Design Idea
63.2 Name, Alphabet, and Tests
63.3 Conditions and States
63.4 Transition Function, Implementation, and Testing
63.5 State Invariant Predicates
63.6 Correctness
63.6.1 Proving State Invariants Hold
63.6.2 Proving L = L(M)
64 The Turing Tar-Pit
16 Turing Machine Composition
65 Simple Common Operations
65.1 Move Right Machine
65.2 Move Left Machine
65.3 Halt Machine
65.4 Machines That Write to the Tape
66 Composing Turing Machines
66.1 Design Idea
66.2 Tests
66.3 Transition Function
66.4 Implementation
67 A Programmed Turing Machine
67.1 Moving the Head Right n Times
67.2 Design Idea
67.3 Tests
67.4 Transitions
67.5 Implementation
68 The Universal Turing Machine
68.1 Syntax
68.2 Design Principles
69 Computing with Turing Machines
69.1 f(a b) = a + b
69.1.1 Design Idea
69.1.2 State Documentation
69.1.3 Transitions
69.1.4 Implementation
69.1.5 Correctness
69.2 copy(w) = w BLANK w
69.2.1 Design Idea
69.2.2 Implementation
69.2.3 Correctness
17 Turing Machine Extensions
70 The Multitape Turing Machine
71 L = {w | w Has Equal Number of as, bs, and cs}
71.1 Name, Alphabet, and Precondition
71.2 Unit Tests
71.3 Conditions and States
71.4 Transition Relation
71.5 Machine Implementation and Testing
71.6 Invariant Predicates
71.6.1 The S Invariant Predicate
71.6.2 The C Invariant Predicate
71.6.3 The D Invariant Predicate
71.6.4 The E Invariant Predicate
71.6.5 The F Invariant Predicate
71.6.6 The G Invariant Predicate
71.6.7 The Y Invariant Predicate
71.6.8 The N Invariant Predicate
71.7 Visualizing mttms
71.8 Proving L(EQABC) = L
71.8.1 Proving Invariants Hold
71.8.2 L(EQABC) = L
72 tm and mttm Equivalence
72.1 Design Idea
72.2 Proof Sketch
73 Turing Machines and Pushdown Automata: Programming Project
74 Other Turing Machine Extensions
74.1 Multiple Heads
74.2 Two-Way Infinite Input Tape
18 Context-Sensitive Grammars
75 Formal Definition
76 A csg for L = anbncn
76.1 Design Idea
76.2 Name, Alphabet, and Syntactic Categories
76.3 Production Rules
76.4 Tests
76.5 Implementation and Testing
77 A csg for Adding Expressions
77.1 Design Idea
77.2 Name, Alphabet, and Syntactic Categories
77.3 Production Rules
77.4 Tests
77.5 Implementation and Testing
78 Equivalence of csgs and tms
19 Church-Turing Thesis and Undecidability
79 The Halting Problem
80 Reduction Proofs
81 Undecidable Problems About Turing Machines
81.1 M Halts on EMP
81.2 There Exists a Word for Which M Halts
81.3 Does M Ever Reach Q Given w?
82 Undecidable Problems About Grammars
82.1 Determine if w Is in the Language of a Grammar
82.2 Is L(G) Empty?
20 Complexity
83 Equivalence of Deterministic and Nondeterministic Turing Machines
83.1 Design Idea
83.2 Correctness
84 Does Solvable Mean a Practical Solution?
85 The Class P
85.1 Defining Practical Solutions
85.2 Closure Under Complement
86 The 2-Satisfiability Problem
86.1 Representing Input Formulae
86.2 Parsing Input Formulae
86.3 The Formula Parser
86.4 The 2-Satisfiability Solver
86.4.1 Design Idea
86.4.2 Testing
86.5 The Solver Function
86.5.1 Simplifying a Formula
86.5.2 The 2-Satisfiability Problem Is in P
87 A Language Not in P
88 The Class NP
89 The Boolean Satisfiability Problem Is in NP
90 Unsolved Problems
Part V Epilogue
21 Where to Go from Here