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.
