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 rewrites the
bodies of quoted lambda objects when they occur in slots of ilk
:FN. However, there are restrictions on which lambda objects are
rewritten, restrictions on the techniques available to the rewriter during
the rewriting of lambda bodies, and restrictions controlling whether the
rewritten object replaces the original object or is is ignored. We explain
below.
When Rewriting of lambda Objects Is Attempted
The rewriter attempts to rewrite the body of a quoted lambda constant
provided
- (a) it occurs in a :FN position of a call of a scion,
- (b) the rune (:executable-counterpart rewrite-lambda-modep))
is enabled (which it is by default),
- (c) the lambda object is well-formed (see well-formed-lambda-objectp),
- (d) every function symbol mentioned in the body has been warranted
Condition (c) 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
warranted (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 (d) 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 rewrite the unquoted body.
If (a) and (b) above hold but either (c) or (d) 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 two ways when rewriting lambda
bodies.
First, 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.)
Second, 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.
What Happens After Rewriting a Lambda Body
Upon rewriting 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. You may turn these warnings off with (toggle-inhibit-warning "Rewrite-lambda-object").
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) arises when
forcing has been disabled and the offending function symbol's warrant is not
among the hypotheses; enabling forcing or adding the warrant as a hypothesis
is recommended.
The warning message noted above can become annoying. It can be inhibited
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).
