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 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 `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: `RETURN-LAST`

(which comes from macroexpansion of calls
of `PROG2$`

, `EC-CALL`

, and others) and `MV-LIST`

.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
`return-last`

and `mv-list`

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