Control for ACL2's termination and induction analyses

**Introduction**

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

(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 `ACL2-count` to `if` tests, like

In the example above, we say that the term *governs*
the recursive call *rule* that
call. Roughly speaking, the set of *governors* of a subterm occurrence
in a given term consists of all superior *rulers* of the occurrence only includes, at least by default,
those tests and their negations from the top-level

(if a (if (if b c d) e f) (if g (foo (if h i j)) k))

For the occurrence of

We have seen that for a subterm occurrence in a term, every ruler is a governor but not necessarily vice-versa. It is the rulers of a recursive call that affect its role in the termination and induction analysis for a function.

One way to overcome the discrepancy between rulers and governors is to
``lift'' the

(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

(defun f (x) (declare (xargs :ruler-extenders (cons))) (cons 3 (if (consp x) (f (cdr x)) nil)))

Let's look at one more (contrived) example:

(defun g (x) (if (atom x) x (len (if (symbolp (car x)) (g (cddr x)) (g (cdr x))))))

There are two recursive calls, and the set of rulers is

You may even wish to provide value

(defun f (x) (declare (xargs :ruler-extenders :all)) (cons 3 (if (consp x) (f (cdr x)) nil)))

Alternatively, you can omit the

(set-ruler-extenders :all) ; or, for example: (set-ruler-extenders '(cons return-last))

You can call the function `default-ruler-extenders` as follows to see
the current global default set of ruler-extenders:

(default-ruler-extenders (w state))

We conclude this introduction by considering the handling of

(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
`posp` test in its termination analysis. The keyword

(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 `return-last`, which comes from macroexpansion of calls
of `prog2$`, `ec-call`, and others; `mv-list`; and `if`, which affects termination analysis through the first argument of calls of

IMPORTANT REMARKS.

- Notice that the argument to
set-ruler-extenders is evaluated, but the argument to:RULER-EXTENDERS inXARGS is not evaluated. - 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 tocons in the example above, then the list of ruler-extenders should includebinary-+ , not+ . Of course, if you use:all then this is not an issue, but see the next remark. - Also please note that by taking advantage of the ruler-extenders, you may
change the induction scheme computed for the function. This is especially
worth remembering for functions containing
`let`or`let*`expressions (which translate to`lambda`applications; see term). If the induction scheme suggested by such a function seems to provide more induction hypotheses than appear necessary, it might help to admit the function with:lambdas included among the ruler extenders even if that is not necessary for the termination proof. This can cause the induction scheme to have a richer case analysis with fewer induction hypotheses on any given induction step. While this can make it more difficult for the system to merge induction schemes to get an appropriate induction, it can also make the proof of each induction step easier. Unfortunately, we have no more precise advice as to exactly when adding:lambdas will help.

To see the ruler-extenders of an existing function symbol,

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

**Details**

We begin by discussing how to set the ruler-extenders by using the macro
`xargs` `declare` forms. NOTE: The legal
values discussed below for `xargs` keyword.

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

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

(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

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,

(set-ruler-extenders '(f))

Then the alternate definition of

(set-ruler-extenders :all)

as this removes all function calls as blockers of the top-down analysis.
In other words, with

ACL2 handles `let` (and `let*`) expressions by translating them
to

(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 (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 (equal k 0) 1 (* k (fact (+ -1 k))))

in the environment that binds

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

(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 (result) (if (our-test result) result 0)) (if (endp x) y (cons (car x) (app (cdr x) y))))

By default, the

(set-ruler-extenders :lambdas)

The above definition of

The example just above illustrates that the heuristically-chosen measure is
suitably sensitive to the ruler-extenders. Specifically: that measure is the
application of `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

This macro generates a call `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 `return-last` `mv-list`, and `if`. 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
community book

(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 (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

(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

(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

(set-ruler-extenders '(identity))

Then the induction scheme generated for the both of the above variants of

- Default-ruler-extenders
- The default ruler-extenders for
`defun`'d functions