Recursion and Induction: Terms

For the purposes of this document, a *term* is a variable symbol, a
quoted constant, or a function application written as a sequence,
enclosed in parenthesis, consisting of a function symbol of arity *n*
followed by *n* terms.

Since `car` is a function symbol of arity one and `cons` is a function
symbol of arity two, then `(cons (car x) y)` is a term. In more
conventional notation this term would be written *cons* (*car* (*x* ), *y* ). We call
`(car x)` and `y` the *actual expressions* or *actuals* of
the *function call* `(cons (car x) y)`.

Semantically, terms are interpreted with respect to (i) an assignment binding
variable symbols to constants and (ii) an interpretation of function symbols as
mathematical functions. For example, suppose the variables `x` and
`y` are bound, respectively, to the constants `1` and `(2 3 4)`,
and suppose the function symbol `cons` is interpreted as the function
that constructs ordered pairs (as it always is). Then the meaning or
*value* of the term `(cons x y)` is `(1 . (2 3 4))` or,
equivalently, `(1 2 3 4)`. That is, the value of a variable is
determined by the variable assignment; the value of a quoted constant is
that constant; and the value of a function application, `(`*f* *a_1* …
*a_n*`)`, is the result of applying the mathematical function assigned to *f*
to the values of the actuals, *a_i*.

ACL2 provides an infinite number of *variable symbols*, whose syntax is
that of symbols. Some example variable symbols are `x`, `a1`, and
`temp`. The symbols `t` and `nil` are not legal variable symbols.

A *quoted constant* is written by prefixing an integer, a character object, a string, or
a symbol by a single quote mark. For example, `'t`, `'nil`, `'-3`, `'``#\A`,
`'"Hello World!"` and `'LOAD` are quoted constants.
Note that we do not consider `'(1 2 3)` a quoted constant. This
is a mere technicality. We will shortly introduce some abbreviations
that allow us to write `'(1 2 3)` as an abbreviation for
`(cons '1 (cons '2 (cons '3 'nil)))`.

ACL2 also has an infinite number of *function symbols* each of which has
an associated *arity* or number of arguments. For the moment we will
concern ourselves with six primitive function symbols: `cons`, `car`,
`cdr`, `consp`, `if`, and `equal`, described below. Note that
we implicitly specify the arity of each primitive function symbol.

`(cons`- construct and return the ordered pair*x**y*)`(`.*x*.*y*)`(car`- return the left component of*x*)*x*, if*x*is a pair; otherwise, return`nil`.`(cdr`- return the right component of*x*)*x*, if*x*is a pair; otherwise, return`nil`.`(consp`- return*x*)`t`if*x*is a pair; otherwise return`nil`.`(if`- return*x**y**z*)*z*if*x*is`nil`; otherwise return*y*.`(equal`- return*x**y*)`t`if*x*and*y*are identical; otherwise return`nil`.

With these primitives we cannot do anything interesting with numbers, characters, strings, and symbols. They are just tokens to put into or take out of pairs. But we can explore most of the interesting issues in recursion and induction in this setting!

(Maybe explore <<term>>?)

Note that if the terms *α* and *β* both evaluate to
the same value, *v*, then the term `(equal` *α*
*β*`)` evaluates to `t`. For example, the terms
`(car (cons '3 '4))` and `'3` both evaluate to the value
`3`, so the term `(equal (car (cons '3 '4)) '3)` evaluates to
`t`.

**Problem 3. ** Which of the utterances below are terms?

`(car (cdr x))``(cons (car x y) z)``(cons 1 2)``(cons '1 '2)``(cons one two)``(cons 'one 'two)``(equal '1 (car (cons '2 '3)))``(if t 1 2)``(if 't '1 '2)``(car (cons (cdr hi-part) (car lo-part)))``car(cons x y)``car(cons(x,y))``(cons 1 (2 3 4))`

**Problem 4. ** For each constant below, write a term whose value is the constant.

`((1 . 2) . (3 . 4))``(1 2 3)``((1 . t) (2 . nil) (3 . t))``((A . 1) (B . 2))`

**Problem 5. ** For each term below, write the constant to which it evaluates.

`(cons (cons '1 '2) (cons (cons '3 '4) 'nil))``(cons '1 (cons '2 '3))``(cons 'nil (cons (cons 'nil 'nil) 'nil))``(if 'nil '1 '2)``(if '1 '2 '3)``(equal 'nil (cons 'nil 'nil))``(equal 'Hello 'HELLO)``(equal (cons '1 '2) (cons '1 'two))`

Next: