O<
The well-founded less-than relation on ordinals up to epsilon-0
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 recurs 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 of 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-rule. 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.
Function: o<
(defun o< (x y)
(declare (xargs :guard (and (o<g x) (o<g y))))
(cond ((o-finp x) (or (o-infp y) (< x y)))
((o-finp y) nil)
((not (equal (o-first-expt x)
(o-first-expt y)))
(o< (o-first-expt x) (o-first-expt y)))
((not (= (o-first-coeff x) (o-first-coeff y)))
(< (o-first-coeff x) (o-first-coeff y)))
(t (o< (o-rst x) (o-rst y)))))
