## SYNTAXP

to attach a heuristic filter on a `:``rewrite` rule
```Major Section:  MISCELLANEOUS
```

```Example:
Consider the :REWRITE rule created from

(IMPLIES (SYNTAXP (NOT (AND (CONSP X) (EQ (CAR X) 'NORM))))
(EQUAL (LXD X) (LXD (NORM X)))).
```
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:

```(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. `Force`d 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 `norm`ed.''

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.