E0-ORD-<

the well-founded less-than relation on ordinals up to epsilon-0
Major Section:  MISCELLANEOUS

If x and y are both e0-ordinalps (see e0-ordinalp) then (e0-ord-< x y) is true iff x is strictly less than y. e0-ord-< is well-founded on the e0-ordinalps. When x and y are both nonnegative integers, e0-ord-< is just the familiar ``less than'' relation (<).

e0-ord-< plays a key role in the formal underpinnings of the ACL2 logic. In order for a recursive definition to be admissible it must be proved to ``terminate.'' By terminate we mean that the arguments to the function ``get smaller'' as the function recurses and this sense of size comparison must be such that there is no ``infinitely descending'' sequence of ever smaller arguments. That is, the relation used to compare successive arguments must be well-founded on the domain being measured.

The most basic way ACL2 provides to prove termination requires the user to supply (perhaps implicitly) a mapping of the argument tuples into the ordinals with some ``measure'' expression in such a way that the measures of the successive argument tuples produced by recursion decrease according to the relation e0-ord-<. The validity of this method rests on the well-foundedness of e0-ord-< on the e0-ordinalps.

Without loss of generality, suppose the definition in question introduces the function f, with one formal parameter x (which might be a list of objects). Then we require that there exist a measure expression, (m x), that always produces an e0-ordinalp. Furthermore, consider any recursive call, (f (d x)), in the body of the definition. Let hyps be the conjunction terms (each of which is either the test of an if in the body or else the negation of such a test) describing the path through the body to the recursive call in question. Then it must be a theorem that

  (IMPLIES hyps (E0-ORD-< (m (d x)) (m x))).
When we say e0-ord-< is ``well-founded'' on the e0-ordinalps we mean that there is no infinite sequence of e0-ordinalps such that each is smaller than its predecessor in the sequence. Thus, the theorems that must be proved about f when it is introduced establish that it cannot recur forever because each time a recursive call is taken (m x) gets smaller. From this, and the syntactic restrictions on definitions, it can be shown (as on page 44 in ``A Computational Logic'', Boyer and Moore, Academic Press, 1979) that there exists a function satisfying the definition; intuitively, the value assigned to any given x by the alleged function is that computed by a sufficiently large machine. Hence, the logic is consistent if the axiom defining f is added.

See e0-ordinalp for a discussion of the ordinals and how to compare two ordinals.

The definitional principle permits the use of relations other than e0-ord-< but they must first be proved to be well-founded on some domain. See well-founded-relation. Roughly put, alternative relations are shown well-founded by providing an order-preserving mapping from their domain into the ordinals. See defun for details on how to specify which well-founded relation is to be used.