Project Website
Index
Table of Contents
Preliminaries
Generic Lemmas not in MathComp
Inverting surjective functions
Setoid Rewriting with Ssreflec's boolean inequalities.
Languages in Type Theory
Closure Properties for Decidable Languages
Deterministic Finite Automata
Regularity
Operations on DFAs
Cut-Off Criterion
Decidability of Language Equivalence
DFA for preimages of homomorphisms
Closure under Right Quotients
Closure under Left Quotients
Residucal Criterion
Pumping Lemma
Nondeterministic Finite Automata.
Epsilon NFAs
Equivalence of DFAs and NFAs
Operations on NFAs
Runs on NFAs
Regular Expressions
Regular Expressions to Finite Automata
Finite Automata to Regular Expressions (Kleene Construction)
Size Bound for Kleene Theorem
Regular expression for images of homomorphimsms
Regular Expression for word reversal
DFA Minimization
Uniqueness of connected and collapsed automata
Construction of the Connected Sub-Automaton
Quoitient modulo collapsing relation
Correctness of Minimization
Uniqueness of minimal automaton
Classifiers
Conversions between Classifiers and DFAs
Most General Classifiers
Two Way Automata
Preliminaries
Definition of 2NFAs and their languages.
Definition of 2DFAs as deterministic 2NFAs
Simulation of DFAs
Vardi Construction
Shepherdson Construction for 2NFAs
Imropoved Bound for Translation of 2DFAs to DFAs
Weak Monadic Second-Order Logic
Language-Theoretic Interpretation
Translation from MSO Formulas to NFAs
Correctness of the Translation
Regularity of the Language of an MSO formula
Translation from NFAs to WMSO