NU-REWRITER

rewriting NTH/UPDATE-NTH expressions 
Major Section:  MISCELLANEOUS

The rewriter contains special provisions for rewriting expressions composed of nth, update-nth, update-nth-array, together with let expressions and other applications of non-recursive functions or 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 s: 
(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 let expression 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 nth expression; in particular, it would expand the nested let expression to the large nested update-nth expression 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 move an nth into a let without expanding the let and how to simplify it if it nestles up against an update-nth.

There are four characteristics of this problem: the presence of nth, the presence of update-nth, the use of let to provide ``sequential'' updates, and the use of constant indices. Nth and 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 using set-nu-rewriter-mode.

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.