Minimize-ruler-extenders
Minimize the ruler-extenders necessary to admit a definition.
Minimize-ruler-extenders is really two utilities. The first,
which we call MIN_NEW below, admits a proposed defun or defund
form by declaring a minimal set of ruler-extenders. This MIN_NEW
utility uses proof to eliminate ruler-extenders as completely as possible,
while still permitting the termination proof to succeed. The second utility,
which we call MIN_OLD below, is applied to a function symbol that already has
a recursive (but not mutually recursive) definition. Here are examples that
illustrate each of these two respective utilities.
; MIN_NEW (to admit a proposed definition):
(minimize-ruler-extenders
(defun foo (x)
(car (if (endp x)
x
(cons (foo (cdr x))
(evens (if (consp (cdr x))
(foo (cddr x))
nil)))))))
; MIN_OLD (to compute minimal ruler-extenders for an existing definition):
(defun bar (x)
(declare (xargs :ruler-extenders :all))
(mod (if (consp x)
(* (bar (car x))
(if (consp (cdr x))
(ifix (cadr x))
17))
3)
23))
(minimize-ruler-extenders bar) ; returns (MOD)
In the first (MIN_NEW) example above, a minimal set of ruler-extenders — in fact, THE minimal set — is the set
{car}. So the definition that is actually submitted, successfully, to
ACL2 is obtained by making that explicit:
ACL2 !>:pe foo
L 2:x(MINIMIZE-RULER-EXTENDERS (DEFUN FOO # ...))
\
>L (DEFUN FOO (X)
(DECLARE (XARGS :RULER-EXTENDERS (CAR)))
(CAR (IF (ENDP X)
X
(CONS (FOO (CDR X))
(EVENS (IF (CONSP (CDR X))
(FOO (CDDR X))
NIL))))))
ACL2 !>
The input form for the MIN_NEW utility should be a call of defun or
defund that defines a function symbol that is not already defined. If
that form specifies :ruler-extenders lst, then ACL2 will look for a
minimal subsequence of lst that can serve as the ruler-extenders.
Otherwise, ACL2 will start by additing an xargs declaration,
:ruler-extenders lst, where lst contains every plausible
ruler-extender, and then will try to find a minimal subsequence of
lst.
Now we turn to the MIN_OLD utility. This utility is applied to a function
symbol F that already has a (singly) recursive definition. It returns a
subset of the ruler-extenders R of F that is minimal in the
following sense: it provides the same induction-machine as R. (The
``induction-machine'' is an ACL2 data structure representing the scheme used
when doing induction based on the recursion in F.)
