Background

It is widely believed that we know how to formalize large tracts of classical mathematics - namely write in the style of Bourbaki [5] using some version of set theory and fill in all the details. The Journal of Formalized Mathematics publishes results formalized in set theory and checked by the Mizar system. In fact, the topic of state minimization of finite automata has been formalized in Mizar [21]. Despite this belief, and the many formalizations accomplished, massive formalization is not a fait accompli, and there are many research issues related to the formalization effort and its computerization. Indeed, some doubt the appropriateness of set theory for expressing working mathematics [12].

In contrast, there is no general agreement on how to formalize computational mathematics. This article is a contribution to understanding that task and exploring one approach to it. Our approach stresses that formalized computational mathematics can be useful in carrying out computations. One of our subgoals is to illustrate this utility in a particular way. We want to show that constructive proofs can be used to synthesize programs.

Specifically, we want to examine whether constructive type theory is a natural expression of the basic ideas of computational mathematics in the same sense that set theory is for ``purely classical mathematics.'' We have explored this question for elementary number theory (), for the algebra of polynomials (), for elementary analysis, and for elementary logic, as well as in other less systematic efforts. The type theory we use is based on Martin-Löf's semantics [26].

In this paper we examine these ideas in the setting of basic automata theory. There are several reasons for this choice.

1. The subject of formalization is closely allied with other subjects in computer science (such as programming languages and semantics, applied logic, automated deduction, problem solving environments, computer algebra systems, knowledge representation, and computing theory). Also automata theory is widely taught in computer science [22] and used in building systems. So we hope for a large sympathetic audience for the material we create.

2. One of the most basic theorems in finite automata theory, the Myhill/Nerode Theorem, illustrates beautifully the idea that algorithms can be extracted from constructive proofs; so it is a good test for our main subgoal.

3. The account of Myhill/Nerode in Hopcroft and Ullman's famous book [17] is constructive except for a few small points, one buried deep in the proof. The nonconstructive steps are easy to miss. We show how to make the proof entirely constructive with a trivial change in the theorem.

4. Automata theory appears to be well suited for expression in type theory. If our account is not convincing on this material, then our task will be harder than we imagine. Moreover, the formal account seems to be clarifying and helpful even in the case of one of the most compact and elegant informal expositions of automata theory. So our claim that formalism adds value is put to a good test.

5. The Myhill/Nerode theorem illustrates a phenomenon that nonspecialists are curious about. Why does formalization expand the work and the text by such large factors (at least a factor of 5 in this case and ``under the surface'' by 3 orders of magnitude)? Moreover, because the formalization of this theorem relies heavily on many results in list theory and a few in algebra, we can see the impact of a knowledge base on the formalization task. Because it required building new basic material about the quotient type, we see why formalization efforts are so laborious.

6. The existence of an earlier formalization of the pumping lemma from automata theory by Christoph Krietz in 1988 [23] in Nuprl 3 allows us to compare the progress made in the tactic collection from version 3 (1988) to version 4.2 (1995).

7. Finally, the formalization reveals some technical problems about how to formalize computational mathematics. The question involves reasoning about quotient sets, and it is a central technical concern of the formalization.