• Top
  • Documentation
    • Xdoc
    • ACL2-doc
    • Recursion-and-induction
      • R-and-i-annotated-bibliography
      • R-and-i-definitions-revisited
      • R-and-i-terms
      • R-and-i-structural-induction
      • R-and-i-relations-between-recursion-and-induction
      • R-and-i-ordinals
      • R-and-i-inadequacies-of-structural-recursion
      • R-and-i-axioms
      • R-and-i-abbreviations-for-terms
      • R-and-i-terms-as-formulas
      • R-and-i-more-problems
      • R-and-i-still-more-problems
      • R-and-i-definitional-principle
      • R-and-i-function-definitions
      • R-and-i-introduction
      • R-and-i-table-of-contents
      • R-and-i-substitutions
      • R-and-i-arithmetic
      • R-and-i-induction-principle
      • R-and-i-data-types
      • R-and-i-more-inadequacies-of-the-definitional-principle
    • Loop$-primer
    • Operational-semantics
    • Pointers
    • Doc
    • Documentation-copyright
    • Course-materials
    • Args
    • ACL2-doc-summary
    • Finding-documentation
    • Broken-link
    • Doc-terminal-test-2
    • Doc-terminal-test-1
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Recursion-and-induction

R-and-i-terms

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 x y) - construct and return the ordered pair (x . y).

(car x) - return the left component of x, if x  is a pair; otherwise, return nil.

(cdr x) - return the right component of x, if x  is a pair; otherwise, return nil.

(consp x) - return t if x  is a pair; otherwise return nil.

(if x y z) - return z  if x  is nil; otherwise return y.

(equal x y) - return 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?

1. (car (cdr x))
2. (cons (car x y) z)
3. (cons 1 2)
4. (cons '1 '2)
5. (cons one two)
6. (cons 'one 'two)
7. (equal '1 (car (cons '2 '3)))
8. (if t 1 2)
9. (if 't '1 '2)
10. (car (cons (cdr hi-part) (car lo-part)))
11. car(cons x y)
12. car(cons(x,y))
13. (cons 1 (2 3 4))

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

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

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

1. (cons (cons '1 '2) (cons (cons '3 '4) 'nil))
2. (cons '1 (cons '2 '3))
3. (cons 'nil (cons (cons 'nil 'nil) 'nil))
4. (if 'nil '1 '2)
5. (if '1 '2 '3)
6. (equal 'nil (cons 'nil 'nil))
7. (equal 'Hello 'HELLO)
8. (equal (cons '1 '2) (cons '1 'two))

Next: Substitutions (or Table of Contents)