Formalizing

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 .

*T mn_12








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.

1. We define to mean . It is immediate that is extension invariant since .
2. To show that is of finite index is precisely to show . We know that the number of states of is an upper bound to this cardinality. The exact size is in fact the number of accessible states. This fact comes out as we argue finiteness.

   Finiteness of is proved by invoking the lemma in Automata_v_of_fin_is_fin,
   .
   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 finite_decidable_subset,
   .

3. We define on to be exactly when .
   We need to show that is functional which follows directly from the definition of .

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 invariant
1.
2.
3.
4.
5.
6.
7. is an Equivalence over

is extension invariant
8. is an Equivalence in by SidePF mn_12_read_SidePf07
))

6.
7.
8.
9. is an Equivalence in
10.
11.

by SidePF


12.
13.



is extension invariant