:rewrite rule
Major Section: MISCELLANEOUS
Example: Consider the :REWRITE rule created fromThe(IMPLIES (SYNTAXP (NOT (AND (CONSP X) (EQ (CAR X) 'NORM)))) (EQUAL (LXD X) (LXD (NORM X)))).
syntaxp hypothesis in this rule will allow the rule to be
applied to (lxd (trn a b)) but will not allow it to be applied to
(lxd (norm a)).
General Form: (SYNTAXP test)may be used as the nth hypothesis in a
:rewrite rule whose
:corollary is (implies (and hyp1 ... hypn ... hypk) (equiv lhs rhs))
provided test is a term, test contains at least one variable, and
every variable occuring freely in test occurs freely in lhs or in
some hypi, i<n. Formally, syntaxp is a function of one argument;
syntaxp always returns t and so may be added as a vacuous
hypothesis. However, the test ``inside'' the syntaxp form is
actually treated as a meta-level proposition about the proposed
instantiation of the rule's variables and that proposition must
evaluate to true (non-nil) to ``establish'' the syntaxp hypothesis.
We illustrate this by slightly elaborating the example given above.
Consider a :rewrite rule whose :corollary is:
(IMPLIES (AND (RATIONALP X)
(SYNTAXP (NOT (AND (CONSP X) (EQ (CAR X) 'NORM)))))
(EQUAL (LXD X) (LXD (NORM X))))
How is this rule applied to (lxd (trn a b))? First, we form a
substitution that instantiates the left-hand side of the conclusion
of the rule so that it is identical to the target term. In the
present case, the substitution replaces x with (trn a b). Then we
backchain to establish the hypotheses, in order. Ordinarily this
means that we instantiate each hypothesis with our substitution and
then attempt to rewrite the resulting instance to true. Of course,
most users are aware of some exceptions to this general rule. For
example, if a hypothesis contains a ``free-variable'' -- one not
bound by the current substitution -- we attempt to extend the
substitution by searching for an instance of the hypothesis among
known truths. Forced hypotheses are another exception to the
general rule of how hypotheses are relieved. Hypotheses marked with
syntaxp, as in (syntaxp test), are also exceptions. Instead of
instantiating the hypothesis and trying to establish it, we evaluate
test in an environment in which its variable symbols are bound to
the quotations of the terms to which those variables are bound in
the instantiating substitution. In the case in point, we evaluate
the test
(NOT (AND (CONSP X) (EQ (CAR X) 'NORM)))in an environment where
x is bound to '(trn a b), i.e., the list
of length three whose car is the symbol 'trn. Thus, the test
returns t because x is a consp and its car is not the symbol 'norm.
When the syntaxp test evaluates to t, we consider the syntaxp
hypothesis to have been established; this is sound because
(syntaxp test) is t regardless of test. If the test
evaluates to nil (or fails to evaluate because of guard violations)
we act as though we cannot establish the hypothesis and abandon the
attempt to apply the rule; it is always sound to give up.
Note that the test of a syntaxp hypothesis does not deal with the
meaning or semantics or values of the terms but with their syntactic
forms. In the example above, the syntaxp hypothesis allows the rule
to be applied to every target of the form (lxd u), provided
(rationalp u) can be established and u is not of the form (norm v).
Observe that without this syntactic restriction the rule above could
loop producing a sequence of increasingly complex targets (lxd a),
(lxd (norm a)), (lxd (norm (norm a))), etc. An intuitive reading of
the rule might be ``norm the argument of lxd (when it is rationalp)
unless it has already been normed.''
Another common syntactic restriction is
(SYNTAXP (AND (CONSP X) (EQ (CAR X) 'QUOTE))).A rule with such a hypothesis can be applied only if
x is bound to
a specific constant. Thus, if x is 23 (which is actually
represented internally as (quote 23)), the test evaluates to t; but
if x is (+ 11 12) it evaluates to nil (because (car x) is the symbol
'+). It is often desirable to delay the application of a rule until
certain subterms are in some kind of normal form so that the
application doesn't produce excessive case splits.
