Major Section: MISCELLANEOUS
The rewriter contains special provisions for rewriting expressions
let expressions and other applications of non-recursive
lambda expressions. For details see the paper
``Rewriting for Symbolic Execution of State Machine Models'' by J
Strother Moore. Also see set-nu-rewriter-mode.
The ``nu-rewriter'' is a recent addition to the main rewrite engine in ACL2. Consider the expression
(let ((s (update-nth 1 (new-a x s) s))) (let ((s (update-nth 2 (new-b x s) s))) (let ((s (update-nth 3 (new-c x s) s))) s)))If the
lets in this expression are expanded, a very large expression results because of the duplicate occurrences of
(update-nth 3 (new-c x (update-nth 2 (new-b x (update-nth 1 (new-a x s) s)) (update-nth 1 (new-a x s) s))) (update-nth 2 (new-b x (update-nth 1 (new-a x s) s)) (update-nth 1 (new-a x s) s))).This expansion of the
letexpression can be very expensive in space and time. In particular, the
(new-a x s)expression might be rewritten many times.
Now imagine asking what 2nd component of the structure is. That is, consider
(nth 2 (let ((s (update-nth 1 (new-a x s) s))) (let ((s (update-nth 2 (new-b x s) s))) (let ((s (update-nth 3 (new-c x s) s))) s))))The normal ACL2 rewrite engine would answer this question by first rewriting the arguments to the
nthexpression; in particular, it would expand the nested
letexpression to the large nested
update-nthexpression and then, using rules such as
(defthm nth-update-nth (equal (nth m (update-nth n val l)) (if (equal (nfix m) (nfix n)) val (nth m l))))would reduce the expression to
(new-b x (update-nth 1 (new-a x s) s)).
The purpose of the nu-rewriter is to allow simplifications like this
without first expanding the
lets. The ``nu'' in the name is an
acronym for ``
nth/update-nth''. The nu-rewriter knows how to
nth into a
let without expanding the
let and how
to simplify it if it nestles up against an
There are four characteristics of this problem: the presence of
nth, the presence of
update-nth, the use of
provide ``sequential'' updates, and the use of constant indices.
update-nth need not occur explicitly; they may be
used inside of definitions of ``wrapper'' functions.
Because the nu-rewriter changes the order in which things are rewritten,
its routine use can make ACL2 unable to reproduce old proofs. It is
therefore switched off by default. If your application exhibits the
characteristics above, you might wish to switch the nu-rewriter on
More will eventually be written about the nu-rewriter. However, it is described in detail in the paper cited at the beginning of this documentation topic.