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.
