Rewriting-versus-cleaning-up-lambda-objects
why change the default action on rewriting lambda objects
See rewrite-lambda-object and rewrite-lambda-object-actions for background information on how the ACL2
rewriter behaves on certain quoted lambda objects. In this topic we
discuss why you might want to change that behavior.
There are three basic actions the rewriter might take when it encounters
a suitable lambda object.
The reason we have several options has to do with the representation of
lambda objects as quoted constants in ACL2's first order logic. Distinct
lambda objects are unequal and yet sometimes by rewriting their bodies
to functionally equivalent terms under ev$ they can become identical.
For example, '(lambda (x) (+ 1 x)) and '(lambda (x) (+ x 1)) are
unequal list constants. But they are functionally equal and by rewriting
their bodies we can make them identical.
The problem is greatly magnified by the way lambda$ and loop$
expressions macroexpand into formal terms. Their expansions are complicated
with guards and tags that play key roles in their Common Lisp compilation and
execution efficiency within the ACL2 top-level read-eval-print loop. But
those guards and tags are irrelevant to their logical meanings. By
eliminating the guards and tags from quoted lambda objects in slots of
ilk :FN we increase the chances that different objects become
identical.
Consider the translation of a thereis loop$ statement. The
thereis loop$ operand looks for an element of the range that
satisfies a given predicate and returns the first non-nil value of that
predicate. The predicate is formally a lambda object. Below we
translate a thereis loop$ and show the result.
ACL2 !>:trans (loop$ for x on a
thereis
(if (equal (car x) b) x nil))
(RETURN-LAST
'PROGN
'(LOOP$ FOR X ON A
THEREIS
(IF (EQUAL (CAR X) B) X NIL))
(THEREIS$+
'(LAMBDA
(LOOP$-GVARS LOOP$-IVARS)
(DECLARE (XARGS :GUARD (IF (TRUE-LISTP LOOP$-GVARS)
(IF (EQUAL (LEN LOOP$-GVARS) '1)
(IF (TRUE-LISTP LOOP$-IVARS)
(EQUAL (LEN LOOP$-IVARS) '1)
'NIL)
'NIL)
'NIL)
:SPLIT-TYPES T)
(IGNORABLE LOOP$-GVARS LOOP$-IVARS))
(RETURN-LAST
'PROGN
'(LAMBDA$ (LOOP$-GVARS LOOP$-IVARS)
(DECLARE (XARGS :GUARD (AND (TRUE-LISTP LOOP$-GVARS)
(EQUAL (LEN LOOP$-GVARS) 1)
(TRUE-LISTP LOOP$-IVARS)
(EQUAL (LEN LOOP$-IVARS) 1))))
(LET ((B (CAR LOOP$-GVARS))
(X (CAR LOOP$-IVARS)))
(DECLARE (IGNORABLE E X))
(IF (EQUAL (CAR X) B) X NIL)))
((LAMBDA (B X)
(IF (EQUAL (CAR X) B) X 'NIL))
(CAR LOOP$-GVARS)
(CAR LOOP$-IVARS))))
(CONS B 'NIL)
(LOOP$-AS (CONS (TAILS A) 'NIL))))
=> *
The predicate being mapped is the quoted lambda object in the first
argument of the thereis$+. When shorn of the logically irrelevant
DECLARE and RETURN-LAST forms this particular quoted lambda
object becomes
'(LAMBDA
(LOOP$-GVARS LOOP$-IVARS)
((LAMBDA (B X)
(IF (EQUAL (CAR X) B) X 'NIL))
(CAR LOOP$-GVARS)
(CAR LOOP$-IVARS)))
But now consider the closely related thereis loop$ which is like
the one translated above but uses different names for the variables.
(loop$ for y on aaa
thereis
(if (equal (car y) bbb) y nil))
The lambda object representing the predicate in this loop$, when
shorn of logically irrelevant material, is
'(LAMBDA
(LOOP$-GVARS LOOP$-IVARS)
((LAMBDA (BBB Y)
(IF (EQUAL (CAR Y) BBB) Y 'NIL))
(CAR LOOP$-GVARS)
(CAR LOOP$-IVARS)))
But note that this lambda object contains the ``variables'' BBB
and Y where the earlier one contained B and X. However, they
are not really variables! They are symbol constants because they occur in
quoted list constants. Thus, the lambda object generated for the first
thereis loop$ is different from the lambda object generated
from the “closely related” one. They are just two different list
constants.
Thus, the translations of those two thereis loop$s are not
instances of one another. So if you proved a rewrite rule about the
(loop$ for x on ...B...) and then the rewriter encountered (loop$ for y
on ...BBB...) the rule would not match. (By the way, this problem has nothing
special to do with thereis loop$s. It happens on every kind of
loop$ because the problem has everything to do with representing
lambda expressions as list constants.)
Fortunately, it is sound to replace the body of a lambda object with
one that is equivalent under ev$. That can be done either by
rewriting the body or by syntactically cleaning the body. It turns out that
both rewriting and syntactic cleaning produce the same result in this case
and reduce these two distinct lambda objects to this one.
'(LAMBDA
(LOOP$-GVARS LOOP$-IVARS)
(IF (EQUAL (CAR (CAR LOOP$-IVARS))
(CAR LOOP$-GVARS))
(CAR LOOP$-IVARS)
'NIL))
Actually, all that is needed in this case is the beta reduction of the
two bodies.
Syntactic cleaning 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. (That argument is
irrelevant to the value of the do$ term and only used in error
reporting.) The logical semantics of loop$ is best understood not by
looking at its translation as we did above but by looking at the result of
syntactically cleaning its translation. That is done by the command
:tc. Tc translates its argument, in this case the
loop$ statement we've been studying, obtaining the large form shown
above, and then syntactically cleans it, returning the internal
representation of the logical semantics.
ACL2 !>:tc (loop$ for x on a
thereis
(if (equal (car x) b) x nil))
(THEREIS$+ '(LAMBDA
(LOOP$-GVARS LOOP$-IVARS)
(IF (EQUAL (CAR (CAR LOOP$-IVARS))
(CAR LOOP$-GVARS))
(CAR LOOP$-IVARS)
'NIL))
(CONS B 'NIL)
(LOOP$-AS (CONS (TAILS A) 'NIL)))
Note that the free variables of the term are A and B. The
iteration variable, x of the loop$ does not appear. Instances of
this term are formed by choosing instantiations of A and B.
(Note: The related command :tcp translates, cleans, and then
converts the internal form of the term into the “pretty”
user-level syntax. E.g., it converts the quoted LAMBDA constant above
to a lambda$ expression, converts the IF expression to an AND,
and converts the CONS terms into LIST terms. But for this
discussion it is really better to see the internal form. That LAMBDA
object above is really a list constant!)
Before a newly proved :rewrite or :linear
rule is stored, the conclusion is syntactically cleaned.
Like syntactic cleaning, rewriting eliminates declarations, guards, and
other compiler-related tags and does beta reduction — but these
transformations are generally carried out by rules whose enabled status can
be altered. Furthermore, rewriting applies :rewrite and other rules
which might commute terms, open function definitions, etc. We don't rewrite
the conclusions of newly proved rules simply because the enabled rules may
change from one event (or subgoal) to another.
As noted earlier, there are three basic actions the rewriter might take
when it encounters a suitable lambda object.
- recursively rewrite the body to get a new body,
- just clean it up syntactically, or
- do nothing — leave lambda object constants untouched.
Since rules are cleaned before storage, it is almost always the case that
you will want the prover either to rewrite lambda objects or
syntactically clean them. In simple cases, like a rule about the first
thereis loop$ above and a conjecture about the second, either
action by the prover reduces “closely related” lambda
objects to identical objects, making it more likely that rules will fire.
So which of the three actions do you want the rewriter to take when it
encounters an eligible lambda object?
- rewrite the body — best if there are multiple lambda objects
in the conjecture that need to be written to be identified, and in simple
cases rewriting is equivalent to syntactic cleaning
- syntactic cleaning — best if you want the lambda objects in
the conjecture to match :rewrite or :linear rules containing
closely related lambda objects, but you find that otherwise necessary
:rewrite rules cause the rewriter to “overshoot” the
syntactically cleaned term as illustrated further below
- hands off — fairly unuseful since rules are cleaned up before
storage. However, one use of this is if you prove a lemma containing a
lambda object but store it with :rule-classes nil and then
:use an instance of it in the :hints for some conjecture that
involves the very same lambda objects.
We now illstrate some typical problems that arise when proving theorems
about loop$s. These examples are documented in the book
books/projects/apply/rewriting-versus-cleaning-examples.
Why you might want to use syntactic cleaning: Suppose you prove the
:rewrite rule below. It says that a certain thereis loop$
computes the same answer as the function last.
(defthm loop$-can-be-last
(implies (listp a)
(equal (loop$ for x on a
thereis
(if (atom (cdr x)) x nil))
(last a))))
What term does this rule target? We can answer that by using the
:tc command.
ACL2 !>:tc (loop$ for x on a
thereis
(if (atom (cdr x)) x nil))
(THEREIS$ '(LAMBDA (LOOP$-IVAR)
(IF (ATOM (CDR LOOP$-IVAR))
LOOP$-IVAR 'NIL))
(TAILS A))
By the way, a more common way to see the rules created by an event is to
use the :pr command. But that command displays the terms of the
rule in user-level syntax and we want to see the internal form here. The
“lambda expression” is really a quoted constant.
Now imagine you are proving a conjecture that involves that identical (!)
loop$. Of course, translation will replace the loop$ by a rather
large tagged term containing compiler directives, etc. Shorn of that
material the term would become the thereis$ term above, but the
translation is what is in the initial Goal. Imagine further that you're
doing this proof in a theory that allows the rewriter to recursively rewrite
the bodies of quoted lambda objects, i.e., you are in a theory as
described by rewrite-lambda-objects-theory. ACL2 starts up in such a
theory and unless you've changed the enabled status of the
rewrite-lambda-modep runes rewriting lambda objects is the default
behavior.
You might expect the loop$-can-be-last rule to fire and replace the
thereis$ term in the Goal by (last a). But that will not
happen! The rule won't fire!
The reason is that before the rewriter rewrites the thereis$ term it
rewrites its arguments. The quoted lambda object in the Goal is
rewritten first. That is necessary because the translated loop$
contains tags, etc. But the rewriter does more than just clean up the body.
It “overshoots” and opens the nonrecursive function atom and
swaps the branches of the if to eliminate the not thus introduced.
The quoted lambda object becomes
'(LAMBDA (LOOP$-IVAR)
(IF (CONSP (CDR LOOP$-IVAR))
'NIL
LOOP$-IVAR))
So when the rewriter then tries to rewrite the thereis$ terms the
quoted lambda object in the rule does not match the one in the rewritten
Goal.
If the rewritten goal is printed, as it is likely to be a checkpoint, you
will see the rewritten body with the consp instead of atom in it.
As usual, pay attention to the checkpoints.
One way to respond to this problem would be to “hobble” the rewriter
by shifting over to syntactic cleaning of quoted lambda objects. This could
be done by providing a local subgoal hint in which you specify
:in-theory (syntactically-clean-lambda-objects-theory)
which would prevent the rewriter from diving into the bodies of
lambda objects and just clean them instead.
Why you should probably use rewriting: There is a deeper lesson
here than just that you might want to hobble the rewriter to prevent it from
diving into quoted lambda bodies. In our view the actual problem is
with the loop$-can-be-last rule itself. ACL2 users are taught to
express rules in maximally rewritten terms. No experienced user would pose a
rule with a non-recursive function like atom in its lefthand side. The
best response to this situation, which may or may not be practical depending
on how loop$-can-be-last came to be a rule in the session, is to change
that rule to
(defthm loop$-can-be-last
(implies (listp a)
(equal (loop$ for x on a
thereis
(if (consp (cdr x)) nil x))
(last a))))
This version of the rule would not only rewrite the thereis loop$ above
but rewrites
(loop$ for x on a
thereis
(if (atom (cdr x)) x nil))
because, as illustrated above, the rewriter by default dives into the
translated loop$ and “normalizes” the resulting
thereis$.
Furthermore, because and macroexpands to an if-term and beta
reduction eliminates local variable names it would rewrite
(loop$ for rest on (aaa aa)
thereis
(let ((z (cdr rest)))
(and (atom z) rest))
But not all such problems can be solved by switching between rewriting
quoted lambda objects and just cleaning them up!
Consider this rewrite rule. The thereis loop$ in the lefthand
side of the rule below is exactly the loop$ whose translation we showed
at the beginning of this topic. The cleaned up internal form of the lefthand
side is the thereis$+ term shown by the first :tc display in this
topic. The rule below says that the thereis loop$ in question
computes member.
(defthm loop$-can-be-member
(equal (loop$ for x on a
thereis
(if (equal (car x) b) x nil))
(member b a)))
You might expect that when the rewriter encounters (an instance of) such a
loop$ it will replace it by a member term. That is actually
true!
For example, if we then tried to prove a conjecture
mentioning
(loop$ for x on aaa
thereis
(if (equal (car x) bbb) x nil))
the loop$-can-be-member rule would fire and replace that loop$
by (member bbb aaa).
But it is easy to misjudge whether a given loop$ is an instance of
another.
Suppose our goal conjecture contained
(loop$ for x on (aaa aa)
thereis (if (equal (car x) (bbb bb)) x nil))
This loop$ looks like the loop$ in loop$-can-be-member
except we've used (aaa aa) instead of a, and (bbb bb) instead
of b.
Will that loop$ be rewritten to (member (bbb v) (aaa u))?
No!
To understand why not, we first have to compare the internal forms of the
two loop$s. Recall that the lefthand side of rewrite rules are cleaned up
before storage, so the internal form of the lefthand side of
loop$-can-be-member is in fact the thereis$+ term produced by
:tc above. If we are either rewriting lambda objects or just
syntactically cleaning lambda objects in the proof we're looking at, the
the internal forms of the loop$ in the conjecture will be just the
:tc of that loop$ (because there's nothing interesting to rewrite
here). So here is the lefthand side of the rule side-by-side with the
rewritten target in the conjecture. We have highlighted the differences in
uppercase and numbered the lines that contain differences.
lhs of rule target
(thereis$+ (thereis$+
'(lambda '(lambda
(loop$-gvars loop$-ivars) (loop$-gvars loop$-ivars)
(if (equal (if (equal
(car (car loop$-ivars)) (car (car loop$-ivars))
(CAR LOOP$-GVARS)) (BBB (CAR LOOP$-GVARS))) ; [1]
(car loop$-ivars) (car loop$-ivars)
'nil)) 'nil))
(cons B 'nil) (cons BB 'nil) ; [2]
(loop$-as (loop$-as
(cons (tails A) 'nil))) (cons (tails (AAA AA)) 'nil))) ; [3]
Note that the target is not an instance of the lefthand side of the rule
— but only because of the difference on line [1]. Lines [2] and [3] of
the lefthand side can be instantiated to become those lines in the target.
But because of [1] our loop$-can-be-member rule will not rewrite the
target shown here.
This kind of problem cannot be fixed by fiddling with how the prover
treats lambda objects. Instead, we need to transform the target
lambda object into the functionally different lambda object in the
rule while simultaneously changing how thereis$+ applies it. In
particular we need to transform target to target' below by moving
the BBB out of [1] and into [2] as shown below.
target target'
(thereis$+ (thereis$+
'(lambda '(lambda
(loop$-gvars loop$-ivars) (loop$-gvars loop$-ivars)
(if (equal (if (equal
(car (car loop$-ivars)) (car (car loop$-ivars))
(BBB (CAR LOOP$-GVARS))) (CAR LOOP$-GVARS)) ; [1]
(car loop$-ivars) (car loop$-ivars)
'nil)) 'nil))
(cons BB 'nil) (cons (BBB BB) 'nil) ; [2]
(loop$-as (loop$-as
(cons (tails (aaa aa)) 'nil))) (cons (tails (aaa aa)) 'nil)))
Note that target' is in fact an instance of the lefthand side of the
rule. But we've changed the semantics of the lambda object and changed
the way thereis$+ uses it by moving the BBB from the inside to the
outside of the lambda. No lambda rewriting can do this. Instead,
we need a rule that rewrites thereis$+. (In fact, a great project would
be to implement a metafunction that does this kind of optimization for all
loop$ scions. We just haven't done that yet. Let us know if you
do!)
Here is a suitable rewrite rule for this particular instance of this
phenomenon. We write it as a thereis loop$ rule rather than a
thereis$+, but they're the same.
(defthm example-of-constant-subterm-abstraction
(implies (warrant bbb)
(equal (loop$ for xxx on a
thereis
(if (equal (car xxx) (bbb bb)) xxx nil))
(let ((zzz (bbb bb)))
(loop$ for xxx on a
thereis
(if (equal (car xxx) zzz) xxx nil))))))
This illustrates another lesson. Remember that we're imagining a proof of
some conjecture that involves a thereis loop$ mentioning BBB
and wondering whether our rewrite rule loop$-can-be-member will hit it.
Had the thereis loop$ in the conjecture been written in the style
of the let expression above, where a variable is bound to (bbb bb)
and then that variable used in the loop$ body, we wouldn't need to move
the (bbb bb) out. Instead, the lambda generated by translating the
loop$ would contain a variable instead of (bbb bb). The name of
the let-bound variable outside the lambda is irrelevant since it
won't appear in the cleaned up lambda object where it is replaced by a
component of the global variables LOOP$-GVARS. In the containing
thereis$+ the value of that global variable will be (bbb bb), which
means the free variable b in our loop$-can-be-member rule can be
instantiated with (bbb bb) to allow the rule to match.
Put another way, by writing the loop$ in the inefficient
way (requiring (bbb bb) to be recomputed on every iteration) we
implicitly produce lambda object that is less general than one with the
(bbb bb) on the outside.
Keep unchanging subterms of loop$ bodies as variables and compute
their values outside of the lambda. Basically, try to write the most
general lambda objects you can.
Finally, these difficulties are exacerbated by the ease with which
loop$ statements can be written and the difference between their
appearance and the formal terms they denote. You might be more successful at
learning to use loop$s in lemmas and theorems if you simply don't use
loop$! Instead, learn to write the corresponding terms, e.g., try
writing a thereis$ or a thereis$+ term instead of a thereis
loop$ statement in your lemmas and theorems. Since the prover's output
contains such terms (rather than loop$ statements), it will be easier to
see where lemmas differ from the targets they were intended to hit. After
enough practice you can write loop$ statements with a better
appreciation of what they actually denote.
