If we want to compute on an automaton like , then we probably
want to use a more convenient representation where the states are
natural numbers. We can define this directly in terms of the
finiteness theorem for
Suppose has
states, then there are maps
We could define the canonical minimal automaton, , in Automata
by
It is now straight forward to build an isomorphism between and
and between
and
of the theorem. (In this case the
onto property is proved as
.)
We can summarize the minimization work in the following way. First,
we take the disjoint union of Automata over all finite types
for states. In type theory this is
The minimization result can be stated as: For every automaton over
, there is an equivalent one with the minimum number of states.
To formalize this, we write
to mean that they accept the same languages,
i.e.
Then we say
is minimal iff for any other
equivalent
to
,
has at least as many states.
Now we can easily prove
Minimization Theorem:
From this theorem we can extract a function which
produces the minimal machine.
In Automata_5we show also that the minimal automaton is connected, where connected is defined in Automata_4as
Define where
was defined before as
Theorem :
We also show that the minimal automaton is unique up to isomorphism among all connected automata. Isomorphism is defined in Automata_4as:
Theorem ():