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

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