PSEUDO-TERMP

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 t

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.