The Nuprl system is designed to extract and execute the computational content of constructive theorems even when it is only implicitly mentioned. So it is possible to actually perform state minimization on an automaton without the need to write a separate minimization algorithm. Instead, just as Hopcroft and Ullman mention, we can extract the algorithm from the proof of the Myhill/Nerode theorem.
To illustrate this point concretely, note that given an automaton,
, Theorem 3.1 tells us that
will be the set of
states of the minimal machine and that this set is finite. Indeed,
we should be able to compute the size,
. We
have carried out this computation for some automata in Automata_6.
With the proofs as we initially completed them, the complexity of the minimization algorithm was exponential in the number of states. However, recent work by Aleksy Nogin on the formalization, Improving the efficiency of Nuprl Proofs [27], has reduced the complexity to a low-order polynomial; this is now displayed on the Web.