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

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

The legal variable symbols are symbols other than

Quoted constants are expressions of the form

Closed

The function `program` mode.
Its definition may be inspected with `pe`

*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, `caar` is defined as a macro symbol;
the associated macro function maps the object `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

(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

Translation also maps `flet` forms into applications of

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 `defstobj` event introducing
`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

*Pseudo-Terms: A Common Guard for Metafunctions*

Because `program` mode, it cannot be
used effectively in conjectures to be proved. Furthermore, from the
perspective of merely guarding a term processing function,

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

Pseudo-terms are recognized by the unary function `pseudo-termp`. If
`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 `pseudo-termp` as
the guard.

- Lambda
- Lambda expressions,
LAMBDA objects, andlambda$ 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
- L<
- Ordering on naturals or lists of naturals
- Kwote
- Quote an arbitrary object
- Kwote-lst
- Quote an arbitrary true list of objects