Constructively Formalizing Automata Theory
Robert L. Constable, Paul B. Jackson, Pavel Naumov, Juan Uribe · The MIT Press eBooks · 2000
We present a constructive formalization of the Myhill-Nerode the-orem on the minimization of nite automata that follows the account in Hopcroft and Ullman's book Formal Languages and Their Relation to Automata. We chose to formalize this theorem because it illustrates many points critical to formalization of computational mathematics, especially the extraction of an important algorithm from a proof as a method of knowing that the algorithm is correct. It also gave us an opportunity to experiment with a constructive implementation of quotient sets. We carried out the formalization in Nuprl, an interactive theorem prover based on constructive type theory. Nuprl borrows an imple-mentation of the ML language from the LCF system of Milner, Gordon, and Wadsworth, and makes heavy use of the notion of tactic pioneered by Milner in LCF. We are interested in the pedagogical value of electronic formal mathematical texts and have put our formalization on the World Wide Web. Readers are invited to judge whether the formalization adds value in comparison to a careful informal account. Key Words and Phrases: automata, constructivity, congruence, equivalence relation, formal languages, foundational logic, LCF, logic, Martin-Lof semantics, Myhill-Nerode theorem, Nuprl, program extrac-