## RULER-EXTENDERS

control for ACL2's termination and induction analyses
```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 prog2\$))
```
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: `PROG2\$`, `EC-CALL`, 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-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 `prog2\$` and `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 distributed 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.