• 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-pairs
        • R-and-i-data-types-exercises
        • R-and-i-symbols
        • R-and-i-identity
        • R-and-i-numbers
        • R-and-i-characters
        • R-and-i-strings
      • 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

• R-and-i-data-types

R-and-i-pairs

Recursion and Induction: Pairs

Pairs are written in Lisp's dot notation. Instead of conventional Cartesian notation, e.g., ⟨ 1, 2 ⟩, Lisp replaces the angle brackets with parentheses and the comma with a dot, (1 . 2). Thus, ((1 . 2) . (3 . 4)) is the pair containing the pair (1 . 2) in its left component and the pair (3 . 4) in its right. In high school, you might have written this object as ⟨⟨1, 2⟩,⟨3, 4⟩⟩.

In Lisp, pairs are called conses. Non-conses are called atoms. The left component is called the car  and the right component is called the cdr  (pronounced “cudder”). (Remark. The names come from the original implementation of Lisp on the IBM 704. That machine had a 36-bit word that was logically divided into two parts, the “address” and the “decrement.” Lisp used such words to represent a cons cell. The address part pointed to the left component and the decrement part pointed to the right component. Thus, the operations were car (“contents of address of register”) and cdr (“contents of decrement of register”).) Lisp provides three conventions for writing parenthesized constants.

• Nil can be written ().

• A pair of the form (x  . nil) may be written (x).

• A pair of the form (x  . (y  …)) may be written (x y  …).

Thus, the cons (1 . (2 . (3 . nil))) may be written (1 2 3). This suggests the most common use of conses: to represent linked lists or sequences. The special role of nil in these conventions is the only sense in which nil is “the empty list.”

Any object can be treated as a list! If a cons is being treated as a list, then its car is the first element and its cdr is treated as a list of the remaining elements. If an atom is treated as a list, it is treated as the empty list. Nil is just the most common atom used in this way.

Thus, the elements of (1 . (2 . (3 . nil))) are 1, 2, and 3, respectively. The length of this list is three. If ((1 . 2) . (3 . 4)) is treated as a list, its elements are (1 . 2) and 3; its length is two. The 4 is just the terminal atom. ((1 . 2) . (3 . nil)) and ((1 . 2) . (3 . 4)) are different objects, but when treated as lists they have the same two elements.

Here is a list of the symbols naming the summer months: (June July August). It could also be written (JUNE . (JULY . (AUGUST . NIL))) and many other ways.

(Maybe explore <<conses>>?)

Next: identity (or Table of Contents)