Formalizing the implication from (1) to (2) is quite direct and elegant in type theory. We go through it now step by step.
To say that a set is accepted by some finite automaton means that there is an automaton, say , accepting . This, in turn, presupposes a set of states, say such that Automata. So there is a mechanical translation of ``accepted by some finite automaton'' into
We are implicitly quantifying over and . This implicit translation is revealed in the first line of the proof, ``let be accepted by some ''
Statement (2) is:
is the union of some of the equivalence classes of an extension invariant equivalence relation of finite index.
Translating this requires an equivalence relation, called in the proof, so we call it in the statement
is defined as we would expect. It says that is an equivalence relation over . It is a specialization of
We need to assert that is of finite index which is just . must be extension invariant, i.e.
Next we consider how to express the idea of statement 2, that ``L is the (effective) union of some of the equivalence classes of an extension invariant equivalence relation of finite index.'' The most direct translation of this would use some idea of union of equivalence classes, say since there are finitely many. We could write where is a subset of the indexes 1 to . So, to say that the union is effective is to say that is a decidable set.
We don't want to express the union idea this way (even though we could), because we are using the language of quotient types rather than that of equivalence classes. That is, we don't need to bring in the type of equivalence classes because we can use the type instead.
We can transform into a statement about as follows. Suppose that a function picks out the classes in the union, so iff . Now notice that for , the equivalence classes are . So we have iff . The map must respect the equivalence relation , so it can actually be defined as a function . Each effective union determines such a map and conversely. Thus to say that is the effective union of some of the equivalence classes, we use a boolean valued function to pick out which classes.
That is, is in iff in Note, is also denoted .
Putting all this together we get the fully expanded formulation. It is named for Myhill-Nerode .
The above version of the theorem is the one displayed on the Web, but we have worked to make both the theorem and the proof more readable. It is instructive to see how this can be done.
We first decided to suppress some of the detail in the statement that
is an equivalence relation by using a less detailed display form.
The result is this display
Next we agreed to allow the assertion of a boolean without
displaying the assert symbol, so True becomes just .
Next we display extension invariance as a simple phrase, `` is
extension invariant.'' Finally we use a general abbreviation device
of suppressing the leading universal quantifiers since this is a
standard convention in mathematics, indeed used by Hopcroft and Ullman
for this theorem. The result is:
is extension invariant.
The proof of this theorem follows.
Finiteness of is proved by invoking the lemma in
We then prove the preconditions of the lemmas, mainly that
The proof of requires showing that if there is a such that , then there is a ``short'' , namely of length less than , the number of states. This is done by invoking the pumping lemma and its corollary from Automata_1.
This in turn requires the pigeon hole lemma of
Automata_1, phole_lemma. Finally, the proof of
inv_of_fin_is_fin requires the key Automata_3lemma
The main steps of the on-line proof are displayed below using a presentation format that can be automatically generated from a mark-up of the original proof. The tools for creating these more readable proofs were provided by Stuart Allen.
The key to this format is that parts of the proof are ``put aside'' to be read later, if at all. Allen calls these side proofs. They are indicated by the phrase SidePF followed by a name. In the on-line version it is possible to click on this proof to read it.
Automata is an Equivalence over is extension
7. is an Equivalence over
is extension invariant
8. is an Equivalence in by SidePF mn_12_read_SidePf07
9. is an Equivalence in
is extension invariant