		Search-engine friendly clone of the ACL2 documentation.

Fgl-rewrite-rules

Binder-functions

Functions that describe constraints on bindings for free variables.

A binder function doesn't have a particular form (other than having at least one argument), but it is one intended to be used with FGL free variable binding constructs such as binder-rules.

A binder function essentially places some logical restrictions on what may be bound to a particular free variable, so that these restrictions may be used in proving the theorem where the binder function. After the theorem is proved, when it is used in rewriting, binder-rules can be used to provide bindings for the variables such that the restrictions are satisfied.

The most trivial example is bind-var, which is defined to simply return its first argument:

(define bind-var (ans form)
  ans)

Because bind-var returns its first argument unchanged no matter what, this places no restrictions on what it returns: it can be made to return any object, just by setting its first argument to that object. Therefore we can create any binder rule we like. E.g., the following rule says that if the second argument to the bind-var form is (foo x), its free variable argument should be bound to (+ 1 x):

(fgl::def-fgl-brewrite bind-var-of-foo
  (implies (equal free-var (+ 1 x))
           (equal (bind-var free-var (foo x))
                  free-var)))

When interpreted as a binder rule, this has no hypotheses (so it can apply whenever bind-var is called on a free variable and an argument that unifies with (foo x)), and it rewrites to (+ 1 x), meaning when it is applied, that free variable will be bound to the object resulting from rewriting (+ 1 x) and this same object will be returned from the bind-var form.

A slightly less simple example: check-equal is a binder function that is Boolean-valued and may only return T if its second and third arguments are equal:

(define check-equal (ans x y)
  (and (equal x y)
       ans
       t))

FGL has a binder meta rule implementing this, which returns T if the two objects are syntactically equal. But another way to get a similar effect would be with this binder rewrite rule:

(fgl::def-fgl-brewrite check-equal-brewrite
  (implies (and (equal x y)
                (equal ans t))
           (equal (check-equal ans x y) ans)))

This rule says that if the hypothesis (equal x y) is satisfied, then the free variable should be bound to t and t returned from the check-equal call.

A non-trivial example: common-suffix-binder must always return something that is a common suffix of its second and third arguments, or else nil:

(define common-suffix-binder (res list1 list2)
  (and (suffixp res list1)
       (suffixp res list2)
       res))

If this binder is used in a theorem, then when proving that theorem, it is known that the return value of the common-suffix-binder call is either a suffix of both lists or NIL.

When applying a rewrite rule that contains a call of common-suffix-binder whose first argument is a free variable, FGL needs to find an object that satisfies that condition; if it can do so, it will bind that object to the free variable and return it from the call of common-suffix-binder. There might be several strategies that could find an object that would satisfy the needed conditions. Here is one example: this pair of binder rewrite rules finds such a suffix for two CONS nest terms if they are the same length and have a syntactically equal common suffix:

(fgl::def-fgl-brewrite find-common-suffix-when-equal
  (implies (and (equal list1 list2)
                (equal res list1))
           (equal (common-suffix-binder res list1 list2) res)))

(fgl::def-fgl-brewrite find-common-suffix-when-not-equal
  (implies (and (not (and (check-equal car-eq a1 a2)
                          (check-equal cdr-eq d1 d2)))
                (equal res (common-suffix-binder res2 d1 d2)))
           (equal (common-suffix-binder res (cons a1 d1) (cons a2 d2)) res)))

The first rule says that if the two lists are provably equal, then the first list should be bound to the free variable and returned from the common-suffix-binder form. The second rule applies when the two terms are both CONS calls, and their arguments are pairwise not provably equal (so that the first rule can apply in the case where they are). In this case, it says to continue the search by looking for a common suffix of the two cdr arguments d1 and d2.