Rewrite-lambda-object
rewriting lambda objects in :FN slots
Lambda objects are quoted constants passed to scions
and applied as functions by apply$. The ACL2 rewriter can be made to
replace the bodies of quoted lambda objects with (supposedly) simpler
bodies that are ev$ equivalent, when the lambda objects occur in
slots of ilk :FN. However, there are restrictions on which
lambda objects can be so simplified, restrictions on the techniques available
to the rewriter during the simplification of lambda bodies, and
restrictions controlling whether the simplified body replaces the original or
is ignored. We explain below.
When an Occurrence of a lambda Objects Is Eligible
An occurrence of a quoted lambda object is eligible to be simplified
provided
- (a) it occurs in a :FN position of a call of a scion,
- (b) the lambda object is well-formed (see well-formed-lambda-objectp),
- (c) every function symbol mentioned in the body has been warranted
However, eligible quoted lambda objects are not modified at all if
the rune (:executable-counterpart rewrite-lambda-modep) is disabled. That rune is enabled by default.
Condition (b) implies the body of the lambda is in fact a well-formed
ACL2 term (so the rewriter can explore it), every function symbol in it is
badged (so that function objects mentioned are used properly), that
every variable symbol occurring freely in the body is among the formals of
the lambda object, and together with (c) implies that the term
``behaves'' as expected if the appropriate warrant hypotheses govern this
occurrence of the object. This last implication means that ev$ of
the body is equal to unquoted body (under a suitable assignment), which means
we can replace the unquoted body.
If (a) holds but either (b) or (c) fails, then a
"rewrite-lambda-object" warning message is printed during the proof.
However, this message is only printed once per lambda object per proof
attempt because otherwise the presence of ill-formed lambda-like objects
in a conjecture will litter the output with repeated warnings. You may turn
these warnings off with (toggle-inhibit-warning
"Rewrite-lambda-object").
Restrictions During Rewriting of a Lambda Body
The rewriter is restricted in three ways when rewriting the bodies of
eligible occurrences of lambda objects.
First, the user can specify one of two actions the rewriter can take on an
eligible lambda object occurrence (in addition to taking no action as
controlled by the rewrite-lambda-modep rune mentioned above). The
available actions are to recursively call the rewriter and normalize the
result, or to do syntactic cleaning only. The default is recursive
rewriting, with the restrictions explained in below. Syntactic cleaning just
eliminates declarations, guards, and various tags irrelevant to the logical
value of the body. We describe how the user specifies the action to be used
in rewrite-lambda-object-actions. We give more details about these
two kinds of lambda body simplification in rewriting-versus-cleaning-up-lambda-objects.
Second, warrant hypotheses in the goal clause are the only
contextual information ``imported'' from the goal clause and made available
while rewriting a lambda body. That means type information about
variables and other terms is forgotten, as are any linear arithmetic
relationships. The reason is simple: the variables in the body are in a
different scope than the variables outside the lambda object. Put
another way, we do not know, in general, to what the lambda object will
eventually be applied and so, in ACL2's untyped logic, we know nothing about
its formal variables.
(Actually, we not only ``import'' the warrants from the goal clause, we
import every ground hypothesis governing the lambda object's occurrence.
But practically speaking that means we only import warrant hypotheses. A
more sophisticated handling of contextual information can be imagined. For
example, if the lambda object occurs as the first argument of a loop$ scion, like collect$ or sum$, then the rewriter could
perhaps extract type information from the target and import that information.
For example, perhaps every element of the target is a number. In that case,
since we know the lambda object in a loop$ scion call is only
applied to elements of that list, we would then be allowed to assume the
corresponding formal of the lambda object is a number. But that more
sophisticated handling of contextual information has not been
implemented.)
Third, recursive functions are never opened when rewriting lambda
bodies. For example, if (len (cons e x)) occurs in a lambda body,
you might expect it to be simplified to (+ 1 (len x)), because that is
what generally happens to that term when occurrences outside lambda
objects are rewritten. ACL2 normally controls the expansion of recursive
functions by reference to terms that already occur within the current goal.
But the lambda object effectively shares no variables with the
surrounding goal and those heuristics are inapplicable. Preliminary
experiments with allowing expansions of recursive functions inside
lambda objects have produced unsatisfactory results such as runaway
expansions. So at the moment we allow no recursive expansions.
The ACL2 implementors hope to address both of the above problems in
eventual future releases.
Syntactic cleaning, in contrast to the restricted rewriting just
described, eliminates declarations, guards, and other compiler-related tags
introduced by translation of lambda$ and loop$. It does beta
reduction, which eliminates local variable names (other than the formals of
the lambda object). And it replaces the last argument of calls of
do$ by nil if that argument is a quoted constant other
than nil. (This argument is irrelevant to the value of the
do$ term and only used in error reporting.)
What Happens After Rewriting a Lambda Body
After the specified action on the body, b, of
(lambda(v1...vn)b) to produce b' the
decision must be made as to whether to return the lambda with the
rewritten body, (lambda(v1...vn)b'), or to
ignore the rewrite and return the original (unrewritten) object. ACL2
ignores the rewrite and returns the original lambda object if any of the
following three cases obtains:
- (a) b' contains variables other than
the lambda formals v1,...,vn,
- (b) b' is not tame, or
- (c) some function symbol appearing in b' has no warrant
hypothesis in the goal clause but forcing is disabled (see force).
In all cases, the rewriter prints a "rewrite-lambda-object" warning
when the rewritten body is different from the original one but the rewrite is
rejected. The warning message displays the before and after lambda
objects, lists the rewrite rules used, and explains which of the three
conditions above was violated. However, this message is only printed once
per lambda object per proof attempt because otherwise the presence of a
lambda object that rewrites inappropriately will litter the output with
repeated warnings.
Condition (a) can arise if a rewrite rule introduces a free variable;
disabling that rewrite rule is recommended. Condition (b) can arise if some
rewrite rule introduces a function symbol that has not been warranted;
disabling that rule can often solve that problem but perhaps a better
response is to use defwarrant to issue a warrant for the offending
function symbol and then supply that warrant as a hypothesis to the goal; the
latter response is perhaps better because it means all the ``usual''
rewriting is done, normalizing terms as expected. Condition (c) can be
addressed by using defwarrant to issue a warrant for the offending
function symbol and enabling forcing (see force).
The warning message noted above can become annoying. You may turn these
warnings off with (toggle-inhibit-warning
"Rewrite-lambda-object").
Be advised that if the "rewrite-lambda-object" warning has been
inhibited (by you or some book included in your session) and then, when
looking at, say, the checkpoints in a failed proof, you see a lambda
object that you expected to be simplified but was not, you may think
rewriting was not attempted for it, for some reason, when in fact it was
attempted but rejected. You can (toggle-inhibit-warning
"Rewrite-lambda-object") and replay the proof attempt to see (all) the
rejected lambda object rewrites.
A Possible Confusion
A metafunction that is included in the book projects/apply/top can
also cause quoted lambda objects to be rewritten. This metafunction,
called relink-fancy-scion, is called on certain calls of the fancy
loop$ scions, e.g., calls of always$+, collect$+, sum$+, etc. The goal of that metafunction is to keep the list of ``global
variables'' in some normal form.
For example,consider the term
(collect$+ (quote
(lambda (loop$-gvars loop$-ivars)
(cons (car loop$-gvars)
(cons (car (cdr loop$-gvars))
(cons (car loop$-ivars) 'nil)))))
(list a b)
target)
which is (essentially) the translation of (loop$ for e in target
collect (list a b e)). Suppose that in some case of a proof about this
term the hypothesis (equal a b) governs this term. The term would thus
become
(collect$+ (quote
(lambda (loop$-gvars loop$-ivars)
(cons (car loop$-gvars)
(cons (car (cdr loop$-gvars))
(cons (car loop$-ivars) 'nil)))))
(list a a)
target)
Relink-fancy-scion will rewrite that term to
(collect$+ (quote
(lambda (loop$-gvars loop$-ivars)
(cons (car loop$-gvars)
(cons (car loop$-gvars)
(cons (car loop$-ivars) 'nil)))))
(list a)
target)
which eliminates the duplicate entry in the list of globals and, as a
necessary side effect, also replaces the body of the lambda object to
eliminate the term (car (cdr loop$-gvars)).
The application of the metafunction relink-fancy-scion can easily but
mistakenly be attributed to the rewriting of lambda objects but it is
not! The metafunction is applied to the whole collect$+ term (and calls
of every other fancy scion), not just the lambda object.
If you want to avoid this normalization of the globals, disable the rune (:meta relink-fancy-scion-correct).
