Pseudo-termp
A predicate for recognizing term-like s-expressions
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 t
If 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, 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?) We have therefore 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, 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.
Subtopics
- Pseudo-term-fty
- Overview of FTY support for pseudo-terms.
- Std/typed-lists/pseudo-term-listp
- Lemmas about lists of pseudo-termps, available in the std/typed-lists library.
