RULER-EXTENDERS

control for ACL2's termination and induction analyses
Major Section:  SWITCHES-PARAMETERS-AND-MODES

Introduction

Consider the following recursive definition, which returns a list of threes of length one more than the length of x.

  (defun f (x)
    (cons 3
          (if (consp x)
              (f (cdr x))
            nil)))
One might expect ACL2's termination analysis to admit this function, since we know that (cdr x) is ``smaller'' than x if (consp x) is true. (By default, ACL2's notion of ``smaller'' is ordinary natural-number <, and the argument x is measured by applying function acl2-count to x.) However, that termination analysis does not consider IF tests, like (consp x) above, when they occur under calls of functions other than IF, such as CONS in the case above.

One way to overcome this problem is to ``lift'' the IF test to the top level, as follows.

  (defun f (x)
    (if (consp x)
        (cons 3 (f (cdr x)))
      (cons 3 nil)))
But another way to overcome the problem is to tell ACL2 to extend its termination (and induction) analysis through calls of cons, as follows.
  (defun f (x)
    (declare (xargs :ruler-extenders (cons)))
    (cons 3
          (if (consp x)
              (f (cdr x))
            nil)))
You may even wish to provide value :all instead of an explicit list of ruler-extenders, so that no function call blocks the termination analysis:
  (defun f (x)
    (declare (xargs :ruler-extenders :all))
    (cons 3
          (if (consp x)
              (f (cdr x))
            nil)))
Alternatively, you can omit the XARGS :RULER-EXTENDERS form, instead modifying the global default set of ruler-extenders:
  (set-ruler-extenders :all)

; or, for example: (set-ruler-extenders '(cons prog2$))

We conclude this introduction by considering the handling of LET expressions by termination analysis. Consider the following example.
  (defun fact (n)
    (the (integer 1 *)
         (if (posp n)
             (* n (fact (1- n)))
           1)))
ACL2 treats the call of THE in the body of this definition as follows.
  (let ((var (if (posp n)
                 (* n (fact (1- n)))
               1)))
    (if (and (integerp var) (<= 1 var))
        var
      <some_error>))
A LET expression, in turn, is treated as a LAMBDA application:
  ((lambda (var)
     (if (if (integerp var)
             (not (< var 1))
           nil)
         var
       <some_error>))
   (if (posp n)
       (* n (fact (1- n)))
     1))
Notice that the posp test, which governs the recursive call of fact, is inside an argument of a function application, namely the application of the LAMBDA expression. So by default, ACL2 will not consider this posp test in its termination analysis. The keyword :LAMBDAS in the list of ruler-extenders denotes all calls of lambda expressions, much as the inclusion of CONS in the ruler-extenders denotes all calls of CONS. The following definition is thus accepted by ACL2.
  (defun fact (n)
    (declare (xargs :ruler-extenders (:lambdas)))
    (the (integer 1 *)
         (if (posp n)
             (* n (fact (1- n)))
           1)))
As a convenience, ACL2 allows the symbol :lambdas in place of (:lambdas), and in fact the former will also include the default ruler-extenders, PROG2$ and EC-CALL.

IMPORTANT REMARKS. (1) Notice that the argument to set-ruler-extenders is evaluated, but the argument to :RULER-EXTENDERS in XARGS is not evaluated. (2) Do not put macro names in your list of ruler-extenders. For example, if you intend that + should not block the termination analysis, in analogy to cons in the example above, then the list of ruler-extenders should include binary-+, not +. Of course, if you use :all then this is not an issue, but see the next remark. (3) Also please note that by taking advantage of the ruler-extenders, you may be complicating the induction scheme stored for the function, whose computation takes similar advantage of the additional IF structure that you are specifying.

Below we describe the notion of ruler-extenders in detail, as well as how to set its default using set-ruler-extenders.

Details

We begin by discussing how to set the ruler-extenders by using the macro set-ruler-extenders; below we will discuss the use of keyword :ruler-extenders in XARGS declare forms.

Examples:
(set-ruler-extenders :basic) ; return to default
(set-ruler-extenders *basic-ruler-extenders*) ; same as immediately above
(set-ruler-extenders :all) ; every governing IF test rules a recursive call
(set-ruler-extenders :lambdas) ; LET does not block termination analysis
(set-ruler-extenders (cons :lambdas *basic-ruler-extenders*))
                               ; same as immediately above
(set-ruler-extenders '(f g)) ; termination analysis goes past calls of f, g

General Form: (set-ruler-extenders val)

where val evaluates to one of :basic, :all, :lambdas, or a true list of symbols containing no keyword other than, optionally, :lambdas.

When a recursive definition is submitted to ACL2 (in :logic mode), the recursion must be proved to terminate; see defun. More precisely, ACL2 explores the IF structure of the body of the definition to accumulate the tests that ``rule'' any given recursive call. The following example reviews how this works. Suppose that f has already been defined.

  (defun g (x y)
    (declare (xargs :measure (+ (acl2-count x) (acl2-count y))))
    (if (consp x)
        (g (cdr x) y)
      (if (consp y)
          (f (g x (cdr y)))
        (f (list x y)))))
ACL2 makes the following response to this proposed definition. Notice that the :measure proposed above must be proved to be an ACL2 ordinal -- that is, to satisfy O-P -- and that the arguments to each recursive call must be smaller (in the sense of that measure and O<, which here reduces to the ordinary < relation) than the formals under the assumption of the ruling IF tests. The first IMPLIES term below thus corresponds to the recursive call (g (cdr x) y), while the second corresponds to the recursive call (g x (cdr y)).
  For the admission of G we will use the relation O< (which is known
  to be well-founded on the domain recognized by O-P) and the measure
  (+ (ACL2-COUNT X) (ACL2-COUNT Y)).  The non-trivial part of the measure
  conjecture is

Goal (AND (O-P (+ (ACL2-COUNT X) (ACL2-COUNT Y))) (IMPLIES (CONSP X) (O< (+ (ACL2-COUNT (CDR X)) (ACL2-COUNT Y)) (+ (ACL2-COUNT X) (ACL2-COUNT Y)))) (IMPLIES (AND (NOT (CONSP X)) (CONSP Y)) (O< (+ (ACL2-COUNT X) (ACL2-COUNT (CDR Y))) (+ (ACL2-COUNT X) (ACL2-COUNT Y))))).

Now consider the following alternate version of the above definition.
  (defun g (x y)
    (declare (xargs :measure (+ (acl2-count x) (acl2-count y))))
    (if (consp x)
        (g (cdr x) y)
      (f (if (consp y)
             (g x (cdr y))
           (list x y)))))
The first test, (consp x), still rules the first recursive call, (g (cdr x) y). And the negation of that test, namely (not (consp x)), still rules the second recursive call (g x (cdr y)). But the call of f blocks the top-down exploration of the IF structure of the body of g, so (consp y) does not rule that second recursive call, which (again) is (g x (cdr y)). As a result, ACL2 fails to admit the above definition.

Set-ruler-extenders is provided to overcome the sort of blocking described above. Suppose for example that the following event is submitted:

  (set-ruler-extenders '(f))
Then the alternate definition of g above is admissible, because the call of f no longer blocks the top-down exploration of the IF structure of the body of g: that is, (consp y) becomes a ruler of the recursive call (g x (cdr y)). In this case, we say that f is a ``ruler-extender''. The same result obtains if we first submit
  (set-ruler-extenders :all)
as this removes all function calls as blockers of the top-down analysis. In other words, with :all it is the case that for every recursive call, every test argument of a superior call of IF contributes a ruler of that recursive call.

ACL2 handles LET (and LET*) expressions by translating them to LAMBDA expressions (see term). The next examples illustrates termination analysis involving such expressions. First consider the following (admittedly inefficient) definition.

  (defun fact (n)
    (let ((k (if (natp n) n 0)))
      (if (equal k 0)
          1
        (* k (fact (+ -1 k))))))
ACL2 translates the body of this definition to a LAMBDA application, essentially:
  ((lambda (k)
     (if (equal k 0)
         1
       (* k (fact (+ -1 k)))))
   (if (natp n) n 0))
As with the application of any function other than IF, the top-down termination analysis does not dive into arguments: the LAMBDA blocks the continuation of the analysis into its argument. But here, the argument of the LAMBDA is (if (natp n) n 0), which has no recursive calls to consider anyhow. What is more interesting: ACL2 does continue its termination analysis into the body of the LAMBDA, in an environment binding the LAMBDA formals to its actuals. In this case, the termination analysis thus continues into the term
  (if (equal k 0)
      1
    (* k (fact (+ -1 k))))
in the environment that binds k to the term (if (natp n) n 0). Thus, the proof obligation is successfully discharged, as reported by ACL2:
  For the admission of FACT we will use the relation O< (which is known
  to be well-founded on the domain recognized by O-P) and the measure
  (ACL2-COUNT N).  The non-trivial part of the measure conjecture is

Goal (IMPLIES (NOT (EQUAL (IF (NATP N) N 0) 0)) (O< (ACL2-COUNT (+ -1 (IF (NATP N) N 0))) (ACL2-COUNT N))). ..... Q.E.D.

That completes the proof of the measure theorem for FACT.

But now consider the following definition, in which the recursion takes place inside the argument of the LAMBDA rather than inside the LAMBDA body.

  (defun app (x y)
    (let ((result (if (endp x)
                      y
                    (cons (car x)
                          (app (cdr x) y)))))
      (if (our-test result)
          result
        0)))
Writing the body in LAMBDA notation:
  ((lambda (result)
     (if (our-test result) 
         result
       0))
   (if (endp x)
       y
     (cons (car x)
           (app (cdr x) y))))
By default, the LAMBDA call blocks the top-down termination analysis from proceeding into the term (if (endp x) ...). To solve this, one can submit the event:
  (set-ruler-extenders :lambdas)
The above definition of app is then admitted by ACL2, because the termination analysis is no longer blocked by the LAMBDA call.

The example just above illustrates that the heuristically-chosen measure is suitably sensitive to the ruler-extenders. Specifically: that measure is the application of acl2-count to the first formal parameter of the function that is tested along every branch of the relevant IF structure (as determined by the rulers) and occurs as a proper subterm at the same argument position in every recursive call. The heuristics for choosing the controller-alist for a definition rule are similarly sensitive to the ruler-extenders (see definition).

The remarks above for defun events are equally applicable when a definition sits inside a mutual-recursion event, except of course that in this case, a ``recursive call'' is a call of any function being defined by that mutual-recursion event.

Rules of class :definition are sensitive to set-ruler-extenders in analogy to the case of defun events.

This macro generates a call (table acl2-defaults-table :ruler-extenders val) and hence is local to any books and encapsulate events in which it occurs. See acl2-defaults-table. The current list of ruler-extenders may be obtained as

  (cdr (assoc-eq :ruler-extenders 
       (table-alist 'acl2-defaults-table (w state))))
or more conveniently, as:
  (default-ruler-extenders (w state))

Note that evaluation of (set-ruler-extenders lst), where lst evaluates to a list, does not necessarily include the default ruler-extenders -- i.e., those included for the argument, :basic -- which are the elements of the list constant *basic-ruler-extenders*, namely prog2$ and ec-call. You may, of course, include these explicitly in your list argument.

We conclude our discussion by noting that the set of ruler-extenders can affect the induction scheme that is stored with a recursive definition. The distributed book books/misc/misc2/ruler-extenders-tests.lisp explains how induction schemes are derived in this case. Consider the following example.

  (defun tree-of-nils-p (x)
    (if (consp x)
        (and (tree-of-nils-p (car x))
             (tree-of-nils-p (cdr x)))
      (null x)))
The above definition generates the following induction scheme. Note that (and u v) expands to (if u v nil), which explains why the term (tree-of-nils-p (car x)) rules the recursive call (tree-of-nils-p (cdr x)), resulting in the hypothesis (tree-of-nils-p (car x)) in the final conjunct below.
  (AND (IMPLIES (NOT (CONSP X)) (:P X))
       (IMPLIES (AND (CONSP X)
                     (NOT (TREE-OF-NILS-P (CAR X)))
                     (:P (CAR X)))
                (:P X))
       (IMPLIES (AND (CONSP X)
                     (TREE-OF-NILS-P (CAR X))
                     (:P (CAR X))
                     (:P (CDR X)))
                (:P X)))
Now consider the following variant of the above definition, in which a call of the function identity blocks the termination analysis.
  (defun tree-of-nils-p (x)
    (if (consp x)
        (identity (and (tree-of-nils-p (car x))
                       (tree-of-nils-p (cdr x))))
      (null x)))
This time the induction scheme is as follows, since only the top-level IF test contributes rulers to the termination analysis.
  (AND (IMPLIES (NOT (CONSP X)) (:P X))
       (IMPLIES (AND (CONSP X)
                     (:P (CAR X))
                     (:P (CDR X)))
                (:P X)))
But now suppose we first designate identity as a ruler-extender.
(set-ruler-extenders '(identity))
Then the induction scheme generated for the both of the above variants of tree-of-nils-p is the one shown for the first variant, which is reasonable because both definitions now produce essentially the same termination analysis.