Filling in Gaps in Textbook Proof

the proof
We are given and a specific machine they call which accepts it. We call this machine . They let be any other machine accepting ; by Theorem 3.1 we know hence . If is also minimal, then . Using this equality they define a map from to ; let's call it . They show is well defined and claim without proof that it is an isomorphism.

The definition of is on the connected set of states, say Given such a let be any string such that , then define This is well-defined because if we pick a different string taking us from to , say with , then mod so mod by Theorem 3.1. Thus .

It is not hard to show that is an isomorphism between and the states of . This implies that . But Hopcroft and Ullman do not carry out this argument. (Instead, they prove separately that ) Let us see what the right argument is.

First we show that is onto. Given a state of , notice that is in for any and that . This means that is onto which means

If is not 1-1, then . But . Since , then , and since we are assuming , then . So . Thus it is contradictory to assert that is not 1-1. (By classical logic this means that is 1-1. Constructively, this is true as well since the property of being 1-1 in these types is decidable.)

Notice that these final steps are subtle in terms of constructive reasoning. They also use basic facts about finite sets that are habitually considered ``immediately'' or ``obviously'' true. But they are in fact not ``obvious'' to Nuprl until we prove them.

a lacuna
There is another gap in the proof that is glossed over even in the above more detailed account. That account assumes that we can compute with equivalence classes as if they were concrete objects. As sets they are ``infinite objects,'' so we have adopted the approach of quotient types discussed in section 4.3.

In order to precisely define the isomorphism discussed above, we need to assign an element of to in . We said that for some such that . But how do we find this ? The definition of assures that it exists, but the semantics of the set type does not allow us to use the witness in a proof of this fact.

We could use a much stronger definition of the connected set of states, requiring the string be kept with the state. That is, we could take Then the function has access to ; it is the witness in the second component of the pair.

An approach that is more similar to the Hopcroft and Ullman proof is to notice that we can actually compute the string given We could for example pick the least string with respect to the lexicographical ordering of . Suppose is this ordering. It is a well-ordering, and there is a least such that So we can define where computes the least . We will not actually formalize either of these approaches. It turns out that once we define the lexicographical ordering, then there is a more direct argument than the one in Hopcroft and Ullman. None of the facts about lexicographical ordering is mentioned in Hopcroft and Ullman.

We can avoid entirely the argument by contradiction (to being 1-1) whose computational version is complex. We briefly discuss our approach next. It is presented in Automata_7 on the Web.