Random-remarks-on-rewriting
Some basic facts about the ACL2 rewriter
The ACL2 rewriter is technically part of the simplifier, but in
this documentation we often conflate the two and say things like ``the
conclusion simplifies to T'' when in fact we should say ``the conclusion
rewrites to T during simplification'' In addition, both the simplifier
and the rewriter are enormously complicated and contain so many heuristics
that users are not often helped by studying the details. For example, the
rewriter takes 18 arguments (some of which are bundles of more rarely used
arguments) and is part of a mutually recursive clique containing 50 functions
as of Version 8.3, including the linear (and non-linear) arithmetic
semi-decision procedures. The rewriter and its clique consume about 6500
lines of code.
But to understand how :rewrite, :rewrite-quoted-constant, :linear, :congruence,
:forward-chaining and other rules behave, the user has to have a
fairly weak model of the simplifier and rewriter, so we sketch that here.
In ACL2, the goals you see printed in proof output are represented
internally as clauses. See clause.
The job of the simplifier is to simplify a clause, returning a set of
clauses whose conjunction is propositionally equivalent to the input clause.
The most desirable output set is the empty set, because the conjunction over
the empty set is T, which means the goal clause was proved. For related
discussions, see hints-and-the-waterfall, where we discuss how
repeated simplifications are performed.
Note that if you are trying to simplify the clause (lit1 lit2
... litk) and you manage to rewrite, say, the liti to T, then the
clause is true. Furthermore, when rewriting a literal of a clause you may
assume all the other literals false because if one were true the clause would
be true. Finally, when you rewrite a literal you are justified in replacing
it with one that is propositional equivalent, since the literals are
disjoined.
The simplifier works by first generating several data structures, here
called the ``context,'' which codify governing assumptions available for the
rewriting of each literal. These data structures include the type-alist and linear-arithmetic data base. They are built using
various rules derived from previously proved lemmas, including :type-prescription, :forward-chaining, and :linear
rules. It then calls the rewriter successively on each literal passing it
the appropriate context and stipulating that the result of the rewriting must
be propositionally equivalent to the input. The rewriter returns a suitable
term. If the result is the unchanged, the simplifier just moves on to the
next literal. If the result contains no IF-expressions, the simplifier
just replaces the old literal with the new one. But if the new term contains
IF-expressions, the simplifier splits them out into a set of clause
segments, i.e., if the literal simplifies to (IF a b c), then the
simplifier gets two new clause segments, ((NOT a) b) and (a c), and
then it splices each segment into the goal clause where the literal was,
producing a set of new clauses, and then resumes rewriting literals in each
new clause. Heuristics try to prevent excessive case splitting, e.g., see
case-split-limitations.
The job of the rewriter is to take a term, some context, and an
equivalence relation, and return a ``simpler'' term that is equivalent to the
input term under the assumptions in the context.
The rewriter works by exploring the term, possibly changing the context
and the equivalence relation as appropriate for the subterms it rewrites.
- If the term is a variable, the rewriter just returns it (unless the
context tells it something interesting about that variable, such as that the
variable is equal to nil). Sometimes you might wish that the value of a
bound variable be rewritten, usually because the value found on the alist was
rewritten under a different equivalence relation than the variable is now
being used. See double-rewrite.
- If the term is a quoted constant, the rewriter tries to apply
:rewrite-quoted-constant rules to that constant.
- If the term is (IF a b c), it rewrites the test, a, under the
equivalence relation IFF to get some (possibly) new term, a'. If
a' is nil or is obviously different from nil (like T),
the rewriter replaces the IF-term by b or c, appropriately,
and rewrites that. If on the other hand, the rewriter can't decide whether
a' is nil or not, it rewrites b to b' in an extended
context in which a' is assumed non-nil and rewrites c to
c' in an extended context in which a' is nil. In rewriting
both branches it preserves the outer equivalence relation -- the one to be
maintained while rewriting the IF-term. Then the rewriter returns
(IF a' b' c').
- If the term is a call of an arithmetic inequality, like (< a b), the
rewriter rewrites a and b and then considers whether the context
allows it deduce the truth or falsity of the inequality using a linear-arithmetic decision procedure. The decision procedure, which is
complete for linear inequalities over the rationals, uses heuristics to
decide many integer cases, to select the order in which inequalities are
combined to eliminate variables, and to handle some non-linear-arithmetic problems.
- If the term is a call of a function symbol, fn, on some argument
terms, a1, ..., an, the rewriter rewrites each argument, ai to
ai'. For each argument the rewriter uses known :congruence
rules to determine which equivalence relations can be used to rewrite terms
in that argument position so as to maintain the outer equivalence. Then,
having transformed (fn a1 ... an) to (fn a1' ... an') the rewriter
tries to apply :rewrite rules to that transformed term, called
the ``target.''.
- Among the rewrite rules generally available for (fn a1' ... an') is
the definition of fn itself. The rewriter considers ``expanding'' the
call, i.e., replacing it by the body of fn after substituting the
ai' for the formal variables, if the definition is enabled, and
then rewriting that. But heuristics are used to prevent the indefinite
expansion of recursive definitions.
For an elementary tutorial on the application of a :rewrite rule
to a target term, see introduction-to-rewrite-rules-part-1 and introduction-to-rewrite-rules-part-2. Those topics also lead to
documentation on how to design effective rules. But just to summarize very
briefly, we offer the following.
:Rewrite rules take the general form
(implies (and hyp1 ... hypk) (equiv lhs rhs))
where equiv is a known equivalence relation. Recall that the
rewriter has a target term to rewrite in some context and is required to
return a term that is equivalent modulo a given equivalence relation, here
called the ``outer'' equivalence. Furthermore, if the target term is a
function application, e.g., (fn a1' ... an'), the argument subterms have
already been rewritten.
If the rule in question is enabled and its equiv refines the outer
equivalence, the rewriter tries to match lhs with the target. By
``match'' we mean it tries to find a substitution for the variables in
lhs that make the instantiated lhs identical to the target. We
discuss matching further below. Second, having found a suitable
substitution, tries to ``relieve'' the hypotheses, as discussed below. If
successful, that means each hypi, when instantiated with the
substitution, is non-nil. Third, if all the hypotheses are relieved,
the target is ``replaced'' by the result of rewriting rhs under the
substitution. We discuss that step more below too.
Matching: Technically, ACL2 uses a restriction of ordinary
first-order unification -- the restriction being that only variables in the
pattern (here the lhs of the rule) may be instantiated. Thus, the
pattern (G x (H x)) matches (G (M A B) (H (M A B))) by binding
x to (M A B). It does not match (G (M A B) (H (M A A))) even
though those two terms ``unify'' by binding x to (M A A) and B
to A. Our pattern matcher is the function one-way-unify in our
source code.
However, our pattern matcher knows some things about the structure of
quoted constants. For example, the pattern (CONS x y) matches the
quoted constant '(A B C), by binding x to 'A and y to
'(B C). This can be seen by running one-way-unify on those two
terms:
ACL2 !>(one-way-unify '(cons x y) ''(A B C))
(T ((Y QUOTE (B C)) (X QUOTE A)))
Note the quote marks in our input. Since one-way-unify expects both
of its arguments to be fully translated formal terms, we have to quote every
constant we write here. And since the arguments to one-way-unify are
evaluated before the function is called, we have to quote the two terms. We
see that one-way-unify returns two results. The first is T,
meaning that a suitable substitution was found. The second is the
substitution. Lisp's abbreviation convention for printed ``dotted pairs,''
its ``quote convention,'' its convention of reading symbols in uppercase, and
our convention here of writing terms (and variables) in lower case but
constants in upper case, all conspire to make the substitution a little hard
to read for novices. Another way to display the exact same substitution
is:
((y . '(B C)) (x . 'A))
i.e., x is bound to 'A and y is bound to (B C).
Below are some other examples, but we've re-displayed the substitutions.
ACL2 !>(one-way-unify '(coerce x 'string) ''"Hello!")
(T ((x . (#H #e #l #l #o #!))))
ACL2 !>(one-way-unify '(intern-in-package-of-symbol x y) ''ACL2::TEMP)
(T ((y . 'TEMP) (x . '"TEMP")))
ACL2 !>(one-way-unify '(binary-+ '3 x) ''7)
(T ((X . '4)))
ACL2 !>(one-way-unify '(unary-- x) ''-7)
(T ((X QUOTE 7)))
ACL2 !>(one-way-unify '(unary-- x) ''7)
(NIL NIL)
ACL2 !>(one-way-unify '(binary-* '2 y) ''8)
(T ((Y QUOTE 4)))
ACL2 !>(one-way-unify '(binary-* x y) ''8)
(NIL NIL)
Note that the pattern matching algorithm is incomplete on quoted
constants! For example, it fails to match (unary-- x) with '7 even
though (unary-- '-7) is '7. It similarly fails to match
(binary-* x y) with '8 even though (binary-* '33 '8/33) is
8; indeed, there are in infinite number of suitable substitutions for
this case, but one-way-unify is designed to return at most one so as to
limit the applicability of rewrite rules to ``reasonable'' cases.
Relieving the Hypotheses: The hypotheses of a rewrite rule are
relieved one at a time starting with the left-most one. The basic strategy
is just to rewrite each hypothesis, assuming the current context and if
IFF equivalence relation. If the result comes back non-NIL the
hypothesis is equivalent to T in the current context. But there are
various special considerations.
- Free variables: It is possible that a hypothesis contains variables that
are not bound by the substitution generated by the match. We call these
``free variables'' and the system tries to bind them to make the instantiated
hypothesis appear among the contextual assumptions. New bindings are
accumulated as hypotheses are relieved. It is possible to find multiple
successful substitutions, some possibly filtered out by subsequent
hypotheses. See free-variables and the documentation topics it
cites.
- Pragmas: It is possible to mark a hypothesis so that it is temporarily
assumed true so that the rewrite rule can be applied. This essentially
spawns another subgoal to prove the hypothesis and thus brings the full power
of the prover (not just the rewriter) to bear on the hypothesis. See force and case-split. It is also possible to include hypotheses
that are logically always true but which cause the attempt to apply the rule
to fail if a certain user-specified computation so indicates. This can be
used to restrict the application of a rule to certain syntactic situations.
See syntaxp.
Replacement: Before the target is replaced by the rewritten
rhs, a heuristic check is made to prevent certain trivial forms of
rewrite loops. See loop-stopper. Otherwise, if the hypotheses are
relieved (or assumed), the rewriter rewrites rhs under the substitution
generated by the match and the hypotheses. It then makes certain heuristic
checks to decide if replacing the target by this new term is a ``good idea''
in the opinion of the ACL2 implementors. The two main checks are designed to
avoid runaway expansion of recursive functions (see definition), and
introducing ``too many ifs'' (see too-many-ifs. The latter
check is used to prevent unmanageable case explosions. (In general, the
number of cases rises exponentially with the number of IFs.)
