		Search-engine friendly clone of the ACL2 documentation.

Fgl-correctness-of-binding-free-variables

Discussion of the logical justification for the bind-var feature.

FGL's bind-var feature can be used to bind a free variable in a rewrite rule to some arbitrary value. Here we discuss how the correctness of that feature may be formalized. Note we discuss this with respect to bind-var, but it applies to binder functions generally.

Requirements and Basic Idea

First we describe the requirements for using the bind-var feature. We must first have a rewrite rule containing a call of bind-var in either the RHS or a hyp. Then, if and when symbolic execution reaches the call of bind-var, it must be the case that the first argument of bind-var is a variable that is not yet bound in the current frame (this is checked in the interpreter). If this is the case, the interpreter may add a binding for that variable to any object; in particular, it interprets the second argument of bind-var under the trivial equivalence unequiv (meaning that the value returned is not important for soundness) and binds it to that value.

The justification for this is essentially that all free variables in a theorem are universally quantified. When we apply a rewrite rule, we start with the free variables of the LHS bound to the unifying substitution. We are free to bind any other variables that are mentioned in the theorem to whatever values we want, because the unifying substitution contains all variables of the LHS, so extending the unifying substitution to include additional variables won't change the value of the LHS under that substitution.

Technical Problem and Solutions

There is a technical problem with this when these free variables appear inside lambda bodies. ACL2 term translation ensures that all lambdas bind all the free variables of their bodies -- when it translates a lambda that has free variables in the body, it adds bindings for those variables to themselves. So if we have a rewrite rule like this:

(equal (foo x)
       (let* ((a (bar x))
              (c (bind-var b (baz x a))))
           ...))

then the outside of the RHS looks like this:

((lambda (a x b) ...)
 (bar x) x b)

We interpret the arguments of a lambda or function call before the body, and normally if we encounter an unbound variable during symbolic execution we produce an error. Therefore, we would run into an error when we process the argument b of the lambda call. To avoid this and get the intended behavior of binding b when we arrive at its bind-var form, we preprocess lambdas to remove bindings of variables to themselves, instead carrying forward the existing bindings from the outer context into the lambda body. (See ACL2 community book "centaur/meta/bindinglist.lisp" for the implementation.)

A further complication is that when we bind a free variable due to bind-var, it must be bound in the context of the current rewrite rule application, not just the current lambda body. To do otherwise would allow that variable to be bound to different objects in a single application of the rule. To deal with this, we effectively have two levels of variable bindings at any time: the major frame produced by the current rewrite rule application, which has a wholly new namespace for variables, and a minor frameproduced by each nesting of lambdas, which carries forward all variable bindings from the previous minor frame and may shadow variable bindings from the major frame. When we add a variable binding with bind-var, that binding goes into the bindings of the major frame.

Statement of Correctness

Finally we discuss how the bind-var feature affects how we state the correctness of the FGL symbolic interpreter.

The correctness of a typical rewriter that takes an alist of variable bindings is along the lines of:

(equivalent-under-relation equiv-relation-context
                           (eval-term input-term (eval-bindings bindings env))
                           (eval-term result-term env))

Here equiv-relation-context, input-term, and bindings are inputs to the rewriter, which produces result-term.

The exact such correctness statement for FGL involves various complications that we won't discuss here, such as the distinction between input ACL2 terms and output symbolic objects and various invariants of the interpreter state. The main complication that we will discuss is that, rather than just an input to the rewriter as would be the case in a typical rewriter, the relevant bindings are changed (extended) by the rewriter as it (potentially) adds variable bindings to the major frame due to bind-var. So the statement we want (again, very approximately) is:

(equivalent-under-relation
  equiv-relation-context
  (eval-term input-term (append (eval-bindings output-minor-bindings env)
                                (eval-bindings output-major-bindings env)))
  (eval-term result-term env))

(To simplify this slightly, we do show that the evaluation of the output and input minor bindings is equivalent.)

This is reasonable and true, but it isn't sufficiently strong to be inductively proved. The problem is that if we successively rewrite two terms, the output major bindings from the second term may be different from those from the first, so the inductive assumption from the first term doesn't help us anymore.

To fix this, we instead prove, approximately:

(forall ext
        (implies (eval-alist-extension-p
                   ext
                   (append (eval-bindings output-minor-bindings env)
                           (eval-bindings output-major-bindings env)))
                 (equivalent-under-relation equiv-relation-context
                                            (eval-term input-term ext)
                                            (eval-term result-term env))))

Where (eval-alist-extension-p a b) holds when a binds all keys present in b to the same values. Since the rewriter only adds pairs to the major bindings whose keys are not yet bound in either the major or minor bindings, the resulting appended, evaluated minor and major bindings is such an extension of the input appended, evaluated major and minor bindings. This allows the inductive assumption about the first term to be applied to the bindings resulting from rewriting the second term.