Term
The three senses of well-formed ACL2 expressions or formulas
Also see untranslate for a relevant utility (and a more
abbreviated explanation of terms).
Examples of Terms:
(cond ((caar x) (cons t x)) (t 0)) ; an untranslated term
(if (car (car x)) (cons 't x) '0) ; a translated term
(car (cons x y) 'nil v) ; a pseudo-term
In traditional first-order predicate calculus a ``term'' is a syntactic
entity denoting some object in the universe of individuals. Often, for
example, the syntactic characterization of a term is that it is either a
variable symbol or the application of a function symbol to the appropriate
number of argument terms. Traditionally, ``atomic formulas'' are built from
terms with predicate symbols such as ``equal'' and ``member;'' ``formulas''
are then built from atomic formulas with propositional ``operators'' like
``not,'' ``and,'' and ``implies.'' Theorems are formulas. Theorems are
``valid'' in the sense that the value of a theorem is true, in any model of
the axioms and under all possible assignments of individuals to variables.
However, in ACL2, terms are used in place of both atomic formulas and
formulas. ACL2 does not have predicate symbols or propositional operators as
distinguished syntactic entities. The ACL2 universe of individuals includes a
``true'' object (denoted by t) and a ``false'' object (denoted by
nil), predicates and propositional operators are functions that return
these objects. Theorems in ACL2 are terms and the ``validity'' of a term
means that, under no assignment to the variables does the term evaluate to
nil.
We use the word ``term'' in ACL2 in three distinct senses. We will speak
of ``translated'' terms, ``untranslated'' terms, and ``pseudo-'' terms.
Translated Terms: The Strict Sense and Internal Form
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 a true list of n terms.
The legal variable symbols are symbols other than t or nil which
are not in the keyword package, do not start with ampersand, do not start and
end with asterisks, and if in the main Lisp package, do not violate an
appropriate restriction (see name).
Quoted constants are expressions of the form (quote x), where x
is any ACL2 object. Such expressions may also be written 'x.
Closed lambda expressions are expressions of the form (lambda (v1
... vn) body) where the vi are distinct legal variable symbols,
body is a term, and the only free variables in body are among the
vi.
The function termp, which takes two arguments, an alleged term x
and a logical world w (see world), recognizes terms of a given
extension of the logic. Termp is defined in :program mode.
Its definition may be inspected with :pe termp for a
complete specification of what we mean by ``term'' in the most strict sense.
Most ACL2 term-processing functions deal with terms in this strict sense and
use termp as a guard. That is, the ``internal form'' of a term
satisfies termp, the strict sense of the word ``term.''
Untranslated Terms: What the User Types
While terms in the strict sense are easy to explore (because their
structure is so regular and simple) they can be cumbersome to type. Thus,
ACL2 supports a more sugary syntax that includes uses of macros and constant
symbols. Very roughly speaking, macros are functions that produce terms as
their results. Constants are symbols that are associated with quoted objects.
Terms in this sugary syntax are ``translated'' to terms in the strict sense;
the sugary syntax is more often called ``untranslated.'' Roughly speaking,
translation just implements macroexpansion, the replacement of constant
symbols by their quoted values, and the checking of all the rules governing
the strict sense of ``term.''
More precisely, macro symbols are as described in the documentation for
defmacro. A macro, mac, can be thought of as a function,
mac-fn, from ACL2 objects to an ACL2 object to be treated as an
untranslated term. For example, caar is defined as a macro symbol;
the associated macro function maps the object x into the object (car
(car x)). A macro form is a ``call'' of a macro symbol, i.e., a list whose
car is the macro symbol and whose cdr is an arbitrary true
list of objects, used as a term. Macroexpansion is the process of replacing
in an untranslated term every occurrence of a macro form by the result of
applying the macro function to the appropriate arguments. The ``appropriate''
arguments are determined by the exact form of the definition of the macro;
macros support positional, keyword, optional and other kinds of arguments.
See defmacro.
In addition to macroexpansion and constant symbol dereferencing,
translation implements the mapping of let and let* forms into
applications of lambda expressions and closes lambda expressions
containing free variables. Thus, the translation of
(let ((x (1+ i))) (cons x k))
can be seen as a two-step process that first produces
((lambda (x) (cons x k)) (1+ i))
and then
((lambda (x k) (cons x k)) (1+ i) k) .
Observe that the body of the let and of the first lambda
expression contains a free k which is finally bound and passed into the
second lambda expression.
Translation also maps flet forms into applications of lambda
expressions. See flet.
When we say, of an event-level function such as defun or defthm, that some argument ``must be a term'' we mean an untranslated term.
The event functions translate their term-like arguments.
To better understand the mapping between untranslated terms and translated
terms it is convenient to use the keyword command :trans to see
examples of translations. See trans and also see trans1.
Finally, we note that the theorem prover prints terms in untranslated form.
But there can be more than one correct untranslated term corresponding to a
given translated term. For example, the translated term (if x y 'nil)
can be untranslated as (if x y nil) and can also be untranslated as
(and x y). The theorem prover attempts to print an untranslated term
that is as helpful to the user as possible. In particular, consider a term of
the form (nth k st) where st is a single-threaded object (see stobj) and the kth accessor of st is, say, kn. The theorem
prover typically would expand (kn st) to (nth k st). If k is
large then it could be difficult for the user to make sense out of a proof
transcript that mentions the expanded term. Fortunately, the untranslation of
(nth k st) would be (nth *kn* st); here *kn* would be a
constant (see defconst) added by the defstobj event introducing
st, defined to have value k. The user can extend this user-friendly
style of printing applications of nth to stobjs; see add-nth-alias. These remarks about printing applications of function nth extend naturally to function update-nth. Moreover, the prover
will attempt to treat terms as stobjs for the above purpose when
appropriate. For example, if function foo has signature ((foo
* st) => (mv * * * st)), where st is introduced with (defstobj st f0
f1), then the term (nth '1 (mv-nth '3 (foo x st0))) will be
printed as (nth *f1* (mv-nth 3 (foo x st0))).
Pseudo-Terms: A Common Guard for Metafunctions
Because termp is defined in :program mode, it cannot be
used effectively in conjectures to be proved. Furthermore, from the
perspective of merely guarding a term processing function, termp often
checks more than is required. Finally, because termp requires the
logical world as one of its arguments it is impossible to use
termp as a guard in places where the logical world is not
itself one of the arguments.
For these reasons we support the idea of ``pseudo-terms.'' A pseudo-term
is either a symbol (but not necessarily one having the syntax of a legal
variable symbol), a true list of length 2 beginning with quote, or the
``application of'' a symbol or pseudo lambda expression to a true list of
pseudo-terms. A pseudo lambda expression is an expression of the form
(lambda (v1 ... vn) body) where the vi are all symbols and body
is a pseudo-term.
Pseudo-terms are recognized by the unary function pseudo-termp. If
(termp x w) is true, then (pseudo-termp x) is true. However, if
x fails to be a (strict) term it may nevertheless still be a pseudo-term.
For example, (car a b) is not a term, because car is applied to
the wrong number of arguments, but it is a pseudo-term.
The structures recognized by pseudo-termp can be recursively
explored with the same simplicity that terms can be. In particular, if x
is not a variablep or an fquotep, then (ffn-symb x) is the
function (symbol or lambda expression) and (fargs x) is the
list of argument pseudo-terms. A metafunction (see meta) or
clause-processor (see clause-processor) may use pseudo-termp as
the guard.
Subtopics
- Lambda
- Lambda expressions, LAMBDA objects, and lambda$ expressions
- Pseudo-termp
- A predicate for recognizing term-like s-expressions
- Term-order
- The ordering relation on terms used by ACL2
- Pseudo-term-listp
- A predicate for recognizing lists of term-like s-expressions
- Guard-holders
- Remove trivial calls from a term
- Termp
- recognizer for the quotation of a term
- Termify
- the process of converting a clause to a term
- L<
- Ordering on naturals or lists of naturals
- Kwote
- Quote an arbitrary object
- Kwote-lst
- Quote an arbitrary true list of objects
