Rulers
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 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. (ACL2's notion of ``smaller'' here is essentially ordinary
natural-number <, and the argument x is measured by applying
function ACL2-count to x; see defun.) However, by default
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; it considers only rulers, as we now
discuss.
In the example above, we say that the term (consp x) governs
the recursive call (f (cdr x)) shown above, but does not rule that
call. Roughly speaking, the set of governors of a subterm occurrence
in a given term consists of all superior IF tests and their negations
that must be true in order for evaluation to reach that subterm; however, the
set of rulers of the occurrence only includes, at least by default,
those tests and their negations from the top-level IF structure of the
term — that is, tests and their negations that are collected by walking
through the true and false branches of IF calls, starting at the top.
Consider for example the following term, where foo is assumed to be a
function symbol.
(if a
(if (if b c d) e f)
(if g
(foo (if h i j))
k))
For the occurrence of c in that term, the only ruler is a; but
both a and b are governors. For the occurrence of i, (not
a) and g are the only rulers; but its governors are (not a),
g, and h.
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 IF test to the top level. We can apply that technique to
the defun of f above, so that now (consp x) is a ruler of the
recursive call, and not merely a governor (though it remains a governor as
well, of course).
(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, by designating that calls of cons should not block the
accumulation of rulers.
(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 {(not (atom
x))} for each of those. The set of governors for the first recursive call
is {(not (atom x)), (symbolp (car x))}, and for the second,
{(not (atom x)), (not (symbolp (car x)))}. The rulers is extended to be
the governors in each case if we specify:
(declare (xargs :ruler-extenders (len))).
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 three basic
ruler-extenders: 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
IF (it continues through the true and false branches of these calls even
without IF being among the ruler-extenders).
IMPORTANT REMARKS.
- Notice that the argument to set-ruler-extenders is evaluated, but the
argument to :RULER-EXTENDERS in XARGS 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
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.
- 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. See induction-coarse-v-fine-grained.
To see the ruler-extenders of an existing function symbol, fn, in a
logical world, wrld, evaluate (ruler-extenders 'fn wrld)
after (include-book
"kestrel/utilities/system/world-queries" :dir :system). For example,
evaluation of (ruler-extenders 'fn (w state)) provides the
ruler-extenders of fn in the current logical world.
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. NOTE: The legal
values discussed below for set-ruler-extenders are the same as the legal
values for the :ruler-extenders 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 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 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 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.
Subtopics
- Induction-coarse-v-fine-grained
- advice on case explosion in complex inductions
- Default-ruler-extenders
- The default ruler-extenders for defun'd functions
