unofficial copies [PDF], [PS]

by Robert L. Constable, Paul B. Jackson, Pavel Naumov, and Juan Uribe

Unpublished manuscript, Cornell University, 1996.

This article and the World Wide Web display of computer checked proofs is an experiment in the formalization of computational mathematics. Readers are asked to judge whether this formalization adds value in comparison to a careful informal account. The topic is state minimization in finite automata theory. We follow the account in Hopcroft and Ullman's book Formal Languages and Their Relation to Automata where state minimization is a corollary to the Myhill/Nerode theorem. That book constitutes one of the most compact and elegant published accounts. It sets high standards against which to compare any formalization.

The Myhill/Nerode theorem was chosen 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 forces us to treat quotient sets computationally.

The theorem proving methodology used here is based on the concept of tactics pioneered by Robin Milner. The theorem prover we use is Nuprl ("new pearl") which, like its companion, HOL, is a descendent of the LCF system of Milner, Gordon and Wadsworth. It supports constructive reasoning and computation.

Key Words and Phrases: automata, constructivity, congruence, equivalence relation, formal languages, LCF, Martin-Löf semantics, Myhill-Nerode theorem, Nuprl, program extraction, propositions-as-types, quotient types, regular languages, state minimization, tactics, type theory.