Next: Filling in Gaps
Up: State Minimization
Previous: State Minimization
Recall Theorem 3.2 reproduced in section 4. We
restate it here as:
Theorem 3.2 The automaton 
of Theorem 3.1 has
the least number of states of any automaton accepting 
, and any
automaton accepting with this minimum number of states is
isomorphic to .
There are several notable points about this theorem and its proof that
bear on their formalization. First, notice that the statement of the
theorem refers to which is defined in the proof of Theorem 3.1.
This is a very economical device, but it is more common to make such
definitions explicit as we do with lang_auto. This defines an
automaton 
given a function 
to define the final states. The
definitions are
Language
Language
Let us review the proof exactly as written in [17].
Proof. In the proof of Theorem 3.1 we saw that any finite
automaton 
accepting defines an
equivalence relation which is a refinement of 
. Thus the number of
states of 
is greater than or equal to the number of states of
of Theorem 3.1. If equality holds, then each of the states of can
be identified with one of the states of . That is, let 
be a
state of . There must be some 
in 
, such that
, otherwise could be removed from 
, and
a smaller automaton found. Identify with the state 
of . This identification will be consistent.
If 
, then, by Theorem
3.1, and 
are in the same equivalence class of . Thus
Qed
Notice that the properties of are proved in the context of
this specific theorem. There is no effort to abstract them as
general principles. So, for example, the notion of isomorphism is
only mentioned in the proof, but never defined. We make this explicit
in Automata_4 discussed below. In addition the key argument that
any automaton accepting defines a refinement of 
is a
observation from the proof of Theorem 3.1 that is not stated as a
separate fact. And the consequence that the number of states of
is greater than the number of is an important general fact that
is not abstracted from the theorem. We state these as separate
theorems card_le and card_ge.
*
*
A notable point about this Hopcroft and Ullman proof is that while it
is based on a nice idea, it is flawed because key details are
omitted. The correspondence between states is not shown to be an
isomorphism. (Hopcroft and Ullman don't hint at the proof they have
in mind.) Failing to prove this led them to insert a derivative fact, namely that the automaton is connected. This is not necessary. Let us
outline their argument again.
Next: Filling in Gaps
Up: State Minimization
Previous: State Minimization