SYNTAXP

attach a heuristic filter on a rule 
Major Section:  MISCELLANEOUS

A calls of syntaxp in the hypothesis of a :rewrite, :definition, or :linear rule is treated specially, as described below. Similar treatment is given to the evaluation of a :meta rule's hypothesis function call.

For example, consider the :rewrite rule created from the following formula. 

Example:
(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)).

Some Related Topics

General Form:
(SYNTAXP test)
Syntaxp always returns t and so may be added as a vacuous hypothesis. However, when relieving the hypothesis, 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.

Note that the test of a syntaxp hypothesis does not, in general, deal with the meaning or semantics or values of the terms, but rather 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 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 unless it has already been normed.''

Note also that a syntaxp hypothesis deals with the syntactic form used internally by ACL2, rather than that seen by the user. In some cases these are the same, but there can be subtle differences with which the writer of a syntaxp hypothesis must be aware. You can use :trans to display this internal representation.

There are two types of syntaxp hypotheses. The simpler type may be a hypothesis of a :rewrite, :definition, or :linear rule provided test contains at least one variable but no free variables (see free-variables). In particular, test may not use stobjs; any stobj name will be treated as an ordinary variable. The case of :meta rules is similar to the above, except that it applies to the result of applying the hypothesis metafunction. (Later below we will describe the second type, an extended syntaxp hypothesis, which may use state.)

We illustrate the use of simple syntaxp hypotheses by slightly elaborating the example given above. Consider a :rewrite rule: 

(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). 
(LXD X) ==> (LXD (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. Thus, in order to relieve the first hypothesis above, we rewrite 
(RATIONALP (trn a b)).
If this rewrites to true, we continue.

Of course, many users are aware of some exceptions to this general description of the way we relieve hypotheses. 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. See free-variables. 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. We instantiate such a hypothesis; but instead of rewriting the instantiated instance, we evaluate the instantiated test. More precisely, 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. So in the case in point, we (in essence) evaluate 

(NOT (AND (CONSP '(trn a b)) (EQ (CAR '(trn a b)) 'NORM))).
This clearly evaluates to t. When a syntaxp test evaluates to true, we consider the syntaxp hypothesis to have been established; this is sound because logically (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.

The acute reader will have noticed something odd about the form 

(NOT (AND (CONSP '(trn a b)) (EQ (CAR '(trn a b)) 'NORM))).
When relieving the first hypothesis, (RATIONALP X), we substituted (trn a b) for X; but when relieving the second hypothesis, (SYNTAXP (NOT (AND (CONSP X) (EQ (CAR X) 'NORM)))), we substituted the quotation of (trn a b) for X. Why the difference? Remember that in the first hypothesis we are talking about the value of (trn a b) -- is it rational -- while in the second one we are talking about its syntactic form. Remember also that Lisp, and hence ACL2, evaluates the arguments to a function before applying the function to the resulting values. Thus, we are asking ``Is the list (trn a b) a consp and if so, is its car the symbol NORM?'' The quotes on both (trn a b) and NORM are therefore necessary. One can verify this by defining trn to be, say cons, and then evaluating forms such as 
(AND (CONSP '(trn a b)) (EQ (CAR '(trn a b)) 'NORM))
(AND (CONSP (trn a b)) (EQ (CAR (trn a b)) NORM))
(AND (CONSP (trn 'a 'b)) (EQ (CAR (trn 'a 'b)) NORM))
(AND (CONSP '(trn a b)) (EQ '(CAR (trn a b)) ''NORM))
at the top-level ACL2 prompt.

See syntaxp-examples for more examples of the use of syntaxp.

An extended syntaxp hypothesis is similar to the simple type described above, but it uses two additional variables, mfc and state, which must not be bound by the left hand side or an earlier hypothesis of the rule. They must be the last two variables mentioned by form; first mfc, then state. These two variables give access to the functions mfc-xxx; see extended-metafunctions. As described there, mfc is bound to the so-called metafunction-context and state to ACL2's state. See syntaxp-examples for an example of the use of these extended syntaxp hypotheses.

We conclude with an example illustrating an error that may occur if you forget that a syntaxp hypothesis will be evaluated in an environment where variables are bound to syntactic terms, not to values. Consider the following stobj introduction (see defstobj). 

  (defstobj st
    (fld1 :type (signed-byte 3) :initially 0)
    fld2)
The following syntaxp hypothesis is ill-formed for evaluation. Indeed, ACL2 causes an error because it anticipates that when trying to relieve the syntaxp hypothesis of this rule, ACL2 would be evaluating (fld1 st) where st is bound to a term, not to an actual stobj as required by the function fld1. The error message is intended to explain this problem. 
  ACL2 !>(defthm bad
           (implies (syntaxp (quotep (fld1 st)))
                    (equal (stp st)
                           (and (true-listp st)
                                (equal (len st) 2)
                                (fld1p (car st))))))


  ACL2 Error in ( DEFTHM BAD ...):  The form (QUOTEP (FLD1 ST)), from
  a SYNTAXP hypothesis, is not suitable for evaluation in an environment
  where its variables are bound to terms.  See :DOC SYNTAXP.  Here is
  further explanation:
       The form ST is being used, as an argument to a call of FLD1, where
  the single-threaded object of that name is required.  But in the current
  context, the only declared stobj name is STATE.  Note:  this error
  occurred in the context (FLD1 ST).


  Summary
  Form:  ( DEFTHM BAD ...)
  Rules: NIL
  Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)

  ACL2 Error in ( DEFTHM BAD ...):  See :DOC failure.

  ******** FAILED ********
  ACL2 !>
Presumably the intention was to rewrite the term (stp st) when the fld1 component of st is seen to be an explicit constant. As explained elsewhere (see free-variables), we can obtain the result of rewriting (fld1 st) by binding a fresh variable to that term using EQUAL, as follows. 
  (defthm good
    (implies (and (equal f (fld1 st))
                  (syntaxp (quotep f)))
             (equal (stp st)
                    (and (true-listp st)
                         (equal (len st) 2)
                         (fld1p (car st))))))
The event above is admitted by ACL2. We can see it in action by disabling the definition of stp so that only the rule above, good, is available for reasoning about stp. 
  (in-theory (disable stp))
Then the proof fails for the following, because the syntaxp hypothesis of the rule, good, fails: (quotep f) evaluates to nil when f is bound to the term (fld1 st). 
  (thm (stp st))
However, the proof succeeds for the next form, as we explain below. 
  (thm (stp (list 3 rest)))
Consider what happens in that case when rule good is applied to the term (stp (list 3 rest)). (See free-variables for relevant background.) The first hypothesis of good binds the variable f to the result of rewriting (fld1 st), where st is bound to the (internal form of) the term (list 3 rest) -- and that result is clearly the term, '3. Then the syntaxp hypothesis is successfully relieved, because the evaluation of (quotep f) returns t in the environment that binds f to '3.