`epsilon-0`

Major Section: MISCELLANEOUS

If `x`

and `y`

are both `e0-ordinalp`

s (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-ordinalp`

s. 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-ordinalp`

s.

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-ordinalp`

s we
mean that there is no infinite sequence of `e0-ordinalp`

s 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.