to attach a heuristic filter on a :rewrite rule

Consider the :REWRITE rule created from


The 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:

              (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
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

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.