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.
