`:`

`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. `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.