Binder-rules
Determining free variable bindings using rewriting
A binder rewrite rule can be created from a theorem with the following form:
(implies (and hypotheses
(rhs-equiv var rhs-form))
(equiv (binder-function var args)
var))
Here var cannot be used in hypotheses, args, or rhs-form, and
equiv and rhs-equiv are both equivalence relations.
Such a rule is used as follows. If the FGL rewriter encounters a form
(binder-function free-var actuals) where free-var is unbound, it first
rewrites the actuals, then may attempt to apply the rule as follows:
- Check that the current equivalence context allows rewriting under
equiv, or else abort the attempt.
- Unify args with the results of rewriting actuals to get the
initial set of variable bindings, or abort the attempt if they don't
unify.
- Push a new rewrite stack frame containing the initial bindings.
- Relieve hypotheses under the bindings exactly as with any other
rewrite rule, perhaps extending the variable bindings, or abort if relieving
any hypothesis fails.
- Rewrite rhs-form under the bindings in a rhs-equiv equivalence
context. The attempt succeeds unless this causes an abort or error.
- Pop the rewrite stack back to the outer context.
- Bind free-var to the result from rewriting rhs-form and replace
the binder-function call with that same result.
See also binder-functions.
