Major Section: MISCELLANEOUS

Example Forms: (pseudo-termp '(car (cons x 'nil))) ; has value t (pseudo-termp '(car x y z)) ; also has value t! (pseudo-termp '(delta (h x))) ; has value t (pseudo-termp '(delta (h x) . 7)) ; has value nil (not a true-listp) (pseudo-termp '((lambda (x) (car x)) b)) ; has value t (pseudo-termp '(if x y 123)) ; has value nil (123 is not quoted) (pseudo-termp '(if x y '123)) ; has value tIf

`x`

is the quotation of a term, then `(pseudo-termp x)`

is `t`

.
However, if `x`

is not the quotation of a term it is not necessarily
the case that `(pseudo-termp x)`

is `nil`

.
See term for a discussion of the various meanings of the word
``term'' in ACL2. In its most strict sense, a term is either a
legal variable symbol, a quoted constant, or the application of an
`n`

-ary function symbol or closed `lambda`

-expression to `n`

terms. By
``legal variable symbol'' we exclude constant symbols, such as `t`

,
`nil`

, and `*ts-rational*`

. By ``quoted constants'' we include `'t`

(aka
`(quote t)`

), `'nil`

, `'31`

, etc., and exclude constant names such as `t`

,
`nil`

and `*ts-rational*`

, unquoted constants such as `31`

or `1/2`

, and
ill-formed `quote`

expressions such as `(quote 3 4)`

. By ``closed
lambda expression'' we exclude expressions, such as
`(lambda (x) (cons x y))`

, containing free variables in their bodies.
Terms typed by the user are translated into strict terms for
internal use in ACL2.

The predicate `termp`

checks this strict sense of ``term'' with
respect to a given ACL2 logical world; See world. Many ACL2
functions, such as the rewriter, require certain of their arguments
to satisfy `termp`

. However, as of this writing, `termp`

is in `:`

`program`

mode and thus cannot be used effectively in conjectures to be
proved. Furthermore, if regarded simply from the perspective of an
effective guard for a term-processing function, `termp`

checks many
irrelevant things. (Does it really matter that the variable symbols
encountered never start and end with an asterisk?) For these
reasons, we have introduced the notion of a ``pseudo-term'' and
embodied it in the predicate `pseudo-termp`

, which is easier to
check, does not require the logical world as input, has `:`

`logic`

mode, and is often perfectly suitable as a guard on term-processing
functions.

A `pseudo-termp`

is either a symbol, a true list of length 2
beginning with the word `quote`

, the application of an `n`

-ary
pseudo-`lambda`

expression to a true list of `n`

pseudo-terms, or
the application of a symbol to a true list of `n`

`pseudo-termp`

s.
By an ```n`

-ary pseudo-`lambda`

expression'' we mean an expression
of the form `(lambda (v1 ... vn) pterm)`

, where the `vi`

are
symbols (but not necessarily distinct legal variable symbols) and
`pterm`

is a `pseudo-termp`

.

Metafunctions may use `pseudo-termp`

as a guard.