Major Section: ACL2-BUILT-INS
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-termps.
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.
