Major Section: SWITCHES-PARAMETERS-AND-MODES
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
(cdr x)is ``smaller'' than
(consp x)is true. (By default, ACL2's notion of ``smaller'' is ordinary natural-number
<, and the argument
xis measured by applying function
x.) However, that termination analysis does not consider
(consp x)above, when they occur under calls of functions other than
IF, such as
CONSin 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
:allinstead 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
:RULER-EXTENDERSform, instead modifying the global default set of ruler-extenders:
(set-ruler-extenders :all)You can call the function
; or, for example: (set-ruler-extenders '(cons prog2$))
default-ruler-extendersas 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
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
THEin 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
LETexpression, in turn, is treated as a
((lambda (var) (if (if (integerp var) (not (< var 1)) nil) var <some_error>)) (if (posp n) (* n (fact (1- n))) 1))Notice that the
posptest, which governs the recursive call of
fact, is inside an argument of a function application, namely the application of the
LAMBDAexpression. So by default, ACL2 will not consider this
posptest in its termination analysis. The keyword
:LAMBDASin the list of ruler-extenders denotes all calls of lambda expressions, much as the inclusion of
CONSin 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
:lambdasin place of
(:lambdas), and in fact the former will also include the default ruler-extenders,
IMPORTANT REMARKS. (1) Notice that the argument to
is evaluated, but the argument to
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
+. Of course, if you use
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
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
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, gwhere
General Form: (set-ruler-extenders val)
valevaluates to one of
:lambdas, or a true list of symbols containing no keyword other than, optionally,
When a recursive definition is submitted to ACL2 (in
the recursion must be proved to terminate; see defun. More precisely, ACL2
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
:measureproposed 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
IFtests. The first
IMPLIESterm 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 isNow consider the following alternate version of the above definition.
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))))).
(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
fblocks the top-down exploration of the
IFstructure of the body of
(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
gabove is admissible, because the call of
fno longer blocks the top-down exploration of the
IFstructure 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
fis 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
:allit is the case that for every recursive call, every test argument of a superior call of
IFcontributes a ruler of that recursive call.
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 (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
LAMBDAblocks the continuation of the analysis into its argument. But here, the argument of the
(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
LAMBDAformals 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
kto 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
(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
LAMBDAcall 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
appis then admitted by ACL2, because the termination analysis is no longer blocked by the
The example just above illustrates that the heuristically-chosen measure is
suitably sensitive to the ruler-extenders. Specifically: that measure is the
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
Rules of class
definition are sensitive to
in analogy to the case of
This macro generates a call
(table acl2-defaults-table :ruler-extenders val)
and hence is
local to any books and
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
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
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
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
identityblocks 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
IFtest 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
identityas a ruler-extender.
(set-ruler-extenders '(identity))Then the induction scheme generated for the both of the above variants of
tree-of-nils-pis the one shown for the first variant, which is reasonable because both definitions now produce essentially the same termination analysis.