O<

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

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

o< 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 o<. The validity of this method rests on the well-foundedness of o< on the o-ps.

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 o-p. 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 (O< (m (d x)) (m x))).
When we say o< is ``well-founded'' on the o-ps we mean that there is no infinite sequence of o-ps 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 o-p for a discussion of the ordinals and how to compare two ordinals.

The definitional principle permits the use of relations other than o< 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.