		Search-engine friendly clone of the ACL2 documentation.

Lambda-opt

A method to optimize lambda expression before RP-Rewriter attempts to rewrite them.

RP-Rewriter does not internally work with terms that has lambda expressions. Every term (conjecture and rules) that is passed to the rewriter will be beta reduced. However, in some cases, doing beta-reduction will cause repetitive rewriting and this may result in significant proof-time and memory issues.

To mitigate this issue, we use a lambda optimization mechanism when adding rules to the RP-rewriter's ruleset with add-rp-rule and proving conjectures with defthmrp. This mechanism is intended to imitate the structure of lambda expressions to prevent repetitive rewriting. For every level of lambda expression, we create a non-executable function so that values of the lambda expressions are rewritten first, then they are bound to the variables, and those variables are applied to the term. For example, add-rp-rule with lambda-opt enabled will produce these events for the given rule:


(defthm foo-redef
  (implies (p x)
           (equal (foo x)
                  (let* ((a (f1 x))
                         (b (f2 x)))
                    (f4 a a b)))))

(add-rp-rule foo-redef
             :lambda-opt t)

;; The above event is translated into this:
(encapsulate
  (((foo-redef_lambda-fnc_1 * *) => *)
   ((foo-redef_lambda-fnc_0 * *) => *))
  (local (defun-nx foo-redef_lambda-fnc_1 (b a)
           (f4 a a b)))
  (disable-exc-counterpart foo-redef_lambda-fnc_1)
  (local (add-rp-rule foo-redef_lambda-fnc_1))
  (local (defun-nx foo-redef_lambda-fnc_0 (a x)
           (foo-redef_lambda-fnc_1 (f2 x) a)))
  (disable-exc-counterpart foo-redef_lambda-fnc_0)
  (local (add-rp-rule foo-redef_lambda-fnc_0))
  (def-rp-rule
    foo-redef-for-rp-openers
    (and (equal (foo-redef_lambda-fnc_1 b a)
                (f4 a a b))
         (equal (foo-redef_lambda-fnc_0 a x)
                (foo-redef_lambda-fnc_1 (f2 x) a)))
    :disabled-for-acl2 t
    ...)
  (defthmd
    foo-redef-for-rp
    (and (implies (p x)
                  (equal (foo x)
                         (foo-redef_lambda-fnc_0 (f1 x) x))))
    :hints ...)
  ... <some-table-events> ...)

Here, add-rp-rule will generate another lemma called foo-redef-for-rp that is aimed to be used by RP-Rewriter in lieu of the original foo-redef rule. The right hand side of the original rule first binds a to (f1 x). After applying foo-redef-for-rp, the rewriter will first work on the (f1 x) term, then it will rewrite foo-redef_lambda-fnc_0 and bind a to rewritten (f1 x) which will mimic the behavior of the original lambda expression. Then, the program binds b to (f2 x) through foo-redef_lambda-fnc_1, and then finally get the result. This way, the repeated (had it been beta reduced) term (f1 x) is rewritten only once.

Users will chiefly observe this lambda optimization behavior when using def-rp-rule, add-rp-rule, and defthmrp. Def-rp-rule simply proves a given lemma using ACL2 and given hints, and then calls add-rp-rule to register the proved lemma with RP-Rewriter possibly with this lambda optimization. Add-rp-rule and defthmrp themselves implement their versions of the lambda optimization. Add-rp-rule parses the term of a given rule's formula and beta reduces left-hand-side (lhs) while retaining the lambda form of the hyps and right-hand-side (rhs). It pre-processes the term to push in the lambda expressions in order to extract the terms for rhs and hyp. When its :lambda-opt argument is set to :max, it tries to look for repeated terms in hyp and rhs separately that are not already bound in lambda expressions for further optimizations. On the other hand, defthmrp does not try to isolate rhs, hyp, and lhs during the optimization process and it works on the term as a whole. However, whatever lambda optimization defthmrp does and whatever events it creates in the process, they are made locally inside an encapsulate and it is only for the sake of RP-Rewriter at the time of its simplification of the given conjecture. Defthmrp still calls add-rp-rule when saving the lemma as a rewrite rule for it to use later.