WELL-FOUNDED-RELATION

show that a relation is well-founded on a set 
Major Section:  RULE-CLASSES

See rule-classes for a general discussion of rule classes and how they are used to build rules from formulas. An example :corollary formula from which a :well-founded-relation rule might be built is as follows. (Of course, the functions pairp, lex2p, and ordinate would have to be defined first.) 

Example:
(and (implies (pairp x) (e0-ordinalp (ordinate x)))
     (implies (and (pairp x)
                   (pairp y)
                   (lex2p x y))
              (e0-ord-< (ordinate x) (ordinate y))))
The above example establishes that lex2p is a well-founded relation on pairps. We explain and give details below.

Exactly two general forms are recognized: 

General Forms
(AND (IMPLIES (mp x) (E0-ORDINALP (fn x)))      ; Property 1
     (IMPLIES (AND (mp x)                       ; Property 2
                   (mp y)
                   (rel x y))
              (E0-ORD-< (fn x) (fn y)))),
or 
(AND (E0-ORDINALP (fn x))                       ; Property 1
     (IMPLIES (rel x y)                         ; Property 2
              (E0-ORD-< (fn x) (fn y))))
where mp, fn, and rel are function symbols, x and y are distinct variable symbols, and no other :well-founded-relation theorem about fn has been proved. When the second general form is used, we act as though the first form were used with mp being the function that ignores its argument and returns t. The discussion below therefore considers only the first general form.

Note: We are very rigid when checking that the submitted formula is of one of these forms. For example, in the first form, we insist that all the conjuncts appear in the order shown above. Thus, interchanging the two properties in the top-level conjunct or rearranging the hyptheses in the second conjunct both produce unrecognized forms. The requirement that each fn be proved well-founded at most once ensures that for each well-founded relation, fn, there is a unique mp that recognizes the domain on which rel is well-founded. We impose this requirement simply so that rel can be used as a short-hand when specifying the well-founded relations to be used in definitions; otherwise the specification would have to indicate which mp was to be used.

Mp is a predicate that recognizes the objects that are supposedly ordered in a well-founded way by rel. We call such an object an ``mp-measure'' or simply a ``measure'' when mp is understood. Property 1 tells us that every measure can be mapped into an ACL2 ordinal. (See e0-ordinalp.) This mapping is performed by fn. Property 2 tells us that if the measure x is smaller than the measure y according to rel then the image of x under fn is a smaller than that of y, according to the well-founded relation e0-ord-<. (See e0-ord-<.) Thus, the general form of a :well-founded-relation formula establishes that there exists a rel-order preserving embedding (namely via fn) of the mp-measures into the ordinals. We can thus conclude that rel is well-founded on mp-measures.

Such well-founded relations are used in the admissibility test for recursive functions, in particular, to show that the recursion terminates. To illustrate how such information may be used, consider a generic function definition 

(defun g (x) (if (test x) (g (step x)) (base x))).
If rel has been shown to be well-founded on mp-measures, then g's termination can be ensured by finding a measure, (m x), with the property that m produces a measure: 
(mp (m x)),                                     ; Defun-goal-1
and that the argument to g gets smaller (when measured by m and compared by rel) in the recursion, 
(implies (test x) (rel (m (step x)) (m x))).    ; Defun-goal-2
If rel is selected as the :well-founded-relation to be used in the definition of g, the definitional principal will generate and attempt to prove defun-goal-1 and defun-goal-2 to justify g. We show later why these two goals are sufficient to establish the termination of g. Observe that neither the ordinals nor the embedding, fn, of the mp-measures into the ordinals is involved in the goals generated by the definitional principal.

Suppose now that a :well-founded-relation theorem has been proved for mp and rel. How can rel be ``selected as the :well-founded-relation'' by defun? There are two ways. First, an xargs keyword to the defun event allows the specification of a :well-founded-relation. Thus, the definition of g above might be written 

(defun g (x)
 (declare (xargs :well-founded-relation (mp . rel)))
 (if (test x) (g (step x)) (base x)))
Alternatively, rel may be specified as the :default-well-founded-relation in acl2-defaults-table by executing the event 
(set-default-well-founded-relation rel).
When a defun event does not explicitly specify the relation in its xargs the default relation is used. When ACL2 is initialized, the default relation is e0-ord-<.

Finally, though it is probably obvious, we now show that defun-goal-1 and defun-goal-2 are sufficient to ensure the termination of g provided property-1 and property-2 of mp and rel have been proved. To this end, assume we have proved defun-goal-1 and defun-goal-2 as well as property-1 and property-2 and we show how to admit g under the primitive ACL2 definitional principal (i.e., using only the ordinals). In particular, consider the definition event 

(defun g (x)
 (declare (xargs :well-founded-relation e0-ord-<
                 :measure (fn (m x))))
 (if (test x) (g (step x)) (base x)))
Proof that g is admissible: To admit the definition of g above we must prove 
(e0-ordinalp (fn (m x)))                        ; *1
and 
(implies (test x)                               ; *2
         (e0-ord-< (fn (m (step x))) (fn (m x)))).
But *1 can be proved by instantiating property-1 to get 
(implies (mp (m x)) (e0-ordinalp (fn (m x)))),
and then relieving the hypothesis with defun-goal-1, (mp (m x)).

Similarly, *2 can be proved by instantiating property-2 to get 

(implies (and (mp (m (step x)))
              (mp (m x))
              (rel (m (step x)) (m x)))
         (e0-ord-< (fn (m (step x))) (fn (m x))))
and relieving the first two hypotheses by appealing to two instances of defun-goal-1, thus obtaining 
(implies (rel (m (step x)) (m x))
         (e0-ord-< (fn (m (step x))) (fn (m x)))).
By chaining this together with defun-goal-2, 
(implies (test x)
         (rel (m (step x)) (m x)))
we obtain *2. Q.E.D.