|
|
|---|
|
|
|
|---|
Recursion and Induction: Abbreviations for Terms
If x is t, nil, an integer, a character object, or a string, and x is used where a term is expected, then x abbreviates the quoted constant 'x. Recall that a single quote mark followed by a symbol, e.g., 'load, is a quoted constant.
In the following, an expression is an integer, a character object, a string, a symbol, an optionally dotted parenthesized sequence of expressions, or a single quote mark followed by an expression. By optionally dotted parenthesized sequence of expressions we mean a parenthesized non-empty sequence of expressions, optionally containing a dot (.) between the last two expressions in the sequence. For example “(A 123 . B)” and “(A (123 B) 'C)” are both optionally dotted parenthesized sequences of expressions.
A single quote mark followed by an optionally dotted parenthesized sequence of expressions, when used as a term, denotes a cons term as follows, using these four rules:
NULL Rule: If '() is used as a term, it abbreviates 'nil.
Singleton Rule: If '(x) is used as a term it abbreviates (cons 'x 'nil).
Dotted Pair Rule: If '(x . y) is used as a term it abbreviates (cons 'x 'y).
List Rule: If '(x α) is used as a term and α is any non-empty sequence of expressions it abbreviates (cons 'x '(α)). Note the new pair of parentheses around α.
Thus, for example, the rules above mean that if '(A B C) is used as a term then it denotes (cons 'A '(B C)), which denotes (cons 'A (cons 'B '(C))), which denotes (cons 'A (cons 'B (cons 'C 'nil))).
If '(A B . C) is used as a term it denotes (cons 'A (cons 'B 'C)).
It remains to deal with cases like ''A and ''(A 'B) involving multiple single quote marks. We do not expect to use such expressions in this course but we specify their meaning just for completeness.
Let α be an expression that does not start with a single quote mark. Consider a sequence of two or more single quote marks followed by α and suppose it is used as a term. It denotes a cons derived as follows. Replace α and the single quote mark immediately before it with (quote α). Repeat that replacement until all but the first single quote mark remains. Then apply the four rules above.
Thus, ''(A 'B), when used as a term, denotes the term derived by the following sequence of steps
''(A 'B)
'(quote (A 'B))
(cons 'quote '((A 'B)))
(cons 'quote (cons '(A 'B) 'nil))
(cons 'quote (cons (cons 'A '('B)) 'nil))
(cons 'quote (cons (cons 'A (cons ''B 'nil)) 'nil))
(cons 'quote (cons (cons 'A (cons '(quote B) 'nil)) 'nil))
(cons 'quote (cons (cons 'A (cons (cons 'quote '(B)) 'nil)) 'nil))
(cons 'quote (cons (cons 'A (cons (cons 'quote (cons 'B 'nil)) 'nil)) 'nil))
Note that every occurrence of single quote now marks a quoted constant.
When (list x_1 … ) is used as a term, it abbreviates (cons x_1 (list … )). When (list) is used as a term, it abbreviates nil. Thus (list a b c) abbreviates (cons a (cons b (cons c nil))).
And and or will be defined as function symbols of two arguments. But if and is used as though it were a function symbol of more than two arguments, then it abbreviates the corresponding right-associated nest of ands. Thus, (and p q r s), when used where a term is expected, abbreviates (and p (and q (and r s))).
If or is used as though it were a function symbol of more than two arguments, then it abbreviates the corresponding right-associated nest of ors.
(Maybe explore term abbreviation in ACL2? But abbreviation is complicated in ACL2 by the presence of a powerful macro facility. To learn about ACL2 term abbreviation, explore <<term>>, paying special attention to “untranslated” terms. Maybe also explore <<macros>>.)
Problem 7.
Show the term abbreviated by each of the following:
The art of displaying a Lisp term in a way that it can be easily read by a person is called pretty printing. We recommend the following heuristics. First, write clearly and count your parentheses. Second, try never to write a single line with more than about 30 non-blank characters on it. Third, if a function call will not fit on a line, break it into multiple lines, indenting each argument the same amount.
Below we show one term pretty printed with successively narrower margins. (Note that the display is a term only if app is a function symbol of arity two.) We find the second and third lines of the first display below excessively long. Each display shows exactly the same term. Note how we break terms to indent arguments the same amount and how we sometimes slide the arguments under the function symbol to save horizontal space. Personally, we find the second display below (the one labeled “width 46”) the easiest to read. We show the others merely to illustrate how more space can be saved when one finds oneself close to the right margin.
|<---------------------------- width 70 ---------------------------->|
(IMPLIES (AND (CONSP A)
(EQUAL (APP (APP (CDR A) B) C) (APP (CDR A) (APP B C))))
(EQUAL (APP (APP A B) C) (APP A (APP B C))))
|<---------------- width 46 ---------------->|
(IMPLIES (AND (CONSP A)
(EQUAL (APP (APP (CDR A) B) C)
(APP (CDR A) (APP B C))))
(EQUAL (APP (APP A B) C)
(APP A (APP B C))))
|<------------ width 38 ------------>|
(IMPLIES
(AND (CONSP A)
(EQUAL (APP (APP (CDR A) B) C)
(APP (CDR A) (APP B C))))
(EQUAL (APP (APP A B) C)
(APP A (APP B C))))
|<---------- width 34 ---------->|
(IMPLIES
(AND
(CONSP A)
(EQUAL (APP (APP (CDR A) B) C)
(APP (CDR A) (APP B C))))
(EQUAL (APP (APP A B) C)
(APP A (APP B C))))
|<------- width 28 ------->|
(IMPLIES
(AND
(CONSP A)
(EQUAL
(APP (APP (CDR A) B) C)
(APP (CDR A) (APP B C))))
(EQUAL
(APP (APP A B) C)
(APP A (APP B C))))
|<---- width 23 ----->|
(IMPLIES
(AND
(CONSP A)
(EQUAL
(APP (APP (CDR A) B)
C)
(APP (CDR A)
(APP B C))))
(EQUAL
(APP (APP A B) C)
(APP A (APP B C))))
Next: