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.
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.
Which of the utterances below are terms?
For each constant below, write a term whose value is the constant.
For each term below, write the constant to which it evaluates.