perm filename LSPDOC[206,LSP]4 blob sn#262820 filedate 1977-02-03 generic text, type C, neo UTF8

COMMENT ⊗ VALID 00038 PAGES C REC PAGE DESCRIPTION C00001 00001 C00004 00002 .require "book.pub[let,jmc]" source_file C00011 00003 .INSERT CONTENTS C00015 00004 .ss Atoms. C00017 00005 .ss List structures. C00023 00006 .ss S-expressions. C00032 00007 .ss The basic functions and predicates of LISP. C00045 00008 .ss Conditional expressions. C00052 00009 .ss Boolean expressions. C00056 00010 .ss Recursive function definitions. C00074 00011 .ss Lambda expressions and functions with functions as arguments. C00086 00012 .ss Label. C00089 00013 .ss Numerical computation. C00096 00014 .s HOW TO WRITE RECURSIVE FUNCTION DEFINITIONS C00102 00015 .ss Simple list recursion. C00111 00016 .ss Simple S-expression recursion. C00114 00017 .ss Other structural recursions. C00117 00018 .ss Tree search recursion. C00132 00019 .ss Game trees. C00144 00020 .s COMPILING IN LISP C00148 00021 .ss Some facts about the PDP-10. C00154 00022 .ss Code produced by LISP compilers. C00155 00023 .BEGIN VERBATIM SELECT 1 C00158 00024 Note that all three compilers produce the same first line of C00161 00025 .ss Listings of LCOM0 and LCOM4 C00162 00026 .SKIP TO LINE 1 C00163 00027 .SKIP TO LINE 1 C00176 00028 .SKIP TO LINE 1 C00177 00029 .s COMPUTABILITY C00202 00030 .s PROVING LISP PROGRAMS CORRECT C00205 00031 .ss First order logic with conditional forms and lambda-expressions. C00217 00032 .ss Conditional forms. C00223 00033 .ss Lambda-expressions. C00225 00034 .ss Algebraic axioms for S-expressions and lists. C00229 00035 .ss Axiom schemas of induction. C00232 00036 .ss Proofs by structural induction. C00235 00037 .ss First Order Theory of Partial Functions C00236 00038 .BACK C00237 ENDMK C⊗; .require "book.pub[let,jmc]" source_file; .font B "ms25"; .font C "grfx25" .font D "grfx35" .PORTION TITLEPAGE .sname ← SSNAME ← NULL .skip 20 .cb RECURSIVE PROGRAMMING IN LISP .SKIP 4 .CB by John McCarthy .skip 20 .cb Stanford University .skip 5 .cb Copyright %Bc%* 1977 by John McCarthy .skip 10 .once center .TURN ON "{}" This version printed at {time} on {date}. .TURN OFF "{}" .INSERT CONTENTS .PORTION MAINPORTION .sname ← SSNAME ← NULL .s INTRODUCTION TO LISP .ss Lists. Symbolic information in LISP is expressed by S-expressions and these are represented in the memory of the computer by list structures. Before giving formal definitions, we shall give some examples. The most common form of S-expression is the list, and here are some lists: .NOFILL The list (A B C E) %1has four elements. The list (A B (C D) E) %1has four elements one of which is itself a list. The list (A) %1has one element. The list ((A B C D)) %1also has one element which itself is a list. The list () %1has no elements; it is also written NIL. %1The list (PLUS X Y) %1has three elements and may be used to represent the expression %2x + %2y. %1The list (PLUS (TIMES X Y) X 3) %1has four elements and may be used to represent the expression %2xy + %2x + 3. %1The list (EXIST X (ALL Y (IMPLIES (P X) (P Y)))) %1may be used to represent the logical expression (∃%2x)(∀%2y).%2P(%2x)⊃%2P(%2y). %1The list (INTEGRAL 0 ∞ (TIMES (EXP (TIMES I X Y)) (F X)) X) %1may be used to represent the expression .TURN ON "↑↓[]&_∪"; %A$%50%6↑∞%2e%6ixy%2f(%2x)%2dx. .TURN OFF %1The list ((A B) (B A C D) (C B D E) (D B C E) (E C D F) (F E)) %1 .FILL is used to represent the network of Figure 1 according to a scheme whereby there is a sublist for each vertex consisting of the vertex itself followed by the vertices to which it is connected. .begin verbatim; select d; INDENT 17; C .SKIP 20 MILLS; ≤'~`≥ ≤' ~ `≥ B ≤' ~ `≥ E .once superimpose 2; A ααααααααα' ~ `ααααααααα F ≥ ≤ `≥ ~ ≤' `≥ ~ ≤' `≥~≤' .SKIP 50 MILLS; D Figure 1 .END The elements of a list are surrounded by parentheses and separated by spaces. A list may have any number of terms and any of these terms may themselves be lists. In this case, the spaces surrounding a sublist may be omitted, and extra spaces between elements of a list are allowed. Thus the lists (A B(C D) E) %1and (A B (C D) E) %1are regarded as the same. .ss Atoms. The expressions A, B, X, Y, 3, PLUS, %1and ALL%1 occurring in the above lists are called atoms. In general, an atom is expressed by a sequence of capital letters, digits, and special characters with certain exclusions. The exclusions are <space>, <carriage return>, and the other non-printing characters, and also the parentheses, brackets, semi-colon, and comma. Numbers are expressed as signed decimal or octal numbers, the exact convention depending on the implementation. Floating point numbers are written with decimal points and, when appropriate, an exponent notation depending on the implementation. The reader should consult the programmer's manual for the LISP implementation he intends to use. Some examples of atoms are .NOFILL THE-LAST-TRUMP A307B 345 3.14159, .FILL %1and from these we can form lists like ((345 3.14159 -47) A307B THE-LAST-TRUMP -45.21). %1 .ss List structures. Lists are represented in the memory of the computer by list structures. A list structure is a collection of memory words each of which is divided into two parts, and each part is capable of containing an address in memory. The two parts are called are called the a-part and the d-part. There is one computer word for each element of the list, and the a-part of the word contains the address of the list or atom representing the element, and the d-part contains the address of the word representing the next element of the list. If the list element is itself a list, then, of course, the address of the first word of its list structure is given in the a-part of the word representing that element. A diagram shows this more clearly than words, and the list structure corresponding to the list (PLUS (TIMES X Y) X 3)%1 which may represent the expression %2xy + %2x + 3 is shown in figure 2. .begin verbatim select c; ⊂αααπααα⊃ ⊂αααπααα⊃ ⊂αααπααα⊃ ⊂αααπααα⊃ ααααα→~ ~ εαααα→~ ~ εαααα→~ ~ εαααα→~ ~ εααααααα⊃ %απα∀ααα$ %απα∀ααα$ %απα∀ααα$ %απα∀ααα$ ~ ↓ ~ ~ ↓ ~ PLUS ~ ~ 3 ~ ~ ⊂αααπααα⊃ ~ ⊂αααπααα⊃ ⊂αααπααα⊃ ~ %α→~ ~ εααβα→~ ~ εαααα→~ ~ ~ ~ %απα∀ααα$ ~ %απα∀ααα$ %απα∀απα$ ~ ↓ ~ ~ ↓ ~ ~ TIMES %απαα$ Y %ααπα$ ↓ ↓ X NIL Figure 2. .END Atoms are represented by the addresses of their property lists which are list structures of a special kind depending on the implementation. (In some implementations, the first word of a property list is in a special area of memory, in others the first word is distinguished by sign, in still others it has a special a-part. For basic LISP programming, it is enough to know that atoms are distinguishable from other list structures by a predicate called %3at%1.) The last word of a list cannot have the address of a next word in its d-part since there isn't any next word, so it has the address of a special atom called NIL%1. A program referrs to a list by the address of its first element. According to this convention, we see that the a-part of a list word is the list element and the d-part is a pointer to a sublist formed by deleting the first element. Thus the first word of the list structure of figure 2 contains a pointer to the list structure representing the atom PLUS%1, while its d-part points to the list ((TIMES X Y) X 3)%1. The second word contains the list structure representing (TIMES X Y)%1 in its a-part and the list structure representing (X 3)%1 in its d-part. The last word points to the atom 3%1 in its a-part and has a pointer to the atom NIL%1 in its d-part. This is consistent with the convention that NIL%1 represents the null list. .ss S-expressions. When we examine the way list structures represent lists we see a curious asymmetry. Namely, the a-part of a list word can contain an atom or a list, but the d-part can contain only a list or the special atom NIL%1. This restriction is quite unnatural from the computing point of view, and we shall allow arbitrary atoms to inhabit the d-parts of words, but then we must generalize the way list structures are expressed as character strings. To do this, we introduce the notion of S-expression. An S-expression is either an atom or a pair of S-expressions separated by "_._" and surrounded by parentheses. In BNF, we can write <S-expression> ::= <atom> | (<S-expression> . <S-expression>). Examples of S-expressions are .NOFILL A (A . B) (A . (B . A)) (PLUS (X . (Y . NIL))) (3 . 3.4) .FILL %1The spaces around the . may be omitted when this will not cause confusion. The only possible confusion is of the dot separator with a decimal point in numbers. Thus, in the above cases, we may write (A.B), (A.(B.A))%1, and (PLUS.(X.(Y.NIL)))%1, but if we wrote (3.3.4)%1 confusion would result. In the memory of a computer, an S-expression is represented by the address of a word whose a-part contains the first element of the pair and whose d-part contains the second element of the pair. Thus, the S-expressions (A.B), (A.(B.A))%1, and (PLUS.(X.(Y.NIL))) %1 are represented by the list structures of figure 3. .begin verbatim select c; ⊂αααπααα⊃ ⊂αααπααα⊃ ⊂αααπααα⊃ ~ ~ ~ ~ ~ εαααα→~ ~ ~ %απα∀απα$ %απα∀ααα$ %απα∀απα$ ↓ ↓ ~ ↓ ~ A B ~ B ~ ~ ~ ~ ~ %ααααααααπαααααααα$ ↓ A ⊂αααπααα⊃ ⊂αααπααα⊃ ⊂αααπααα⊃ ~ ~ εαααα→~ ~ εαααα→~ ~ ~ %απα∀ααα$ %απα∀ααα$ %απα∀απα$ ↓ ↓ ↓ ↓ PLUS X Y NIL Figure 3. .END Note that the list (PLUS X Y)%1 and the S-expression (PLUS . (X . (Y . NIL)))%1 are represented in memory by the same list structure. The simplest way to treat this is to regard S-expressions as primary and lists as abbreviations for certain S-expressions, namely those that never have any atom but NIL as the second part of a pair. In giving input to LISP, either the list form or the S-expression form may be used for lists. On output, LISP will print a list structure as a list as far as it can, otherwise as an S-expression. Thus, some list structures will be printed in a mixed notation, e.g. ((A . B) (C . D) (3))%1. In general, the list (%2a b . . . z)%1 may be regarded as an abbreviation of the S-expression (%2a . (%2b . (%2c . (... (%2z . NIL) ...)))%1. .SKIP 2 .GROUP Exercises 1. If we represent sums and products as indicated above and .APART use (MINUS X), (QUOTIENT X Y)%1, and (POWER X Y)%1 as representations of -%2x%1, %2x/%2y%1, and %2x%6y%1 respectively, then a. What do the lists (QUOTIENT 2 (POWER (PLUS X (MINUS Y)) 3)) %1and (PLUS -2 (MINUS 2) (TIMES X (POWER Y 3.3))) %1represent? b. How are the expressions %2xyz+3(%2u+%2v)%6-3%1 and (%2xy-%2yx)/(%2xy+%2yx)%1 to be represented? 2. In the above mentioned graph notation, what graph is represented by the list ((A D E F)(B D E F)(C D E F)(D A B C)(E A B C)(F A B C))? %13. Write the list ((PLUS (TIMES X Y) X 3)%1 as an S-expression. This is sometimes referred to as "dot-notation". 4. Write the following S-expressions in list notation to whatever extent is possible: .NOFILL a. (A . NIL) b. (A . B) c. ((A . NIL) . B) d. ((A . B) . ((C . D) . NIL). .FILL 5. Prove that the number of "shapes" of S-expressions with %2n%1 atoms is %2(2n - 2)!/(n!(n - 1)!)%1. (The two shapes of S-expressions with three atoms are (A.(B.C))%1 and ((A.B).C)%1). 6. The above result can also be obtained by writing %2S_=#A#+#S%3x%2S%1 as an "equation" satisfied by the set of S-expressions with the interpretation that an S-expression is either an atom or a pair of S-expressions. The next step is to regard the equation as the quadratic %2S%62%2_-_S_+_A_=_0%1, solve it by the quadratic formula choosing the minus sign for the square root. Then the radical is regarded as the 1/2 power and expanded by the binomial theorem. Manipulating the binomial coefficients yields the above formula as the coefficient of %2A%6n%1 in the expansion. Why does this somewhat ill-motivated and irregular procedure give the right answer? The last two exercises are unconnected with subsequent material in these notes. .ss The basic functions and predicates of LISP. The main form of LISP program is the LISP function, and LISP functions are built up from basic LISP functions, predicates, variables and constants. An expression with variables in it whose value depends on the values of the variables is called a %2form%1. LISP functions are constructed from LISP %2forms%1 which are written in two languages - %2publication language%1 and %2internal language%1. Publication language is easier for people to read and write, but publication language programs are not S-expressions, and therefore it is not easy to write LISP programs to generate, interpret or compile other LISP programs when these programs are in publication language. The internal language programs are S-expressions and are harder for a person to read and write, but it is easier for a person to write a program to manipulate %2object programs%1 when the object programs are in internal language. Besides all that, most LISP implementations accept only internal language programs rather than some form of publication language. Just as numerical computer programs are based on the four arithmetic operations of addition subtraction, multiplication, and division, and the arthmetic predicates of equality and comparison, so symbolic computation has its basic predicates and functions. LISP has three basic functions and two predicates. Each will be explained first in its publication form, and then the internal form will be given. First, we have two functions %3a%1 and %3d%1. %3a %2x%1 is the a-part of the S-expression x%1. Thus, %3a(A . B) = A%1, and %3a((A . B) . A) = (A . B)%1. %3d %2x%1 is the d-part of the S-expression %2x%1. Thus %3d(A . B) = B%1, and %3d((A . B) . A) = A%1. %3a %2x%1 and %3d %2x%1 are undefined in basic LISP when %2x%1 is an atom, but they may have a meaning in some implementations. The internal forms of %3a %2x%1 and %3d %2x%1 are (CAR X)%1 and (CDR X)%1 respectively. The names CAR%1 and CDR%1 stood for "contents of the address part of register" and "contents of the decrement part of register" in a 1957 precursor of LISP projected for the IBM 704 computer. The names have persisted for lack of a clearly preferable alternative. A certain ambiguity arises when we want to use S-expression constants in the internal language. Namely, the S-expression A%1 could either stand for itself or stand for a variable A%1 whose value is wanted. Even (CAR X)%1 is ambiguous since sometime the S-expression (CAR X)%1 itself must be referred to and not the result of evaluating it. Internal language avoids the ambiguity by using (QUOTE %2e)%1 to stand for the S-exression %2e%1. Thus the publication language form %3a (A B)%1 corresponds to the internal language form (CAR (QUOTE (A.B)))%1 and both have the value A%1 obtained by taking the %3a%1-part of the S-expression (A.B)%1. Since lists are a particular kind of S-expression, the meanings of %3a%1 and %3d%1 for lists are also determined by the above definitions. Thus, we have %3a(A B C D) =%3 A %1and %3d(A B C D) = (B C D), %1and we see that, in general, %3a %2x%1 is the first element of the list %2x%1, and %3d %2x%1 is the rest of the list, deleting that first element. Notice that for S-expressions, the definitions of %3a %2x%1 and %3d %2x%1 are symmetrical, while for lists the symmetry is lost. This is because of the unsymmetrical nature of the convention that defines lists in terms of S-expressions. Notice, further, our convention of writing %3a%1 and %3d%1__ without brackets surrounding the argument. Also, we use lower case letters for our function names and for variables, reserving the upper case letters for the S-expressions themselves. The third function %2cons[%2x, %2y]%1 forms the S-expression whose a-part and d-part are %2x%1 and %2y%1 respectively. Thus %2cons[(A.B), A] = ((A.B).A). %1We see that for lists, %2cons%1 is a prefixing operation. Namely, %2cons[%2x, %2y]%1 is the list obtained by putting the element %2x%1__ onto the front of the list %2y%1. Thus %2cons[A, (B C D E)] = (A B C D E). %1If we want %2cons[%2x, %2y]%1 to be a list, then %2y%1 must be a list (possibly the null list NIL%1), and %2x%1 must be a list or an atom. In the case of S-expressions in general, there is no restriction on the arguments of %2cons%1. Usually, we shall write %2x . y%1 instead of %2cons[%2x, %2y]%1 since this is briefer. The internal language form of %2cons[x,y]%1 is (CONS X Y)%1. The name "CONS" comes from "construct" referring to the way %2cons[x,y]%1 is constructed from the free storage list. The first predicate is %3at %2x%1. %3at %2x%1 is true if the S-expression %2x%1 is atomic and false otherwise. The internal form is (ATOM X)%1. The second predicate is equality of atomic symbols written %2x %3eq %2y%1. Equality of S-expressions is tested by a program based on %3eq%1. Actually %3eq%1 does a bit more than testing equality of atoms. Namely, %2x %3eq %2y%1 is true if and only if the addresses of the first words of the S-expressions %2x%1 and %2y%1 are equal. Therefore, if %2x %3eq %2y%1, then %2x%1 and %2y%1 are certainly the same S-expression since they are represented by the same structure in memory. The converse is false because there is no guarantee in general that the same S-expression is not represented by two different list structures. In the particular case where at least one of the S-expressions is known to be an atom, this guarantee can be given, because LISP represents atoms uniquely in memory. The internal form is (EQ X Y)%1. The above are all the basic functions of LISP; all other LISP functions can be built from them using recursive conditional expressions as will shortly be explained. However, the use of certain abbreviations makes LISP programs easier to write and understand. %3n %2x%1 is an abbreviation for %2x %3eq NIL%1. It rates a special notation because NIL%1 plays the same role among lists that zero plays among numbers, and list variables often have to be tested to see if their value is NIL%1. Its internal form is (NULL X)%1. The notation %2list[%2x1, x2, . . . , xn]%1 is used to denote the composition of %2cons%1's that forms a list from its elements. Thus %2list[x, y, z] = cons[x, cons[y, cons[z, NIL%2]]]%1 and forms a list of three elements out of the quantities %2x, y, %1 and %2z%1. We often write <%2x y . . . z>%1 instead of %2list[%2x, y, . . . , z]%1 when this will not cause confusion. The experienced implementer of programming languages will expect that since %2list%1 has a variable number of arguments, its implementation will pose problems. He will be right. The internal form of %2<x y ... z>%1 is (LIST X Y ... Z)%1. Compositions of %3a%1 and %3d%1 are written by concatenating the letters %3a%1 and %3d%1. Thus, it is easily seen that %3ad %2x%1 denotes the second element of the list %2x%1, and %3add %2x%1 denotes the third element of that list. The internal forms of these functions are CADR%1 and CADDR%1 respectively. Besides the basic functions of LISP, there will be user-defined functions. We haven't given the mechanism function definition yet, but suppose a function %2subst%1 taking three arguments has been defined. It may be used in forms like %2subst[x,y,z]%1 having internal form (SUBST X Y Z)%1. As in other programming languages and in mathematics generally, new forms can be constructed by applying the functions and predicates to other forms and not just to variables and constants. Thus we have forms like %2subst[x,y,%3a z%2] . subst[x,y,%3d %2z]%1 involving a user defined function %2subst%1. Its internal form is (CONS (SUBST X Y (CAR Z)) (SUBST X Y (CDR Z)))%1. .ss Conditional expressions. When the form that represents a function depends on whether a certain predicate is true of the arguments, conditional expressions. are used. The conditional expression (more properly %2conditional form%1) %3if %2p %3then %2a %3else %2b %1is evaluated as follows: First %2p%1 is evaluated and determined to be true or false. If %2p%1 is true, then %2a%1 is evaluated and its value is the value of the expression. If %2p%1 is false, then %2b%1 is evaluated and its value is the value of the expression. Note that if %2p%1 is true, %2b%1 is never evaluated, and if %2p%1 is false, then %2a%1 is never evaluated. The importance of this will be explained later. A familiar function that can be written conveniently using conditional expressions is the absolute value of a real number. We have |%2x| = %3if %2x<0 %3then -%2x %3else %2x. %1A more general form of conditional expression is %3if %2p %3then %2a %3else if %2q %3then %2b . . . %3else if %2s %3then %2d %3else %2e. %1There can be any number of terms; the value is determined by evaluating the propositional terms %2p, q%1, etc. until a true term is found; the value is then that of the term following the next %3then%1. If none of the propositional terms is true, then the value is that of the term following the %3else%1. The function graphed in figure 4 is described by the equation %2tri[%2x] = %3if %2x<-1 %3then 0 %3else if %2x<0 %3then 1+%2x %3else if %2x<1 %3then 1-%2x %3else 0. .BEGIN NOFILL; PREFACE 0 MILLS; . VARIABLE CHQZWX; . TURN OFF "%παβ#∞∂\→←↓↑∪{"; . AT 8 ⊂" "⊃ ; <<i.e. nothing special--disables other AT 8 response>> . AT 16 ⊂" "⊃ ; <<similar>> . AT "∞" ⊂ TURN ON "∂{"; CHQZWX←CHARW; CHARW←8}∂+1{CHARW←CHQZWX; TURN OFF; ⊃; . GROUP . SELECT D; . NARROW 0,-1000 ∞ ~ ∞ ~ .once superimpose 2; ≤'`≥(0,1) ∞ ~ ≤'∞ ~∞ `≥ ≤'∞ ~∞ `≥ ≤'∞ ~∞ `≥ .once superimpose 2; '∞ ~∞ ` ======================αααααααααααααααααα====================== ∞ (-1,0) ~ (1,0) ∞ ~ ∞ ~ Figure 4. .WIDEN .END The internal form of conditional forms is made in a more regular way than the publication form; the publication form was altered to conform to ALGOL. We write (COND (p1 e1) (p2 e2) ... (pn en))%1 with any number of terms. Its value is determined by evaluating the p%1's successively until one is found which is true. Then the corresponding e%1 is taken as the value of the conditional expression. If none of the p%1's is true, then the value of the conditional expression is undefined. Thus all the e%1's are treated the same which makes programs for interpreting or compiling conditional expressions easier to write. Putting parentheses around each p-e%1 pair was probably a mistake in the design of LISP, because it unnecessarily increases the number of right parentheses. It should have been (COND p1 e1 p2 e2 ... pn en)%1, but such a change should be made now only as part of a massive improvement. Conditional expressions may be compounded with functions to get forms like %3if n %2x %3then NIL %3else %3a %2x . append[%3d %2x,y]%1 involving a yet to be defined function %2append%1. The internal form of this is (COND ((NULL X) NIL) (T (CONS (CAR X) (APPEND (CDR X) Y))))%1. One would normally have expected to write (QUOTE NIL)%1 and (QUOTE T)%1, but there is a special convention that NIL%1 and T%1 may be written without QUOTE%1. This means that these symbols cannot be used as variables. The value of T%1 is the propositional constant %3true%1, i.e. it is always true so that it is impossible to "fall off the end" of a conditional expression with T%1 as its last p%1. It is the translation into internal form of the final %3else%1 of a conditional expression. .ss Boolean expressions. In making up the propositional parts of conditional expressions, it is often necessary to combine elementary propositional expressions using the Boolean operators and, or, and not. We use the symbols ∧%1, ∨%1, and ¬%1 respectively, for these operators. The Boolean operators may be described simply by listing the values of the elementary Boolean expressions for each case of the arguments. Thus we have: .NOFILL T∧T = T T∧F = F F∧T = F F∧F = F T∨T = T T∨F = T F∨T = T F∨F = F ¬T = F ¬F = T. .FILL Since both ∧ and ∨ are associative we can write Boolean forms like %2p1∧p2∧p3%1 without worrying about grouping. The internal forms are (AND p1 p2 ... pn)%1, (OR p1 p2 ... pn)%1 and (NOT p)%1. It is also customary to use NIL%1 instead of F%1, because in most LISP systems both Boolean %3false%1 and the null list are represented by the number 0. This makes certain tests run faster, but introduces so many complications in implementation that it was certainly a bad idea. %1The Boolean operators can be described by conditional expressions in the following way: .NOFILL %2p∧%2q = %3if %2p %3then %2q %3else F %2p∨%2q = %3if %2p %3then T %3else %2q ¬%2p = %3if %2p %3then F %3else T. .FILL %1Note that if %2p%1 is false %2p∧%2q%1 is false independent of the value of %2q%1, and likewise if %2p%1 is true, then %2p∨%2q%1 is true independent of %2q%1. If %2p%1 has been evaluated and found to be false, then %2q%1 does not have to be evaluated at all to find the value of %2p∧%2q%1, and, in fact, LISP does not evaluate %2q%1 in this case. Similarly, %2q%1 is not evaluated in evaluating %2p∨%2q%1 if %2p%1 is true. This procedure is in accordance with the above conditional expression descriptions of the Boolean operators. The importance of this convention which contrasts with that of ALGOL 60, will be apparent later when we discuss recursive definitions of functions and predicates. Boolean expressions can be combined with functions and conditional exrpessions to get forms like %3 if n %2x ∨ %3n d %2 x %3then %2x %3else %3a %2x . alt %3dd %2x%1 the internal form of which is (COND ((OR (NULL X) (NULL (CDR X))) X) (T (CONS (CAR X) (ALT (CDDR X)))))%1. .ss Recursive function definitions. In such languages as FORTRAN and Algol, computer progrrams are expressed in the main as sequences of assignment statements and conditional %3go to%1's. In LISP, programs are mainly expressed in the form of recursively defined functions. We begin with an example. The function %2alt[%2x]%1 gives a list whose elements are alternate elements of the list %2x%1 beginning with the first. Thus .NOFILL %2alt[(A B C D E)] = (A C E), %2alt[(((A B) (C D))] = ((A B)), %2alt[(A)] = (A), %1and %2alt[NIL] = NIL. .fill In LISP %2alt%1 is defined by the equation %2alt[x] ← %3if n %2x ∨ %3n d %2x %3then %2x %3else a %2x . alt[%3dd %2x]%1. In case you need a review of our precedence conventions, fully bracketed it looks like %2alt[x] ← %3if %2[%3n%2[x] ∨ %3n%2[%3d%2[x]]] %3then%2 x %3else%2 [%3a%2[x] . alt[%3dd%2[x]]]%1. This definition uses no ways of forming expressions that we haven't introduced previously, but it uses the function %2alt%1 in the right hand side of its own defining equation. To get the value of %2alt x%1 for some particular list, we evaluate the right hand side of the definition substituting that list for %2x%1 whenever %2x%1 is encountered and re-evaluating the right hand side with a new %2x%1 whenever a form %2alt e%1 is encountered. This process is best explained by using it to evaluate some expressions. Consider evaluating %2alt[NIL]%1. We do it by evaluating the expression to the right of the ←%1 sign remembering that the variable %2x%1 has the value NIL%1. A conditional expression is evaluated by first evaluating the first propositional term ¬ in this case %3n %2x ∨ %3n d %2x%1. This expression is a disjunction and in its evaluation we first evaluate the first disjunct, namely %3n_%2x%1. Since %2x = NIL, %3n %2x%1 is true, the disjunction is true, and the value of the conditional expression is the value of the term after the first true propositiional term. The term is %2x%1, and its value is NIL%1, so the value of %2alt[NIL]%1 is NIL%1 as stated above. Obeying the rules about the order of evaluation of terms in conditional and Boolean expressions is important in this case since if we didn't obey these rules, we might find ourselves trying to evaluate %3n d %2x%1 or %2alt[%3dd %2x]%1, and since %2x%1 is NIL%1, neither of these has a value. An attempt to evaluate them in LISP would give rise to an error return. As a second example, consider %2alt[(A B)]%1. Since neither %3n %2x%1 nor %3n d %2x%1 is true in this case, the disjunction %3n %2x ∨ %3n d %2x %1is false and the value of the expression is the value of %3a %2x . alt[%3dd %2x]. %3a %2x%1 has the value A%1, and %3dd %2x%1 has the value NIL%1, so we must now evaluate %2alt[NIL]%1, and we already know that the value of this expression is NIL%1. Therefore, the value of %2alt[(A B)]%1 is that of A.NIL%1 which is (A)%1. We can describe this evaluation in a less wordy way by writing .NOFILL %2alt[(A B)] = %3if n(A B) ∨ %3n d(A B) %3then (A B) %3else %3a(A B).%2alt[%3dd(A B)] = %3if NIL ∨ %3n d(A B) %3then (A B) %3else %3a(A B).%2alt[%3dd(A B)] = %3if NIL %3then (A B) %3else %3a(A B).%2alt[%3dd(A B)] = %3a(A B).%2alt[%3dd(A B)] = A.%2alt[NIL] = A.[%3if nNIL ∨ %3ndNIL %3then NIL %3else aNIL.%2alt[%3ddNIL]] = A.[%3if T ∨ %3ndNIL %3then NIL %3else aNIL.%2alt[%3ddNIL]] = A.[%3if T %3then NIL %3else aNIL.%2alt[%3ddNIL]] = A.[NIL] = (A). .FILL %1This is still very long-winded, and now that the reader understands the order of evaluation of conditional and Boolean expressions, we can proceed more briefly to evaluate %2alt[(A B C D E)] = A.%2alt[(C D E)] = A.[C.%2alt[(E)]] = A.[C.(E)] = (A C E). %1Here are three more examples of recursive functions and their application: We define %2last%1 by %2last[%2x] ← %3if n d %2x %3then a %2x %3else %2last[%3d %2x], %1and we compute %2last[(A B C)] = %3if nd(A B C) %3then a(A B C) %3else %2last[%3d(A B C)] = %2last[(B C)] = %2last[(C)] = C. %1Clearly %2last%1 computes the last element of a list. %2last[NIL]%1 is undefined in the LISP language; the result of trying to compute it may be an error message or may be some random result depending on the implementation. The function %2subst%1 is defined by %2subst[%2x, y, z] ← %3if at %2z %3then [%3if %2z %3eq %2y %3then %2x %3else %2z] %3else %2subst[x,y,%3a %2z].subst[x,y,%3d %2z]%1. We have %2subst[(A.B), X, ((X.A).X)] = = %2subst[(A.B), X, (X.A)]%2subst[(A.B), X, X] = [%2subst[(A.B), X, X].%2subst[(A.B), X, A]].(A.B) = [[(A.B)].A].(A.B)] = (((A.B).A).(A.B)). %2subst%1 computes the result of substituting the S-expression %2x%1 for the atom %2y%1 in the S-expression %2z%1. This operation is important in all kinds of symbolic computation. The function %2append[x,y]%1 which gives the concatenation of the lists %2x%1 and %2x%1 is also important. It is also denoted by the infixed expression %2x*%2y%1 since it is associative. We have the examples (A B C)*(D E F) = (A B C D E F), %1and NIL*(A B) = (A B) = (A B)*NIL, %1and the formal definition %2x*%2y ← %3if n %2x %3then %2y %3else [%3a %2x].[[%3d %2x]*%2y]. %1The Boolean operations can also be used in making recursive definitions provided we observe the order of evaluation of constituents. First, we define a predicate %2equal%1 by %2equal[x,y] ← x %3eq %2y ∨ [¬%3at %2x ∧ ¬%3at %2y ∧ equal[%3a %2x,%3a %2y] ∧ equal[%3d %2x, %3d %2y]]%1. %2equal[x,y]%1 is true if and only if %2x%1 and %2y%1 are the same S-expression, and the use of this predicate makes up for the fact that the basic predicate %3eq%1 is guaranteed to test equality only when one of the operands is known to be an atom. We shall also use the infixes =%1 and ≠%1. Membership of an S-expression %2x%1 in a list %2y%1 is tested by %2member[%2x, y] ← ¬%3n %2y ∧ [[%2x = %3a %2y] ∨ %2member[%2x, %3d %2y]]. %1This relation is also denoted by %2x_ε_y%1. Her? are some computations: .NOFILL %2member[B, (A B)] = ¬%3n (A B) ∧ [[B = %3a (A B)] ∨ %2member[B, %3d (A B)]], = %2member[B, (B)] = T. .FILL %1Sometimes a function is defined with the help of auxiliary functions. Thus, the reverse of a list %2x%1 , (e.g. %2reverse[(A B C D)] = (D C B A)%1), is given by .NOFILL %2reverse[%2x] ← %2rev[%2x, NIL] %1where %2rev[%2x, y] ← %3if n %2x %3then %2y %3else %2rev[%3d %2x, [%3a %2x].%2y]. %1A computation is %2reverse[(A B C)] = %2rev[(A B C), NIL] = %2rev[(B C), (A)] = %2rev[(C), (B A)] = %2rev[NIL, (C B A)] = (C B A). %1A more elaborate example of recursive definition is given by %2flatten[%2x] ← %2flat[%2x, NIL] %2flat[%2x, y] ← %3if at %2x %3then %2x.y %3else %2flat[%3a %2x, flat[%3d %2x, y]]. %1We have %2flatten[((A.B).C)] = %2flat[((A.B).C), NIL] = %2flat[(A.B), %2flat[C, NIL]] = %2flat[(A.B), (C)] = %2flat[A, %2flat[B, (C)]] = %2flat[A, (B C)] = (A B C). .FILL %1The reader will see that the value of %2flatten[%2x]%1 is a list of the atoms of the S-expression %2x%1 from left to write. Thus %2flatten[((A B) A)] = (A B NIL A NIL)%1. Many functions can be conveniently written in more than one way. For example, the function %2reverse%1 mentioned above can be written without an auxiliary function as follows: %2reverse[%2x] ← %3if n %2x %3then NIL %3else %2reverse[%3d %2x]*<a x> %1but it will be explained later that the earlier definition involves less computation. The use of conditional expressions for recursive function definition is not limited to functions of S-expressions. For example, the factorial function and the Euclidean algorithm for the greatest common divisor are expressed as follows: .NOFILL %2n! ← %3if %2n=0 %3then 1 %3else %2n(%2n-1)! %1and %2gcd(%2m, n) ← %3if %2m>%2n %3then %2gcd(%2n, m) %3else if %2m=0 %3then %2n %3else %2gcd(%2n mod m, m) .FILL %1where %2n mod m%1 denotes the remainder when %2n%1 is divided by %2m%1 and may itself be expressed recursively by %2n mod m ← %3if %2n<%2m %3then %2n %3else (%2n-%2m) %2mod m.%1 The internal form of function definitions depends on the implementation. Stanford LISP and UCI LISP for the PDP-10 computer use the form (DE <function name> <list of variables> <right hand side>)%1. In these LISPs, the above definition of %2subst%1 is (DE SUBST (X Y Z) (COND ((ATOM Z) (COND ((EQ Z X) Y) (T Z))) (T (CONS (SUBST X Y (CAR Z)) (SUBST X Y (CDR Z))))))%1, and the definition of %2alt%1 is (DE ALT (X) (COND ((OR (NULL X) (NULL (CDR X))) X) (T (CONS (CAR X) (ALT (CDDR X))))))%1. Another notation for function definition called the DEFPROP%1 notation will be explained after λ-expressions have been introduced. %1 Exercises 1. Consider the function %2drop%1 defined by %2drop[%2x] ← %3if n %2x %3then NIL %3else <%3a %2x>.%2drop[%3d %2x]. %1Compute (by hand) %2drop[(A B C)]%1. What does %2drop%1 do to lists in general? Write %2drop%1 in internal notation using DE%1. 2. What does the function %2r2[%2x] ← %3if n %2x %3then NIL %3else %2reverse[%3a %2x].%2r2[%3d %2x] %1do to lists of lists? How about %2r3[%2x] ← %3if at %2x %3then %2x %3else %2reverse[%2r4[%2x]] %2r4[%2x] ← %3if n %2x %3then NIL %3else %2r3[%3a %2x].%2r4[%3d %2x]? %13. Compare %2r3'[%2x] ← %3if at %2x %3then %2x %3else %2r3'[%3d %2x]*<%2r3'[%3a %2x]> %1with the function %2r3%1 of the preceding example. 4. Consider %2r5%1 defined by .NOFILL %2r5[%2x] ← %3if n %2x ∨ %3n d %2x %3then %2x %3else [%3a %2r5[%3d %2x]] . %2r5[%3a %2x . r5[%3d %2r5[%3d %2x]]]. .FILL %1Compute %2r5[(A B C D)]%1. What does r5%1 do in general? Needless to say, this is not a good way of computing this function even though it involves no auxiliary functions. .ss Lambda expressions and functions with functions as arguments. .once turn on "↑"; It is common to use phrases like "the function 2%2x+%2y%1". This is not a precise notation because we cannot say 2%2x+%2y(3, 4)%1 and know whether the desired result is 2↑.3+4 or 2↑.4+3 regarding the expression as a function of two variables. Worse yet, we might have meant a one-variable function of %2x%1 wherein %2y%1 is regarded as a parameter. The problem of giving names to functions is solved by Church's λ-notation. In the above example, we would write λ%2x y: 2%2x+%2y%1 to denote the function of two variables with first argument %2x%1 and second argument %2y%1 whose value is given by the expression 2%2x+%2y%1. Thus, [λ%2x y: 2%2x+%2y][3, 4] = 10%1. %1Likewise, [λ%2y x: 2%2x+%2y][3, 4] = 11%1. Like variables of integration and the bound variables of quantifiers in logic, variables following λ are bound or dummy and the expression as a whole may be replaced by any others provided the replacement is done consistently and does not make any variable bound by λ the same as a free variable in the expression. Thus λ%2x y: 2%2x+%2y%1 represents the same function as λ%2y x: 2%2y+%2x%1 or λ%2u v: 2%2u+%2v%1 , but in the function of one argument λ%2x: 2%2x+%2y%1 , we cannot replace the variable %2x%1 by %2y%1 , though we could replace it by %2u%1. λ-notation plays two important roles in LISP. First, it allows us to rewrite an expression containing two or more occurrences of the same sub-expression in such a way that the expression occurs only once. Thus (2%2x+1)%64+3(2%2x+1)%63%1 can be written [λ%2w: %2w%64+3%2w%63][2%2x+1]%1. This can save considerable computation, and corresponds to the practice in ordinary programming of assigning to a variable the value of a sub-expression that occurs more than once in an expression and then writing the expression in terms of the variable. The second use of λ-expressions is in using functions that take functions as arguments. Suppose we want to form a new list from an old one by applying a function %2f%1 to each element of the list. This can be done using the function %2mapcar%1 defined by %2mapcar[%2x, f] ← %3if n %2x %3then NIL %3else %2f[%3a %2x] . %2mapcar[%3d %2x, f]. %1Suppose the operation we want to perform is squaring, and we want to apply it to the list (1 2 3 4 5 6 7)%1. We have %2mapcar[(1 2 3 4 5 6 7), λ%2x: %2x%62] = (1 4 9 16 25 36 49). %1A more generally useful operation than %2mapcar%1 is %2maplist%1 in which the function is applied to the successive sublists of the list rather than to the elements. %2maplist%1 is defined by %2maplist[%2x, f] ← %3if n %2x %3then NIL %3else %2f[%2x] . %2maplist[%3d %2x, f]. %1As an application of %2maplist%1 and functional arguments, we shall define a function for differentiating algebraic expressions involving sums and products. The expressions are built up from atoms denoting variables and integer constants according to the syntax .NOFILL <expression> ::= <variable> | <integer> | (PLUS <explist>) | (TIMES <explist>) <explist> ::= <expression> | <expression><explist> .FILL Here, PLUS%1 followed by a list of arguments denotes the sum of these arguments and TIMES%1 followed by a list of arguments denotes their product. The function %2diff[%2e, v]%1 gives the partial derivative of the expression %2e%1 with respect to the variable %2v%1. We have .NOFILL %2diff[%2e, v] ← %3if at %2e %3then [%3if %2e %3eq %2v %3then 1 %3else 0] %3else if a %2e %3eq PLUS %3then PLUS . %2mapcar[%3d %2e, λ%2x: %2diff[%2x, v]_] %3else if a %2e %3eq TIMES %2then PLUS.%2maplist[%3d %2e, λ%2x: TIMES . %2maplist[%3d %2e, λ%2y: %3if %2x %3eq %2y %3then %2diff[%3a %2y, v] %3else a %2y]]. .FILL %1The term that describes the rule for differentiating products corresponds to the rule .NOFILL .COMMENT ******************************************!!!!!!!!!!!!********** . The formula below must be filled in by hand as follows: . PI SIGMA PI (i.e. the corrseponding capital greek . i i j letters and the lowercase subscripts . ↓ ↓ ↓ in the places indicated by the arrows) .; .COMMENT ******************************************!!!!!!!!!!!!********** . ∂/∂%2v %2e%5i%1 = [%3if %2i=%2j %3then ∂%2e%5j/∂%2v %3else %2e%5j]. .; .FILL and %2maplist%1 has to be used rather than %2mapcar%1 since whether to differentiate in forming the product is determined by equality of the indices %2i%1 and %2j%1 rather than equality of the terms %2e%5i%1 and %2e%5j%1. Two more useful functions with functions as arguments are the predicates %2andlis%1 and %2orlis%1 defined by the equations %2andlis[%2u, p] ← %3n %2u ∨ [%2p[%3a %2u] ∧ %2andlis[%3d %2u, p]] %1and %2orlis[%2u, p] ← ¬%3n %2u ∧ [%2p[%3a %2u] ∨ %2orlis[%3d %2u, p]]. The internal form for a λ-expression is (LAMBDA <list of variables> <expression to be evaluated>)%1. Thus λ x: diff[x,v]%1 is written (LAMBDA (X V) (DIFF X V))%1. When a function specified with λ is written as an argument of a function taking a functional argument, then the λ-expression is marked with the identifier FUNCTION%1. Thus the above definition of %2diff%1 translates to .NOFILL (DE DIFF (E V) (COND ((ATOM E) (COND ((EQ E V) 1) (T 0))) ((EQ (CAR E) (QUOTE PLUS)) .FILL (CONS (QUOTE PLUS) (MAPCAR (CDR E) (FUNCTION (LAMBDA (X) (DIFF X V)))))) .NOFILL .FILL ((EQ (CAR E) (QUOTE TIMES)) (CONS (QUOTE PLUS) (MAPLIST (CDR E) (FUNCTION (LAMBDA (X) (CONS (QUOTE TIMES) (MAPLIS (CDR E) (FUNCTION (LAMBDA (Y) (COND ((EQ X Y) (DIFF (CAR Y) V)) (T (CAR Y))))))))))))))%1. Another way of writing function definitions in internal notation uses LAMBDA%1 to make a function of the right side of a definition. It is like writing %2subst%1 and %2alt%1 as %2subst = λx y z.[%3if at %2z %3then %2[%3if %2z %3eq%2 y %3then%2 x %3else %2z] %3else %2subst[x,y,%3a%2 z] . subst[x,y,%3d%2 z]]%1 and %2alt = λx.[%3if n %2x ∨ %3n d %2x %3then%2 x %3else a %2x .alt %3dd%2 x]%1. The definitions of %2subst%1 and %2alt%1 take the forms (DEFPROP SUBST (LAMBDA (X Y Z) (COND ((ATOM Z) (COND ((EQ Z X) Y) (T Z))) (T (CONS (SUBST X Y (CAR Z)) (SUBST X Y (CDR Z)))))))%1, and (DEFPROP ALT (LAMBDA (X) (COND ((OR (NULL X) (NULL (CDR X))) X) (T (CONS (CAR X) (ALT (CDDR X)))))))%1. The general form is (DEFPROP <function name> <defining λ-expression>)%1 and is often used by programs that output LISP. .if lines < 8 then skip to column 1 %1 Exercises 1. Compute %2diff[(TIMES X (PLUS Y 1) 3), X]%1 using the above definition of %2diff%1. Now do you see why algebraic simplification is important? 2. Compute %2orlis[((A B) (C D) E), %3at]%1. .ss Label. The λ mechanism is not adequate for providing names for recursive functions, because in this case there has to be a way of referring to the function name within the function. Therefore, we use the notation %3label[%2f, e]%1 to denote the expression %2e%1 but where occurrences of %2f%1 within %2e%1 refer to the whole expression. For example, suppose we wished to define a function that takes alternate elements of each element of a list and makes a list of these. Thus, we want %2glub[((A B C) (A B C D) (X Y Z))] = ((A C) (A C) (X Z)).%1 We can make the definition %2glub[%2x] ← %2mapcar[%2x, %3label[%2alt, λ%2x: %3if n %2x ∨ %3n d %2x %3then %2x %3else a %2x . alt[%3dd %2x]]]. The internal form of %2label[<name>,<function expression>]%1 is (LABEL <name> <function expression>)%1, so that the internal form of the definition of %2glub%1 is (DE GLUB (X) (MAPCAR X (LABEL ALT (LAMBDA (X) (COND (OR (NULL X) (NULL (CDR X))) X) (T (CONS (CAR X) (ALT (CDDR X))))))))%1. The identifier %2alt%1 in the above example is bound by the label and is local to that expression, and this is the general rule. The label construction is not often used in LISP since it is more usual to give functions global definitions. D. M. R. Park pointed out that if we allow variables to represent functions and use a suitable λ construction, the use of label could be avoided. .ss Numerical computation. Numerical calculation and symbolic calculation must often be combined, so LISP provides for numerical computation also. In the first place, we need to include numbers as parts of symbolic expressions. LISP has both integer and floating point numbers which are regarded as atoms. These numbers may be included as atoms in writing S-expressions. Thus we can have the lists (1 3 5)%1, (3.5 6.1 -7.2E9)%1, and (PLUS X 1.3)%1; the first is a list of integers, the second a list of floating point numbers, and the third a symbolic list containing both numberical and non-numerical atoms. Integers are written without decimal points which are used to signal floating point numbers. As in Fortran, the letter E%1 is used to signal the exponent of a floating point number which is a signed integer. The sizes of numbers admitted depends on the implementation. When a dotted pair, say (1 . 2)%1 is wanted, the spaces around the dot distinguish it from the list (1.2)%1 whose sole element is the floating point number 1.2. In publication language we will use ordinary mathematical notation for numerical functions. For exponentiation we will use the usual superscript notation %2x%6y%1 when typographically convenient and the linear Algol notation %2x↑y%1 when it isn't. Of course, numerical and symbolic calculation must often be combined, so that the function giving the length of a list can be written %2length u ← %3if n %2u %3then 0 %3else 1 %2+ length %3d %2u%1. The internal notation for numerical functions is that used in the examples given: (PLUS X Y ... Z)%1 for %2x+y+...+z%1, (TIMES X ... Z)%1 for %2xy...z%1, (MINUS X)%1 for %2-x%1, (DIFFERENCE X Y)%1 for %2x-y%1, (QUOTIENT X Y)%1 for %2x/y%1, and (POWER X Y)%1 for %2x%6y%1. Since numbers that form part of list structures must be represented by pointers anyway, there is room for a flag distinguishing floating point numbers and integers. Therefore, the arithmetic operations are programmed to treat types dynamically, i.e. a variable may take an integer value at one step of computation and a real value at another. The subroutines realizing the arithmetic functions make the appropriate tests and create results of appropriate types. This is slow compared to direct use of the machine's arithmetic instructions, so that LISP can be efficiently used only when the numerical calculations are small or at least small compared to the symbolic calculations in a problem. Besides functions of numbers we need predicates on numbers and the usual =, <, >, ≤, and ≥ are used with the internal names EQUAL, LESSP, GREATERP, LESSEQP%1, and GREATEREQP%1, respectively. Not all are implemented in all LISP systems, but of course the remaining ones can be defined. Besides that, the predicate %2numberp%1 is used to distinguish numbers from other atoms. It is worth remarking that including type flags in numbers would benefit many programming languages besides LISP and would not cost much in either storage or hardware. As a first example of a combined numeric and symbolic computation, here is an interpreter for expressions with sums and products. Assume that the values of variables are given in an %2association list%1, having the form (<variable1>.<value1>) ... (<variablen>.<valuen>)), e.g. ((X . 5) (Y . 9.3) (Z . 2.1))%1. The function is %2numval[e,a] ← %3if %2numberp e %3then %2e %3else if at %2e %3then d %2assoc[e,a] %3else if a %2e %3eq PLUS %3then %2evplus[%3d %2e,a] %3else if a %2e %3eq TIMES %3then %2evtimes[%3d %2e,a]%1 where %2evplus[u,a] ← %3if n %2u %3 then 0 %3else %2numval[%3a %2u,a] + evplus[%3d %2u,a]%1, %2evtimes[u,a] ← %3if n %2u %3 then 1 %3else %2numval[%3a %2u,a] + evtimes[%3d %2u,a]%1, and %2assoc[x,a] ← %3if n %2a %3 then NIL %3else if aa %2a %3eq %2x %3then da %2a %3else %2assoc[x,%3d %2a]%1. .s HOW TO WRITE RECURSIVE FUNCTION DEFINITIONS .ss Static and dynamic ways of programming. In order to write recursive function definitions, one must think about programming differently than is customary when writing programs in languages like Fortran or Algol or in machine language. In these languages, one has in mind the state of the computation as represented by the values of certain variables or locations in the memory of the machine, and then one writes statements or machine instructions in order to make the state change in an appropriate way. When writing LISP recursive functions one thinks differently. Namely, one thinks about the value of the function, asks for what values of the arguments the value of the function is immediate, and, given an arbitrary values of the arguments, for what simpler arguments must the function be known in order to give the value of the function for the given arguments. Let us take a numerical example; namely, suppose we want to compute the function %2n!%1. For what argument is the value of the function immediate. Clearly, for %2n = 0 or %2n = 1%1, the value is immediately seen to be 1. Moreover, we can get the value for an arbitrary %2n%* if we know the value for %2n-1. Also, we see that knowing the value for %2n = 1 is redundant, since it can be obtained from the %2n = 0 case by the same rule as gets it for a general %2n%* from the value for %2n-1%1. All this talk leads to the simple recursive formula: %2n! ← %3if %2n = 0 %3then 1 %3else %2n(%2n-1)!. %1We may regard this as a static way of looking at programming. We ask what simpler cases the general case of our function depends on rather than how we build up the desired state of the computation. One often is led to believe that static = bad and dynamic = good, but in this case, the static way is often better than the dynamic way. Perhaps this distinction is equivalent to what some people call the distinction between %2top-down%1 and %2bottom-up%1 programming with %2static%1 corresponding to %2top-down%1. LISP offers both, but the static style is better developed in LISP, and we will emphasize it. .if lines < 10 then skip to column 1 Compare the above recursive definition with the following obvious Algol program for computing %2n!: .NOFILL %3integer procedure %2factorial(%2n); %3integer %2s; %3begin %2s := 1; %2loop: %3if %2n = 0 %3then go to %2done; %2s := %2n*%2s; %2n := %2n-1; %3go to %2loop; %2done: %2factorial := %2s; %3end; .FILL %1The LISP program is shorter and clearer in this particularly favorable case. Actually, when we discuss the mechanism of recursion, it will turn out that the LISP program will be inefficient in using the pushdown mechanism unnecessarily and should be replaced by the following somewhat longer program that corresponds to the above Algol program rather precisely: %2n! ← %2fact(%2n, %2s), %1where %2fact(%2n, %2s) ← %3if %2n = 0 %3then %2s %3else %2fact(%2n-1, %2n*%2s). %1In fact, compilers should produce the same object code from the two programs. .ss Simple list recursion. About the simplest form of recursion in LISP occurs when one of the arguments is a list, the result is immediate when the argument is null, and otherwise we need only know the result for the %3d%*-part of that argument. Consider, for example, %2u*%2v%1, the result of %2append%1ing the list %2v%1 to the list %2u%1. The result is immediate for the case %3n %2u%1 and otherwise depends on the result for %3d %2u%1. Thus, we have %2u*%2v ← %3if n %2u %3then %2v %3else a %2u . [%3d %2u * %2v]. %1On the other hand, if we had tried to recur on %2v%1 rather than on %2u%1 we would not have been successful. The result would be immediate for %3n %2v%1, but %2u*%2v%1 cannot be constructed in any direct way from %2u*%3d %2v%1 without a function that puts an element onto the end of a list. (From a strictly list point of view, such a function would be as elementary as %2cons%1 which puts an element onto the front of a list, but, when we consider the implementation of lists by list structures, we see that the function is not so elementary. This has led some people to construct systems in which lists are bi-directional, but, in the main, this has turned out to be a bad idea). Anyway, it is usually easier to recur on one argument of a function than to recur on the other. The %2append%1 function machine coded in most Lisp systems in a way that allows an arbitrary number of arguments, e.g. (APPEND (QUOTE (A B)) (QUOTE (C D)) (QUOTE (E F))) is (A B C D E F). It is often necessary to represent a correspondence between the elements of a small set of atoms and certain S-expressions by a list structure. This is conveniently done by means of an association list which is a list of pairs, each pair consisting of an atom and the corresponding S-expression. Thus the association list ((X . (PLUS A B)) (Y . C) (Z . (TIMES U V)), %1which would print as ((X PLUS A B)) (Y . C) (Z TIMES U V)), %1pairs X%1 with (PLUS A B), Y%1 with C%1, etc. We need a function to tell whether anything is associated with the atom %2x%1 in the association list %2a%1, and, if so, to tell us what. We have .NOFILL %2assoc[%2x, a] ← %3if n %2a %3then NIL %3else if %2x %3eq aa %2a %3then a %2a%3else %2assoc[%2x, %3d %2a]. .FILL %1Its value is NIL%1 if nothing is associated with %2x%1 and the association pair otherwise. E.g. %2assoc[X, ((X.W) (Y.V))] = (X.W)%1. %2assoc%1 is also built in to most Lisp systems. It commonly happens that a function has no simple recursion, but there is a simple recursion for a function with one more variable that reduces to the desired function when the extra variable is set to NIL%1. Thus %2reverse[%2u] ← %2rev1[%2x, NIL], %1where %2rev1[%2u, v] ← %3if n %2u %3then %2v %3else %2rev1[%3d %2u, %3a %2u . v]. %2reverse%1 has a direct recursive definition as discovered by S. Ness, but no-one would want to use the following in actual computation nor does it generate much understanding, only appreciation of Mr. Ness's ingenuity: .NOFILL %2reverse[%2u] ← %3if n %2u ∨ %3n d %2u %3then %2u %3else a %2reverse[%3d %2u] . %2reverse[%3a %2u. %2reverse[%3d %2reverse[%3d %2u]]]. %1 .FILL Exercises 1. Using the function %2member[%2x, u]%1 defined in Chapter I which may also be written %2x ε %2u%1, write function definitions for the union %2u ∪ %2v%1 of lists %2u%1 and %2v%1, the intersection %2u ∩ %2v%1, and the set difference %2u-%2v%1. What is wanted should be clear from the examples: (A B C) ∪ (B C D) = (A B C D), (A B C) ∩ (B C D) = (B C), %1and (A B C) - (B C D) = (A). %1Pay attention to getting correct the trivial cases in which some of the arguments are NIL%1. In general, it is important to understand clearly the trivial cases of functions. 2. Suppose %2x%1 takes numbers as values and %2u%1 takes as values lists of numbers in ascending order, e.g. (2 4 7)%1. Write a function %2merge[%2x, u]%1 whose value is obtained from that of %2u%1 by putting %2x%1 in %2u%1 in its proper place. Thus %2merge[3, (2 4)] = (2 3 4)%1, and %2merge[3, (2 3)] = (2 3 3)%1. 3. Write functions giving the union, intersection, and set difference of ordered lists; the result is wanted as an ordered list. Note that computing these functions of unordered lists takes a number of comparisons proportional to the square of the number of elements of a typical list, while for ordered lists, the number of comparisons is proportional to the number of elements. 4. Using %2merge%1, write a function %2sort%1 that transforms an unordered list into an ordered list. 5. Write a function %2goodsort%1 that sorts a list using a number of comparisons proportional to %2n log n%1, where %2n%1 is the length of the list to be sorted. .ss Simple S-expression recursion. In another class of problems, the value of the function is immediate for atomic symbols, and for non atoms depends only on the values for the a-part and the d-part of the argument. Thus %2subst%1 was defined by .NOFILL %2subst[%2x, y, z] ← %3if at %2z %3then [%3if %2z %3eq %2y %3then %2x %3else %2z] %3else %2subst[%2x, y, %3a %2z] . %2subst[%2x , y , %3d %2z]. .FILL %1Two other examples are %2equal%1 which gives the equality of S-expressions and %2flat%1 which spreads an S-expression into a list of atoms: They are defined by %2x=%2y ← %2x %3eq %2y ∨ [¬%3at %2x ∧ ¬%3at %2y ∧ %3a %2x = %3a %2y ∧ %3d %2x = %3d %2y], %1and %2flat[%2x] ← %2flata[%2x, NIL] %1where %2flata[x,u] ← %3if at %2x %3then %2x.y %3else %2flata[%3a %2x,flata[%3d %2x,y]]%1. The kind of double recursion used in %2flat%1 is often useful. %2flat%1 could also be written %2flat x ← %3if at %2 x %3then%2 <x> %3then%2 flat %3a%2 x * flat %3d%2 x, which is a bit easier to follow although less efficient, because the %2append%1 function copies unnecessarily. .if lines < 7 then skip to column 1 EXERCISES 1. Write a predicate to tell whether a given atom occurs in a given S-expression, e.g. %2occur[B, ((A.B).C)] = T%1. 2. Write a predicate to tell how many times a given atom occurs in an S-expression. 3. Write a function to make a list without duplications of the atoms occurring in an S-expression. 4. Write a function to make a list of all atoms that occur more than once in a given S-expression paired with their multiplicities. 5. Write a predicate to tell whether an S-expression has more than one occurrence of a given S-expression as a sub-expression. .ss Other structural recursions. When lists are used to represent algebraic expressions, functions of these algebraic expressions often have a recursive form closely related to the inductive definition of the expressions. Suppose, for example, that sums and products are represented respectively by the forms (PLUS X Y)%1 and (TIMES X Y)%1 and that the values of variables are given on an a-list. We can write a recursive formula for the value of an expression as follows: .NOFILL %2value[%2e, a] ← %3if at %2e %3then d %2assoc[%2e, a] %3else if a %2e %3eq PLUS %3then %2value[%3ad %2e, a] + %2value[%3add %2e, a] %3else if a %2e %3eq TIMES %3then %2value[%3ad %2e, a] * %2value[%3add %2e, a]. .FILL %1On the other hand, suppose that sums and products are not restricted to have just two arguments; then we must use auxiliary functions to define the value of an expression, as follows: .NOFILL %2value[%2e, a] ← %3if at %2e %3then d %2assoc[%2e, a] %3else if a %2e %3eq PLUS %3then %2vplus[%3d %2e, a] %3else if a %2e %3eq TIMES %3then %2vtimes[%3d %2e, a]. %1where %2vplus[%2u, a] ← %3if n %2u %3then 0 %3else %2value[%3a %2u, a] + %2vplus[%3d %2u, a], %1and %2vtimes[%2u, a] ← %3if n %2u %3then 1 %3else %2value[%3a %2u, a] * %2vtimes[%3d %2u, a]. .FILL %1In both cases, the recursion form is related to the structure of the algebraic expressions more closely than to the structure of S-expressions or lists. .ss Tree search recursion. .FILL We begin with a general depth first tree search function. It can be used to search specific trees of possibilities by defining three auxiliary functions in a way that depends on the application. We have %2search p ← qif lose p qthen %1LOSE%2 qelse qif ter p qthen p qelse searchlis[successors p]%1 where %2searchlis u ← qif qn u qthen %1LOSE%2 qelse {search qa u}[λx: qif x = %1LOSE%2 qthen searchlis qd u qelse x]%1. In the applications, we start with a position %2p%40%1, and we are looking for a win in the successor tree of %2p%40%1. Certain positions lose and there is no point looking at their successors. This is decided by the predicate %2lose%1. A position is a win if it doesn't lose and it satisfies the predicate %2ter%1. The successors of a position is given by the function %2successors%1, and the value of %2search p%1 is the winning position. No non-losing position should have the name LOSE or the function won't work properly. Simple S-expression recursion can be regarded as a special case of depth first recursion. It is special in that there exactly two branches, but even more important, the tree is the tree of parts of the S-expression and is present at the beginning of the calculation. In case of tree search recursion, the tree is generated by the %2successors%1 function. Our first application is finding a path from an initial node to a final node in a graph represented by a list structure as described in chapter I. A position is a path starting from the initial node and continuing to some intermediate node and is represented by a list of its nodes in reverse order. The three functions for this application are %2lose p ← %3a %2p ε %3d %2p, ter p ← [%3a %2p = final],%1 and %2successors p ← mapcar[qd assoc[qa p, graph], λx: x . p]%1. Another example is the so-called %2Instant Insanity%1 puzzle. There are four cubical blocks, and each face of each block is colored with one of four colors. The object of the puzzle is to build a tower of all four blocks such that each vertical face of the tower involves all four colors. In order to use the above defined function %2search%1 for this purpose, we must define the representation of positions and give the functions %2lose, ter, %1and %2successors%1. A position is represented by a list of lists ¬ one for each face of the tower. Each sublist is the list of colors of the faces of the blocks showing in that face. We shall assume that the blocks are described in the following longwinded but convenient way. (We'll take up precomputing this description later.) For each block there is a list of the 24 orientations of the block where each orientation is described as a list of the colors around the vertical faces of the block when it is in that orientation. Thus the puzzle is described by a list of lists of lists which we shall call %2puzz%1. We now have %2p%40%1 = (NIL NIL NIL NIL), %2lose p ← orlis[p, λu: qa u ε qd u]%1, %2ter p ← [length qa p = 4]%1, and %2successors p ← mapcar[qa nth[puzz, 1 + length qa p], λx: mapcar2[p, x, λyz: z.y]]%1, where %2mapcar2[u, v, f] ← qif qn u qthen qNIL qelse f[qa u, qa v] . mapcar2[qd u, qd v, f]%1. Getting the initial position in the desired form is as complicated a computation as the actual tree search. It can be conveniently done by a sequence of assignment statements starting with a description of the blocks: %2puzz1 ← %1((G B B W R G) (G G B G W R) (G W W R B R) (G G R B W W)). Here each block is represented by a list of the colors of the faces starting with the top face, going around the sides in a clockwise direction and finishing with the bottom face. We need to go from this description of the blocks to a list of the possible cycles of colors on the vertical faces for the 24 orientations of the block. This not easy, because the order in which we have given the colors is not invariant under rotations of the block. An easy way out is to start with a block whose faces are assigned the numbers 1 thru 6 starting with the top, going clockwise around the sides and finishing with the bottom. We write down one cycle of side colors for each choice of the face put on top and get the list of all 24 cycles by appending the results of generating the cyclic permutations of the cycles. All this is accomplished by the assignment. %2puzz2 ← cycles[(2 3 4 5)] * cycles[(2 5 4 3)] * cycles[(1 2 6 4)] * cycles[(1 4 6 2)] * cycles[(1 3 6 5)] * cycles[(1 5 6 3)]%1, where the function %2cycles%1 is defined by %2cycles u ← maplist[u, λx: x * upto[u, x]]%1 with the auxiliary function %2upto[u, x] ← qif x qeq u qthen qNIL qelse qa u . upto[qd u, x]%1. Next we create for each block a list of substitutions expressing the colors of the six numbered faces. We have %2puzz3 ← mapcar[puzz1, λx: prup[(1 2 3 4 5 6), x]]%1, and we use these substitutions to get for each block the list of 24 orientations of the block. Thus %2puzz4 ← mapcar[puzz3, λs: sublis[s, puzz3]]%1. %2puzz4%1 has all 24 orientations of the first block while for symmetry reasons we need only consider three as distinct, say the first, ninth, and seventeenth. So we finally get %2puzz ← <qa nth[qa puzz4, 1], qa nth[qa puzz4, 9], qa nth[qa puzz4, 17]> . qd puzz4.%1 The program when compiled runs about 11 seconds on the KA-10. A more sophisticated representation of face cycles and partial towers makes a factor of ten speedup without changing the basic search algorithm. A face cycle is represented by 16 bits in a word four for each face a particular one of which being turned on tells us the color of the face. If we %3or%1 these words together for the blocks in a partial tower we get a word which tells us for each face of the tower what colors have been used. A particular face cycle from the next block can be added to the tower if the %3and%1 of its word with the word representing the tower is zero. We represent a position by a list of words representing its partial towers with 0 as the last element and the highest partial tower as the first element. The virtue of this representation is that it makes the description of the algorithm short. The initial position is (0). The new %2puzz%1 can be formed from the old one by the assignment %2puzza ← mapcar[puzz, λx: mapcar[x, zap]], %1 where %2zap v ← qif qn v qthen 0 qelse poo qa v + 16 * zap qd v%1. and %2poo x ← qif x = %1R%2 qthen 1 qelse if x = %1W%2 qthen 2 qelse qif x = %1G%2 qthen 4 qelse 8%1. Now we need the new functions %2lose, ter, %1and %2successors%1. These are %2lose p ← %3false%2, %2ter p ← [length p = 5], %1 and %2successors p ← mapchoose[qa nth[puzza, length p], λx: qa p %3and%2 x = 0, λx: [qa p %3or%2 x] . p].%1 where %2mapchoose[u, pred, fn] ← qif qn u qthen qNIL qelse qif pred qa u qthen fn[qa u] . mapchoose[qd u, pred, fn] qelse mapchoose[qd u, pred, fn].%1 %2lose%1 is trivial, because the %2mapchoose%1 is used to make sure that only non-losing new positions are generated by %2successors%1. This version runs in a little less than one second on the KA-10. A greater speedup can be made by the application of some mathematics. In fact, with enough mathematics, extensive tree search is unnecessary in this problem. %2search%1 is used when we want to search a tree of possibilities for a solution to a problem. Naturally we can do other things with tree search recursion than just search. For example we may want to find all solutions to a problem. This can be done with a function %2allsol%1 that uses the same %2lose, ter, %1and %2successors%1 functions as does %2search%1. The simplest way to write %2allsol%1 is %2allsol p ← qif lose p qthen qNIL qelse qif ter p qthen <p> qelse mapapp[successors p, allsol]%1, where %2mapapp[u, fn] ← qif qn u qthen qNIL qelse fn[qa u] . mappap[qd u, fn]%1. This form of the function is somewhat inefficient because of all the %2append%1ing. A more efficient form uses an auxiliary function as follows: %2allsol p ← allsola[p, qNIL] allsola[p, found] ← qif lose p qthen found qelse qif ter p qthen p . found qelse allsolb[successors p, found]%1, %2allsolb[u, found] ← qif qn u qthen found qelse allsolb[qd u, allsola[qa u, found]].%1 The recursive program structure that arises here is common when a list is to be formed by recurring through a list structure. .ss Game trees. .FILL The positions that can be reached from an initial position in a game form a tree, and deciding what move to make often involves searching this tree. However, game trees are searched in a different way than the trees we have looked at, because the opposing interests of the players makes it not a search for a joint line of play that will lead to the first player winning, but rather a search for a strategy that will lead to a win regardless of what the other player does. The simplest situation is characterized by a function %2successors%1 that gives the positions that can be reached in one move, a predicate %2ter%1 that tells when a position is to be regarded as terminal for the given analysis, and a function %2imval%1 that gives a number approximating the value of the position to one of the players. We shall call this player the maximizing player and his opponent the minimizing player. Usually, the numerical values arise, because the search cannot be carried out to the end of the game, and the analysis stops with reasonably static positions that can be evaluated by some rule. Naturally, the function %2imval%1 is chosen to be easy to calculate and to correlate well with the probability that the maximizing player can win the position. The simplest rule for finding the correct move in a position uses auxiliary functions %2valmax%1 and %2valmin%1 that give a value to a position by using %2imval%1 if the position is terminal and taking the max or min of the successor positions otherwise. For this we want functions for getting the maximum or the minimum of a function on a list, and they are defined as follows: %2maxlis[u, f] ← %3if n %2u %3then %2-∞ %3else %2 max[f[%3a %2u], maxlis[%3d %2u, f]], %1 and %2minlis[u, f] ← %3if n %2u %3then %2∞ %3else %2 min[f[%3a %2u], minlis[%3d %2u, f]].%1 In these functions, -∞ and ∞ represent numbers that are smaller and larger than any actual values that will occur in evaluating %2f%1. If these numbers are not available, then it is necessary to prime the function with the values of %2f%1 applied to the first element of the list, and the functions are meaningless for null lists. Iterative versions of the functions are generally better; we give only the iterative version of %2maxlis%1, namely %2maxlis[u, f] ← maxlisa[u, -∞, f], %1 where %2maxlisa[u, x, f] ← %2if n %2u %3then %2x %3else %2maxlisa[%3d %2u, max[x, f[%3a %2u]], f].%1 We now have %2valmax p ← %3if %2ter p %3then %2imval p %3else %2maxlis[successors p, valmin]%1, and %2valmin p ← %3if %2ter p %3then %2imval p %3else %2minlis[successors p, valmax]%1. .NOFILL The best move is now chosen by %2movemax p ← bestmax[succesors p, valmin], %1 or %2movemin p ← bestmin[succesors p, valmax], %1 where %2bestmax[u, f] ← bestmaxa[%3d %2u, %3a %2u, f[%3a %2u], f], %2bestmaxa[u, sofar, valsofar, f] ← %3if n %2u %3then %2sofar .FILL %3else if %2f[%3a %2u] ≤ %2bestsofar %3then %2bestmaxa[%3d %2u, sofar, bestsofar, f] .NOFILL %3else %2bestmaxa[%3d %2u, %3a %2u, f[%3a %2u], f], %2bestmin[u, f] ← bestmina[%3d %2u, %3a %2u, f[%3a %2u], f], %1 and %2bestmina[u, sofar, valsofar, f] ← %3if n %2u %3then %2sofar .FILL %3else if %2f[%3a %2u] ≥ %2bestsofar %3then %2bestmina[%3d %2u, sofar, bestsofar, f] .NOFILL %3else %2bestmina[%3d %2u, %3a %2u, f[%3a %2u], f].%1 .FILL However, this straight minimax computation of the best move does much more computation in general than is usually necessary. The simplest way to see this is from the move tree of Figure 2.6. .NOFILL .begin verbatim select d; .INDENT 32; ≤ 8 max ≤' .once superimpose 3; ' αααα 1 ≤≥ min ≤' `≥ ≤' ` 6 .once superimpose 2; ' ≥ `≥ ≤ 9 `≥ ≤' .once superimpose 3; `' αααα X ≥ `≥ ` X .END ↔%DFigure 2.6%1 .FILL We see from this figure that it is unnecessary to examine the moves marked x, because their values have no effect on the value of the game or on the correct move since the presence of the 9 is sufficient information at this point to show that the move leading to the vertex preceding it should not be chosen by the minimizing player. The general situation is that it is unnecessary to examine further moves in a position once a move is found that refutes moving to the position in the first place. This idea is called the αβ-heuristic and expressed in the following recursive definitions: %2maxval p ← maxval1[p, -∞, ∞], maxval1[p, α, β] ← %3if %2ter p %3then %2max[α, min[β, imval p]] %3else %2maxval2[successors p, α, β], maxval2[u, α, β] ← {minval1[%3a %2u, α, β]}[λw: %3if %2w = β %3then %2β %3else %2maxval2[%3d %2u, w, β]], %2minval p ← minval1[p, -∞, ∞], minval1[p, α, β] ← %3if %2ter p %3then %2max[α, min[β, imval p]] %3else %2minval2[successors p, α, β], minval2[u, α, β] ← {maxval1[%3a %2u, α, β]}[λw: %3if %2w = α %3then %2α %3else %2minval2[%3d %2u, α, w].%1 The reduction in number of positions examined given by the αβ algorithm over the simple minimax algorithm depends on the order in which the moves are examined. In the worst case, the moves happen to be examined in inverse order of merit in every position on the tree, i.e. the worst move first. In that case, there is no improvement over minimax. The best case is the one in which the best move in every position is examined first. If we look %2n%1 moves deep on a tree that has %2k%1 successors to each position, then minimax looks at %2k%6n%1 positions while αβ looks at about only %2k%6n/2%1. Thus a program that looks at 10%64%1 moves with αβ might have to look at 10%68%1 with minimax. For this reason, game playing programs using αβ make a big effort to include as good as possible an ordering of moves into the %2successors%1 function. When there is a deep tree search to be done, the way to make the ordering is with a short look-ahead to a much smaller depth than the main search. Still shorter look-aheads are used deeper in the tree, and beyond a certain depth, non-look-ahead ordering methods are of decreasing complexity. A version of αβ incorporating optimistic and pessimistic evaluations of positions was first proposed by McCarthy about 1958. Edwards and Hart at M.I.T. about 1959 proved that the present version of αβ works and calculated the improvement it gives over minimax. The first publication, however, was Brudno (1963). It is worth noting that αβ was not used in the early chess playing programs in spite of the fact that it is clearly used in any human play. Its non-use, therefore, represents a failure of self-observation. Very likely, there are a number of other algorithms used in human thought that we have not noticed an incorporated in our programs. To the extent that this is so, artificial intelligence will be %2a posteriori%1 obvious even though it is %2a priori%1 very difficult. .s COMPILING IN LISP .ss Introduction Compiling is an important example of symbolic computation and has received much study. Much of the study has been devoted to parsing which is essentially the transformation of an input string in the source language into an internal form. The internal form used depends on the compiler. Sometimes it is Polish prefix or postfix notation, sometimes it is list structure, and sometimes it consists of entries in a collection of tables. When internal notation LISP is being compiled, the parsing is trivial, because the input is S-expressions and the internal form wanted is list structure, so what parsing there is is done by the ordinary LISP %2read%1 routine. Therefore, compilers can be very compact and transparent in structure, and we can concentrate our attention on the code generation phase. This is as it should be, because, in my opinion, parsing is basically a side issue in compiling, and code generation is the matter of main scientific interest. We shall describe two compilers in this chapter called LCOM0 and LCOM4 which compile S-expression LISP into machine language for the PDP-10 computer according to the conventions of Stanford LISP 1.6. For now we shall take these conventions for granted. Before describing the compilers, we must describe these conventions. The target language is called LAP for LISP assembly program. Each function is compiled separately into a separate LAP program, and these programs are written onto a disk file. These files can later be read into a LISP core image and assembled in place by the LAP assembler which is part of the LISP runtime routines. The compiler, on the other hand, is a separate LISP core image that can be instructed to compile several input files. For an input file called <name>, it produces and output file called <name>.LAP. All this is specific to the PDP-10 time-sharing system and fortunately works the same whether the time-sharing system is the D.E.C. system, the Stanford system, or TENEX. The LAP program produced is a list of words; the last word is NIL, and the first word is a header of the form (LAP %2fname%1 SUBR) where %2fname%1 is the name of the function compiled. This header tells the DSKIN program that it should read S-expressions till it comes to NIL and then submit what it has collected to the LAP assembler which will assemble it into core. The rest of the words are either atoms representing labels or lists representing single PDP-10 instructions. .ss Some facts about the PDP-10. The following facts about the PDP-10 may be of use: The PDP-10 has a 36 bit word and an 18 bit address. In instructions and in accumulators used as index registers the address is found in the right part of the word where the least significant bits in arithmetic reside. There are 16 general registers which serve simultaneously as accumulators (receiving the results of arithmetic operations), index registers (modifying the nominal addresses of instructions to form effective addresses), and as the first 16 registers of memory (if the effective address of an instruction is less than 16, then the instruction uses the corresponding general register as its operand.) All instructions have the same format and are written for the LAP assembly program in the form (<op name> <accumulator> <address> <index register>). Thus _(MOVE 1 3 P)_ causes accumulator _1_ to receive the contents of a memory register whose address is _3+c(P), i.e. 3+<the contents of general register P>. If no index register is specified, then the address used is just <address>. If the op name is followed by _@, then the memory reference is indirect, i.e. the effective addrress is the contents of the right half of the word directly addressed by the instruction (modified by the index register and indirect bit of that word). In the following description of some instructions useful in constructing the compiler, <ef> denotes the effective address of an instruction. .BEGIN INDENT 8,30,8 .PREFACE 0 .AT 0 ⊂BREAK⊃ .AT 24 ⊂""⊃ .TURN ON "∂" .VARIABLE I .I ← 31 MOVE ∂(I)(ac) ← c(<ef>) MOVEI ∂(I)c(ac) ← <ef> MOVEM ∂(I)c(<ef>) ← c(ac) HLRZ ∂(I)right half of c(ac) ← left half of c(<ef>) HRRZ ∂(I)right half of c(ac) ← right half of c(<ef>) ∂(16)(These two are used indirectly for _car_ and _cdr_ respectively.) ADD ∂(I)c(ac) ← c(ac) + c(<ef>) SUB ∂(I)c(ac) ← c(ac) - c(<ef>) JRST ∂(I)go to <ef> JUMPE ∂(I)if c(ac) = 0 then go to <ef> JUMPN ∂(I)if c(ac) ≠ 0 then go to <ef> CAME ∂(I)if c(ac) = c(<ef>) then <skip next instruction> CAMN ∂(I)if c(ac) ≠ c(<ef>) then <skip next instruction> PUSH ∂(I)c(c(right half of ac)) ← c(<ef>); the contents of each half of ac is increased by one and if the contents of the left half is then _0, a stack overflow interrupt occurs. (PUSH P ac) is is used in LISP to put c(ac) on the stack. POP ∂(I)c(<ef>) ←c(c(right half of ac)); the contents of each half of ac are then decreased by 1. This may be used for removing the top element of the stack. Thus (POP P 1) puts the top element of the stack in accumulator 1. The i-th element of the stack is obtained by (MOVE@ 1 i P). POPJ ∂(I)(POPJ P) is used for returning from a subroutine .END These instructions are adequate for compiling basic LISP code with the addition of the subroutine calling pseudo-instrucion. (CALL %2n (E <subr) S) is used for calling the LISP subroutine <subr> with %2n%1 arguments. The convention is that the arguments will be stored in successive accumulators beginning with accumulator _1, and the result will be returned in accumulator _1. In particular the functions _ATOM_ and _CONS_ are called with _(CALL 1 (E ATOM) S)_ and (CALL 2 (E CONS) S) respectively, and programs produced by you compiler will be called similarly when their names are referred to. .ss Code produced by LISP compilers. We will discuss two compilers, a simple one called LCOM0 and a more optimising compiler called LCOM4. LCOM4 produces about half as many instructions for a given function as does LCOM0. Besides these, there is the standard PDP-10 LISP compiler written at M.I.T. by Richard Greenblatt and Stuart Nelson and modified by Whitfield Diffie. .SKIP TO LINE 1 .BEGIN VERBATIM SELECT 1 Examples of output of LCOM0, LCOM4, and the regular Lisp compiler For the file containing: (DEFPROP DROP (LAMBDA(X) (COND ((NULL X) NIL) (T (CONS (LIST (CAR X)) (DROP (CDR X)))))) EXPR) ****************************************************************** LCOM0 produces the following code: (LAP DROP SUBR) (PUSH P 1) (MOVE 1 0 P) (PUSH P 1) (MOVE 1 0 P) (SUB P (C 1 0 1 0)) (CALL 1 (E NULL) S) (JUMPE 1 G0163) (MOVEI 1 0) (JRST G0162) G0163 (MOVEI 1 (QUOTE T)) (JUMPE 1 G0164) (MOVE 1 0 P) (PUSH P 1) (MOVE 1 0 P) (SUB P (C 1 0 1 0)) (CALL 1 (E CAR) S) (PUSH P 1) (MOVE 1 0 P) (SUB P (C 1 0 1 0)) (CALL 1 (E LIST) S) (PUSH P 1) (MOVE 1 -1 P) (PUSH P 1) (MOVE 1 0 P) (SUB P (C 1 0 1 0)) (CALL 1 (E CDR) S) (PUSH P 1) (MOVE 1 0 P) (SUB P (C 1 0 1 0)) (CALL 1 (E DROP) S) (PUSH P 1) (MOVE 1 -1 P) (MOVE 2 0 P) (SUB P (C 2 0 2 0)) (CALL 2 (E CONS) S) (JRST G0162) G0164 G0162 (SUB P (C 1 0 1 0)) (POPJ P) NIL LCOM4 produces the following code: (LAP DROP SUBR) (PUSH P 1) (MOVE 1 0 P) (JUMPE 1 G0162) (HLRZ@ 1 0 P) (CALL 1 (E LIST) S) (PUSH P 1) (HRRZ@ 1 -1 P) (CALL 1 (E DROP) S) (MOVE 2 1) (MOVE 1 0 P) (SUB P (C 1 0 1 0)) (CALL 2 (E CONS) S) G0162 (SUB P (C 1 0 1 0)) (POPJ P) NIL ****************************************************************** The ILISP compiler produces the following code: (LAP DROP SUBR) (PUSH P 1) (JUMPE 1 TAG1) (HLRZ@ 1 0 P) (CALL 1 (E NCONS) S) (PUSH P 1) (HRRZ@ 1 -1 P) (CALL 1 (E DROP) S) (POP P 2) (CALL 2 (E XCONS) S) TAG1 (SUB P (C 1 0 1 0)) (POPJ P) NIL .END Note that all three compilers produce the same first line of heading. This is necessary for the LAP assembly program which also requires the _NIL_ at the end as punctuation. The standard compiler uses a function called _XCONS_ that has the same effect as CONS_ except that it receives its arguments in the reverse order which is sometimes convenient. This requires, of course, that the compiler be smart enough to decide where it is more convenient to put the arguments of the %2cons%1 function. My two compilers are similar in structure, but the better one, which is twice as long, uses the following optimisations. 1. When the argument of CAR or CDR is a variable, it compiles a (HLRZ@ 1 i P) or (HRRZ@ 1 i P) which gets the result through the stack without first compiling the argument into an accumulator. 2. When it has to set up the arguments of a function in the accumulators, in general, the program must compute the arguments one at a time and save them on the stack, and then load the accumulators from the stack. However, if one of the arguments is a variable, is a quoted expression, or can be obtained from a variable by a chain of _cars_ and _cdrs, then it need not be computed until the time of loading accumulators since it can be computed using only the accumulator in which it is wanted. 3. The Diffy compiler produces about 10 percent less code than LCOM4; the main difference seems to be that it sometimes notices when it has an expression that it will need later. Sometimes this feature leads it astray. For example, it may save _%3a %2u%1_ for later use at greater cost than re-computing it. It should further be noted that quoted S-expressions can be compiled with the instruction (MOVEI 1 (QUOTE α)). .ss Listings of LCOM0 and LCOM4 First are listings of both compilers in blackboard notation. Following these is an an annotated listing of LCOM0 in S-expression notation, and a listing of LCOM4 in that notation. .SKIP TO LINE 1 LCOM0: .REQUIRE "LC0.BB" SOURCE_FILE .SKIP TO LINE 1 LCOM4: .REQUIRE "LC4.BB" SOURCE_FILE .SKIP TO LINE 1 Annotated listing of LCOM0: .BEGIN VERBATIM SELECT 1 (DEFPROP LC0FNS (LC0FNS COMPL COMP PRUP MKPUSH COMPEXP COMPLIS LOADAC COMCOND COMBOOL COMPANDOR) VALUE) ~COMPL is the user-callable driver. It is a FEXPR. It takes as ~ an argument a single file name, which must have no extension. ~ EXPRs on a file called FILNAM will be compiled into LAP and ~ written on the file FILNAM.LAP. Other types of function ~ definitions and non-definitions are simply copied to output. (DEFPROP COMPL (LAMBDA(FILE) (PROG (Z) (EVAL (CONS (QUOTE OUTPUT) (CONS (QUOTE DSK:) (LIST (CONS (CAR FILE) (QUOTE LAP)))))) (EVAL (CONS (QUOTE INPUT) (CONS (QUOTE DSK:) FILE))) (INC T NIL) LOOP (SETQ Z (ERRSET (READ))) (COND ((ATOM Z) (GO DONE))) (SETQ Z (CAR Z)) (COND ((OR (EQ (CAR Z) (QUOTE DE)) (AND (EQ (CAR Z) (QUOTE DEFPROP)) (EQ (CADDDR Z) (QUOTE EXPR)))) (PROG (PROG) (SETQ PROG (COND ((EQ (CAR Z) (QUOTE DE)) (COMP (CADR Z) (CADDR Z) (CADDDR Z))) (T (COMP (CADR Z) (CADR (CADDR Z)) (CADDR (CADDR Z)))))) (OUTC T NIL) (MAPC (FUNCTION PRINT) PROG) (OUTC NIL NIL) (PRINT (LIST (CADR Z) (LENGTH PROG))))) (T (OUTC T NIL) (PRINT Z) (OUTC NIL NIL))) (GO LOOP) DONE (OUTC T NIL) (OUTC NIL T) (INC NIL T) (RETURN (QUOTE ENDCOMP)))) FEXPR) ~COMP compiles a single function definition, returning a list of ~ the LAP code corresponding to the definition. ~ FN is the atomic name of the function being compiled. ~ VARS is the formal parameter list for the function. ~ EXP is the function body. (DEFPROP COMP (LAMBDA(FN VARS EXP) ((LAMBDA(N) (APPEND (LIST (LIST (QUOTE LAP) FN (QUOTE SUBR))) (MKPUSH N 1) (COMPEXP EXP (MINUS N) (PRUP VARS 1)) (LIST (LIST (QUOTE SUB) (QUOTE P) (LIST (QUOTE C) N 0 N 0))) (QUOTE ((POPJ P) NIL)))) (LENGTH VARS))) EXPR) ~PRUP returns an A-LIST formed by pairing successive elements of ~ VARS with consecutive integers beginning with N. (DEFPROP PRUP (LAMBDA(VARS N) (COND ((NULL VARS) NIL) (T (CONS (CONS (CAR VARS) N) (PRUP (CDR VARS) (PLUS N 1)))))) EXPR) ~MKPUSH returns a list of N (PUSH P i) instructions, where i runs ~ from M to M+N-1. Used to push arguments onto the stack. (DEFPROP MKPUSH (LAMBDA(N M) (COND ((LESSP N M) NIL) (T (CONS (LIST (QUOTE PUSH) (QUOTE P) M) (MKPUSH N (PLUS M 1)))))) EXPR) ~COMPEXP is the heart of LCOM0. It determines precisely ~ what an expression is, and compiles appropriate code ~ for it. It returns a list of that code. ~ EXP is the expression to be compiled. ~ M is minus the number of entries on the stack. When ~ added to a value retrieved from the A-LIST VPR, it ~ can be used to locate a variable on the stack. ~ VPR is an A-LIST, associating variable names with ~ numbers which, when added to M, give stack offsets. ~ Both M and VPR maintain these definitions throughout. (DEFPROP COMPEXP (LAMBDA(EXP M VPR) (COND ((NULL EXP) (QUOTE ((MOVEI 1 0)))) ~NIL ((EQ EXP T) (QUOTE ((MOVEI 1 (QUOTE T))))) ~T ((ATOM EXP) ~variable (LIST (LIST (QUOTE MOVE) 1 (PLUS M (CDR (ASSOC EXP VPR))) (QUOTE P)))) ((OR (EQ (CAR EXP) (QUOTE AND)) ~boolean expression (EQ (CAR EXP) (QUOTE OR)) (EQ (CAR EXP) (QUOTE NOT))) ((LAMBDA(L1 L2) (APPEND (COMBOOL EXP M L1 NIL VPR) (LIST (QUOTE (MOVEI 1 (QUOTE T))) (LIST (QUOTE JRST) 0 L2) L1 (QUOTE (MOVEI 1 0)) L2))) (GENSYM) (GENSYM))) ((EQ (CAR EXP) (QUOTE COND)) ~COND (COMCOND (CDR EXP) M (GENSYM) VPR)) ((EQ (CAR EXP) (QUOTE QUOTE)) ~QUOTE (LIST (LIST (QUOTE MOVEI) 1 EXP))) ((ATOM (CAR EXP)) ~function call ((LAMBDA(N) (APPEND (COMPLIS (CDR EXP) M VPR) (LOADAC (DIFFERENCE 1 N) 1) (LIST (LIST (QUOTE SUB) (QUOTE P) (LIST (QUOTE C) N 0 N 0))) (LIST (LIST (QUOTE CALL) N (LIST (QUOTE E) (CAR EXP)) (QUOTE S))))) (LENGTH (CDR EXP)))) ((EQ (CAAR EXP) (QUOTE LAMBDA)) ~LAMBDA expression ((LAMBDA(N) (APPEND (COMPLIS (CDR EXP) M VPR) (COMPEXP (CADDAR EXP) (DIFFERENCE M N) (APPEND (PRUP (CADAR EXP) (DIFFERENCE 1 M)) VPR)) (LIST (LIST (QUOTE SUB) (QUOTE P) (LIST (QUOTE C) N 0 N 0))))) (LENGTH (CDR EXP)))) (T NIL))) ~oops EXPR) ~COMPLIS compiles code to evaluate each expression in a list of ~ expressions and to push those values onto the stack. It ~ returns a list of that code. It is used to compile code ~ to evaluate arguments to called functions or LAMBDA expressions. ~ U is a list of expressions. (DEFPROP COMPLIS (LAMBDA(U M VPR) (COND ((NULL U) NIL) (T (APPEND (COMPEXP (CAR U) M VPR) (QUOTE ((PUSH P 1))) (COMPLIS (CDR U) (DIFFERENCE M 1) VPR))))) EXPR) ~LOADAC returns a list of (MOVE i j P) instructions, loading ~ consecutive accumulators from the top of the stack. ~ K indexes the accumulator loaded. ~ N indexes the stack offset. (DEFPROP LOADAC (LAMBDA(N K) (COND ((GREATERP N 0) NIL) (T (CONS (LIST (QUOTE MOVE) K N (QUOTE P)) (LOADAC (PLUS N 1) (PLUS K 1)))))) EXPR) ~COMCOND compiles a COND. ~ U is a list of clauses in the COND. ~ L is a label to be emitted at the end of all code for ~ the COND. (DEFPROP COMCOND (LAMBDA(U M L VPR) (COND ((NULL U) (LIST L)) (T ((LAMBDA(L1) (APPEND (COMBOOL (CAAR U) M L1 NIL VPR) (COMPEXP (CADAR U) M VPR) (LIST (LIST (QUOTE JRST) L) L1) (COMCOND (CDR U) M L VPR))) (GENSYM))))) EXPR) ~COMBOOL compiles code for a single predicate. That is, the ~ code generated evaluates the predicate and branches somewhere, ~ depending on the value. ~ P is the predicate. ~ L is a label which represents the branch point. ~ FLG is a flag. If FLG is NIL, code is to fall thru on non-NIL ~ result and branch to L on NIL result. If FLG is non-NIL, ~ code is to fall thru on NIL result and branch to L on ~ non-NIL result. (DEFPROP COMBOOL (LAMBDA(P M L FLG VPR) (COND ((ATOM P) ~simple variable (APPEND (COMPEXP P M VPR) (LIST (LIST (COND (FLG (QUOTE JUMPN)) (T (QUOTE JUMPE))) 1 L)))) ((EQ (CAR P) (QUOTE AND)) ~conjunction (COND ((NOT FLG) (COMPANDOR (CDR P) M L NIL VPR)) (T ((LAMBDA(L1) (APPEND (COMPANDOR (CDR P) M L1 NIL VPR) (LIST (LIST (QUOTE JRST) 0 L)) (LIST L1))) (GENSYM))))) ((EQ (CAR P) (QUOTE OR)) ~disjunction (COND (FLG (COMPANDOR (CDR P) M L T VPR)) (T ((LAMBDA(L1) (APPEND (COMPANDOR (CDR P) M L1 T VPR) (LIST (LIST (QUOTE JRST) 0 L)) (LIST L1))) (GENSYM))))) ((EQ (CAR P) (QUOTE NOT)) ~negation (COMBOOL (CADR P) M L (NOT FLG) VPR)) (T ~other expression (APPEND (COMPEXP P M VPR) (LIST (LIST (COND (FLG (QUOTE JUMPN)) (T (QUOTE JUMPE))) 1 L)))))) EXPR) ~COMPANDOR compiles code for lists of predicates connected ~ conjunctively or disjunctively. ~ U is a list of predicates. ~ L is a label. ~ FLG is a flag. If FLG is NIL, we are to fall thru on non-NIL ~ results and branch to L on NIL results (AND case). If FLG ~ is non-NIL, we are to fall thru on NIL results and branch ~ to L on non-NIL results (OR case). (DEFPROP COMPANDOR (LAMBDA(U M L FLG VPR) (COND ((NULL U) NIL) (T (APPEND (COMBOOL (CAR U) M L FLG VPR) (COMPANDOR (CDR U) M L FLG VPR))))) EXPR) .END .SKIP TO LINE 1 LCOM4: .BEGIN VERBATIM SELECT 1 .REQUIRE "LCOM4" SOURCE_FILE .END .s COMPUTABILITY .ss The function %2eval%1. Except for speed and memory size all present day stored program computers are equivalent in what computations they can do. A program written for one computer can be translated to run on another. Indeed, one can write a simulator for one computer to run on another. To put it in commercial terms, no computer manufacturer can advertise that his machine can do calculations impossible on the machine made by his competitors. This is well known intuitively, and the first mathematical theorem of this kind was proved by A.M. Turing (1936), who defined a primitive kind of computer now called a Turing machine, and showed how to make a universal machine that could do any computation done by any Turing machine when given a description of the machine to be simulated and the initial tape of the computation to be imitated. In LISP the function %2eval%1 is a universal LISP function in the sense that any computation done by any LISP function can be done by %2eval%1 when %2eval%1 is given suitable arguments. %2eval%1 has two arguments the first of which is a LISP expression in the notation given in the previous section, while the second is a list of pairs that give the values of any free variables that may occur in the expression. Since any computation can be described as evaluating an expression without free variables, the second argument plays a role mainly in the recursive definition of %2eval%1, and we can start our computations with the second argument NIL. To illustrate this, suppose we want to apply the function %2alt%1 to the list (A B C D E), i.e. we wish to evaluate %2alt[(A B C D E)]%1. This can be obtained by computing .NOFILL %2eval[((LABEL ALT (LAMBDA (X) (COND ((OR (NULL X) (NULL (CDR X))) X) (T (CONS (CAR X) (ALT (CDDR X))))))) (QUOTE (A B C D E)), NIL]%1, .FILL and gives the expected result (A C E). The second argument of %2eval%1, taken as NIL in the above example is a list of dotted pairs where the first element of each pair is an atom representing a variable and the second element is the value assigned to that variable. A variable may occur more than once in the list and the value chosen is that paired with the first occurrence of the variable. We illustrate this by the equation %2eval[(CAR X), ((X.(B.C)) (Y.A) (X.B))] = B%1, i.e. we have evaluated %3a %2x%1 with %2 x = (B.C)%1. The value associated with a variable in such a list of pairs is computed by the auxiliary function %2assoc%1 which has the recursive definition %2assoc[%2v, a] ← %3if n %2a %3then NIL %3else if aa %2a %3 eq %2v %3then a %2a %3else %2alt[%2v, %3d %2a]%1. .BEGIN PREFACE 0 NOFILL Thus we have %2assoc[X, ((X.(B.C)) (Y.A) (X.B))] = (X.(B.C))%1. A simplified version of the usual LISP %2eval%1 is the following: %2eval[%2e, a] ← .FILL %3if at %2e %3then [%3if %2numberp %2e ∨ %2e %3eq NIL ∨ %2e %3eq T %3then %2e %3else%2 assoc[%2e, a]] .NOFILL %3else if at a%2 e %3then [%3if a %2e%3 eq CAR %3then a %2eval[%3ad %2e, a] %3else if a %2e%3 eq CDR %3then d %2eval[%3ad %2e, a] .FILL %3else if a %2e%3 eq CONS %3then %2eval[%3ad %2e, a] . %2eval[%3add %2e, a] .NOFILL %3else if a %2e%3 eq ATOM %3then at %2eval[%3ad %2e, a] .FILL %3else if a %2e%3 eq EQ %3then at %2eval[%3ad %2e, a] %3eq %2eval[%3add %2e, a] .NOFILL %3else if a %2e%3 eq QUOTE %3then ad %2e %3else if a %2e%3 eq COND %3then %2evcon[%3d %2e, a] .FILL %3else if a %2e%3 eq LIST %3then %2mapcar[%3d %2e, λ%2x: %2eval[%2x, a]] .NOFILL %3else %2eval[%3d %2assoc[%3a %2e, a] . %3d %2e, a]] .FILL %3else if aa %2e %3eq LAMBDA %3then %2eval[%3adda %2e, prup[%3ada %2e, mapcar[%3d %2e, λ%2x: %2eval[%2x, a]]] * %2a] .BREAK %3else if aa %2e %3eq LABEL %3then %2eval[%3adda %2e . %3d %2e, [%3ada %2e . %3a %2e] . %2a]%1, .NOFILL where the auxiliary function %2evcon%1 is defined by .FILL %2evcon[%2u, a] ← %3if %2eval[%3aa %2u, a] %3then %2eval[%3ada %2u, a] %3else %2evcon[%3d %2u, a]%1, .END and the auxiliary function %2prup%1 used for pairing up the elements of two lists of equal length is defined by .BEGIN PREFACE 0 NOFILL .FILL %2prup[%2u, v] ← %3if n %2u %3then NIL %3else [%3a %2u . %3a %2v] . %2prup[%3d %2u,%3d %2v].%1 .NOFILL .END The way %2eval%1 works should be clear; atoms are either immediately evaluable or have to be looked up on the list %2a%1; expressions whose first term is one of the elementary functions are evaluated by performing the indicated operation on the result of evaluating the arguments; %2list%1 has to be handled specially, because it has an indefinite number of arguments; conditionals are handled by an auxiliary function that evaluates the terms in the right order; quoted S-expressions are trivial; non-elementary functions have their definitions looked up on %2a%1 and substituted for their names; when a function is specified by a λ, the inner expression is evaluated with a new %2a%1 which is obtained by evaluating the arguments and pairing them up with the variables and putting them on the front of the old %2a%1; and finally, %3label%1 is handled by pairing the name of the function with the expression on %2a%1 and replacing the whole function by the λ-part. %2eval%1 plays both a theoretical and a practical role in LISP. Historically, the list notation for LISP functions and %2eval%1 were first devised in order to show how easy it is to define a universal function in LISP - the idea was to advocate LISP as an alternative to Turing machines for doing the elementary theory of computability. The notation used was chosen without much regard for human convenience, because the original idea was purely theoretical; the notation for conditional expressions, for example, has an unnecessary extra level of parentheses. However, S. R. Russell noted that %2eval%1 could serve as an interpreter for LISP and promptly programmed it in machine language with minor modifications for practical purposes. Since a compiler was long delayed, the interpreter was more easily modified and handled some difficult cases with functional arguments better, an interpreter based on %2eval%1 has remained a feature of most LISP systems. The way %2eval%1 handles arguments corresponds to the call-by-value method of parameter passing in ALGOL and similar languages. There is also a form of %2eval%1 that corresponds to call-by-name. Here it is: .BEGIN PREFACE 0 NOFILL %2neval[%2e, a] ← %3if at %2e%3 then [%3if %2e %3eq T %3 then T %3else if %2e %3eq NIL %3then NIL %3else if %2numberp e %3then %2e %3else %2neval[%3ad %2assoc[%2e, a], %3dd %2 assoc[%2e, a]]] %3else if at a %2e %3 then [%3if a %2e %3eq CAR %3then a %2neval[%3ad %2e, a] %3else if a %2e %3eq CDR %3then d %2neval[%3ad %2e, a] .FILL %3else if a %2e %3eq CONS %3then %2neval[%3ad %2e, a] . neval[%3add %2e, a] .NOFILL %3else if a %2e %3eq ATOM %3then at %2neval[%3ad %2e, a] .FILL %3else if a %2e %3eq EQ %3then %2neval[%3ad %2e, a] %3eq %2neval[%3add %2e, a] .NOFILL %3else if a %2e %3eq QUOTE %3then ad %2e %3else if a %2e %3eq COND %3then %2nevcon[%3d %2e, a] .FILL %3else if a %2e %3eq LIST %3then %2mapcar[%3d %2e , λ%2x: %2neval[%2x, a]] .NOFILL %3else %2neval[%3d %2assoc[%3a %2e, a] . %3d %2e, a]] .FILL %3else if aa %2e %3eq LAMBDA %3then %2neval[%3adda %2e, nprup[%3ada %2e, %3d %2e, %2a]] .NOFILL .FILL %3else if aa %2e %3eq LABEL %3then %2neval[%3adda %2e . %3d %2e, [%3ada %2e . %3a %2e] . %2a], %1 .NOFILL where the auxiliary function %2nevcon%1 is given by .FILL %2nevcon[%2u, a] ← %3if %2neval[%3aa %2u, %2a] %3then %2neval[%3ada %2u, %2a] %3else %2nevcon[%3d %2u, %2a].%1 and nprup is .FILL %2nprup[%2u, v,a] ← %3if n %2u %3then %2a %3else [%3a %2u . [%3a %2v . a]] . %2nprup[%3d %2u, %3d %2v,a].%1 .END The difference between %2eval%1 and %2neval%1 is only in two terms. %2eval%1 evaluates a variable by looking it up on the association list whereas %2neval%1 looks it up on the association list and evaluates the result in the context in which it was put on the association list. Correspondingly, when a λ-expression is encountered, %2eval%1 forms a new association list by pairing the values of the arguments with the variables bound by the λ and putting the new pairs in front of the old association list, whereas %2neval%1 pairs the arguments themselves with the variables and puts them on the front of the association list. The function neval also saves the current association list with each variable on the association list, so that the variables can be evaluated in the correct context. In most cases both give the same result with the same work, but %2neval%1 gives a result in some cases in which %2eval%1 loops. An example is obtained by evaluating %2F[2, 1]%1 where %2F%1 is defined by .NOFILL %2F[%2x, y] ← %3if%2 x=0 %3then 0 %3else %2F[%2x-1, %2F[%2y-2, %2x]].%1 Exercises .FILL 1. Write %2neval%1 and the necessary auxiliary functions in list form, and try them out on some examples. .ss Computability.%1 Some LISP calculations run on indefinitely. The most trivial case occurs if we make the recursive definition %2loop x ← %2loop x%1 and attempt to compute %2loop[%2x]%1 for any %2x%1 whatsoever. Don't dismiss this example just because no-one would write such an obviously useless function definition. There is a sense in which it is the "zero" of a large class of non¬terminating function definitions, and, as the Romans experienced but never learned, leaving zero out of the number system is a mistake. Nevertheless, in most programming, non-terminating calculations are the results of errors in defining functions. Therefore, it would be useful to be able to tell whether a function definition gives a result for all arguments. In fact, it would be useful to be able to tell whether a function will terminate for a single argument. Let us make this goal more precise. Suppose that %2f%1 is a LISP function and %2a%1 is an S-expression, and we would like to know whether the computation of %2f[%2a]%1 terminates. Suppose %2f%1 is represented by the S-expression %2f*%1 in the usual S-expression notation for LISP functions. Then the S-expression (f* (QUOTE a))%1 represents %2f[%2a]%1. Define the function %2term%1 by giving %2term[%2e]%1 the value %3true%2 if %2e%1 is an S-expression of the form (f* (QUOTE a))%1 for which %2f[%2a]%1 terminates and %3false%1 otherwise. We now ask whether %2term%1 is a LISP function, i.e. can it be constructed from %2car, cdr, cons, atom, %1 and %2eq%1 using λ, %3label%1, and conditional expressions? Well, it can't, as we shall shortly prove, and this means that it is not %2computable%1 whether a LISP calculation terminates, since if %2term%1 were computable by any computer or in any recognized sense, it could be represented as a LISP function. Here is the proof: Consider the function %2terma%1 defined from %2term%1 by %2terma u ← %3if%2 term list[%2u, list[QUOTE%2, u]] %3then%2 loop u %3else true%1, and suppose that %2f%1 is a LISP function and that %2f*%1 is its S-expression representation. What is %2terma f*%1? Well %2terma f*%1 tells us whether the computation of %2f[%2f*]%1 terminates, and it tells us this by going into a loop if %2f[%2f*]%1 terminates and giving %3true%1 otherwise. Now if %2term%1 were a LISP function, then %2terma%1 would also be a LISP function. Indeed if %2term%1 were represented by the S-expression %2term*%1, then %2terma%1 would be represented by the S-expression %2terma* = (LAMBDA (U) (COND ((%2term* (LIST U (LIST (QUOTE QUOTE) U))) (LOOP U)) (T T))). Now consider %2terma[%2terma*]%1. According to the definition of %2terma%1, this will tell us whether %2terma[%2terma*]%1 is defined, i.e. it tells about itself. However, it gives this answer in a contradictory way; namely %2terma[%2terma*]%1 looping tells us that %2terma[%2terma*]%1 terminates, and %2terma[%2terma*]%1 being %3true%1 tells us that %2terma[%2terma*]%1 doesn't terminate. This contradiction tells us that %2term%1 is not a LISP function, and there is no general procedure for telling whether a LISP calculation terminates. The above result does not exclude LISP functions that tell whether LISP calculations terminate. It just excludes perfect ones. Suppose we have a function %2t%1 that sometimes says calculations terminate, sometimes says they don't terminate, and sometimes runs on indefinitely. We shall further assume that when %2t%1 gives an answer it is always right. Given such a function we can improve it a bit so that it will always give the right answer when the calculation it is asked about terminates. This is done by mixing the computation of %2t[%2e]%1 with a computation of %2eval[%2e, NIL]%1 doing the computations alternately. If the %2eval[%2e, NIL]%1 computation ever terminates, then the new function asserts termination. Given such a %2t%1, we can always find a calculation that does not terminate but %2t%1 doesn't say so. The construction is just like that used in the previous proof. Given %2t%1, we construct %2ta u ← %3if%2 t list[%2u, list[QUOTE%2, u]] %3then%2 loop u %3else true%1, and then we consider %2ta[%2ta*]%1. If this had the value %3true%1, then it wouldn't terminate so therefore it doesn't terminate but is not one of those expressions which %2t%1 decides. Thus for any partial decider we can find a LISP calculation which doesn't terminate but which the decider doesn't decide. This can in turn be used to get a slightly better decider, namely %2t%51[%2e] ← %3if%2 e = %2ta* %3then DOESN'T-TERMINATE %3else%2 t[%2e]%1. Of course, %2t%51%1 isn't much better than %2t%1, since it can decide only one more computation, but we can form %2t%52%1 by applying the same process, and so forth. In fact, we can even form %2t%5∞%1 which decides all the cases decided by any %2t%5n%1. This can be further improved by the same process, etc. How far can we go? The answer is technical; namely, the improvement process can be carried out any recursive ordinal number of times. Unfortunately, this kind of improvement seems to be superficial, since none of the new computations proved not to terminate are likely to be of practical interest. Exercises. .ITEM←0; #. Write a function that gives %2t%5n+1%1 in terms of %2t%5n%1. #. Write a function that gives %2t%5∞%1 in terms of %2t%1. #. If you know about Turing machines, write a LISP function to simulate an arbitrary Turing machine given a description of the machine in some convenient notation. #. Write a LISP function that will translate a Turing machine description into a LISP function that will do the same computation. #. If you really like Turing machines, write a description of a Turing machine that will interpret LISP internal notation. .s PROVING LISP PROGRAMS CORRECT In this chapter we will introduce techniques for proving LISP programs correct. The techniques will mainly be limited to what we may call %2clean%1 LISP programs. In particular, there must be no side effects, because our methods depend on the ability to replace subexpressions by equal expressions. The necessary basic facts can be divided into several categories: first order logic including conditional forms and first order lambda-expressions, algebraic facts about lists and S-expressions, facts about the inductive structure of lists and S-expressions, and general facts about functions defined by recursion. .ss First order logic with conditional forms and lambda-expressions. The logic we shall use is called first order logic with equality, but we will extend it by allowing conditional forms to be terms and lambda-expressions to be function expressions. From the mathematical point of view, these extensions are inessential, because, as we shall see, every sentence that includes conditional forms or first order lambdas can readily be transformed into an equivalent sentence without them. However, the extensions are practically important, because they permit us to use recursive definitions directly as formulas of the logic. Formulas of the logic are built from constants, variables predicate symbols, and function symbols using function application, conditional forms, boolean forms, lambda expressions, and quantifiers. %3Constants%1: We will use S-expresssions as constants standing for themselves and also lower case letters from the first part of the alphabet to represent constants in other domains than S-expressions. %3Variables%1: We will use the letters %2u%1 thru %2z%1 with or without subscripts as variables. The variables %2u%1 and %2v%1 will usually stand for lists while %2x%1 thru %2z%1 will stand for S-expressions. %3Function symbols%1: The letters %2f%1, %2g%1 and %2h%1 with or without subscripts are used as function symbols. The LISP function symbols %3a%1, %3d%1 and . (as an infix) are also used as function symbols. We suppose that each function symbol takes the same definite number of arguments every time it is used. We will often use one argument functions symbols as prefixes, i.e. without brackets, just as %3a%1 and %3d%1 have been used up to now. %3Predicate symbols%1: The letters %2p%1, %2q%1 and %2r%1 with or without subscripts are used as predicate symbols. We will also use the LISP predicate symbol %3at%1 as a constant predicate symbol. The equality symbol = is also used as an infix. We suppose that each predicate symbol takes the same definite number of arguments each time it is used. Infix and prefix notation will also be used where this is customary. Next we define terms, sentences, function expressions and predicate expressions inductively. A term is an expression whose value will be an object like an S-expression or a number while a sentence has value T%1 or F%1. Terms are used in making sentences, and sentences occur in terms so that the definitions are %2mutually recursive%1 where this use of the word %2recursive%1 should be distinguished from its use in recursive definitions of functions. Function expressions are also involved in the mutual recursion. %3Terms%1: Constants are terms, and variables are terms. If %2f%1 is a function expression taking %2n%1 arguments, and %2t%51%2,_..._,t%5n%2%1 are terms, then %2f[t%51%2,_..._,t%5n%2]%1 is a term. If %2p%1 is a sentence and %2t%51%2%1 and %2t%52%1 are terms, then %3if%2_p_%3then%2_t%51%2_%3else%2_t%52%1%1 is a term. We soften the notation by allowing infix symbols where this is customary. %3Sentences%1: If %2p%1 is a predicate expression taking %2n%1 arguments and %2t%51%2,_..._,t%5n%2%1 are terms, then %2p[t%51%2,_..._,t%5n%2]%1 is a sentence. Equality is also used as an infixed predicate symbol to form sentences, i.e. %2t%51%2_=_t%52%1%1 is a sentence. If %2p%1 is a sentence, then %2¬p%1 is also a sentence. If %2p%1 and %2q%1 are sentences, then %2p∧q%1, %2p∨q%1, %2p⊃q%1, and %2p≡q%1 are sentences. If %2p%1, %2q%1 and %2r%1 are sentences, then %3if%2_p_%3then%2_q_%3else%2_r%1 is a sentence. If %2x%51%2,_...,_x%5n%2%1 are variables, and %2p%1 is a term, then %2∀x%51%2_..._x%5n%2:t%1 and %2∀x%51%2_..._x%5n%2:t%1 are sentences. %3Function expressions%1: A function symbol is a function expression. If %2x%51%2,_..._,x%5n%2%1 are variables and %2t%1 is a term, then %2[λx%51%2,_..._,x%5n%2:t]%1 is a function expression. %3Predicate expressions%1: A predicate symbol is a predicate expression. If %2x%51%2,_..._,x%5n%2%1 are variables and %2p%1 is a sentence, then %2[λx%51%2,_..._,x%5n%2:p]%1 is a predicate expression. An occurrence of a variable %2x%1 is called bound if it is in an expression of one of the forms %2[λx%51%2_..._x%5n%2:t]%1, %2[λx%51%2_..._x%5n%2:p]%1, %2[∀x%51%2_..._x%5n%2:p]%1 or %2[∃x%51%2_..._x%5n%2:p]%1 where %2x%1 is one of the numbered %2x%1's. If not bound an occurrence is called free. The %2semantics%1 of first order logic consists of the rules that enable us to determine when a sentence is true and when it is false. However, the truth or falsity of a sentence is relative to the interpretation assigned to the constants, the function and predicate symbols and the free variables of the formula. We proceed as follows: We begin by choosing a domain. In most cases we shall consider the domain will include the S-expressions and any S-expression constants appearing in the formula stand for themselves. We will allow for the possibility that other objects than S-expressions exist, and some constants may designate them. Each function or predicate symbol is assigned a function or predicate on the domain. We will normally assign to the basic LISP function and predicate symbols the corresponding basic LISP functions and predicates. Each variable appearing free in a sentence is also assigned an elemet of the domain. All these assignments constitute an interpretation, and the truth of a sentence is relative to the interpretation. The truth of a sentence is determined from the values of its constituents by evaluating successively larger subexpressions. The rules for handling functions and predicates, conditional expressions, equality, and Boolean expressions are exactly the same as those we have used in the previous chapters. We need only explain quantifiers: %2∀x%51%2_..._x%5n%2:e%1 is assigned true if and only if %2e%1 is assigned true for all assignments of elements of the domain to the %2x%1's. If %2e%1 has free variables that are not among the %2x%1's, then the truth of the sentence depends on the values assigned to these remaining free variables. %2∃x%51%2_..._x%5n%2:e%1 is assigned true if and only if %2e%1 is assigned true for %2some%1 assignment of values in the domain to the %2x%1's. Free variables are handled just as before. %2λx%51%2_..._x%5n%2:u%1 is assigned a function or predicate according to whether %2u%1 is a term or a sentence. The value of %2[λx%51%2_..._x%5n%2:u][t%51%2,...,t%5n%2] is obtained by evaluating the %2t%1's and using these values as values of the %2x%1's in the evaluation of %2u%1. If %2u%1 has free variables in addition to the %2x%1's, the function assigned will depend on them too. Those who are familiar with the lambda calculus should note that λ is being used here in a very limited way. Namely, the variables in a lambda-expression take only elements of the domain as values, whereas the essence of the lambda calculus is that they take arbitrary functions as values. We may call these restricted lambda expressions %2first order lambdas%1. .ss Conditional forms. All the properties we shall use of conditional forms follow from the relation %2[p ⊃ [%3if%2 p %3then %2a %3else%2 b] = a] ∧ [¬p ⊃ [%3if%2 p %3then%2 a %3else%2b] = b]%1. (If we weren't adhering to the requirement that all terms be defined for all values of the variables, the situation would be more complicated). It is, however, worthwhile to list separately some properties of conditional forms. First we have the obvious %3if_T_%3then%2_a_%3else%2_b%2 = a%1 and %3if_F_%3then%2_a_%3else%2_b%2 = b%1. Next we have a %2distributive law%1 for functions applied to conditional forms, namely %2f[%3if%2 p %3then%2 a %3else%2 b] = %3if%2 p %3then%2 f[a] %3else%2 f[b]%1. This applies to predicates as well as functions and can also be used when one of the arguments of a function of several arguments is a conditional form. It also applies when one of the terms of a conditional form is itself a conditional form. Thus %3if%2 [%3if%2 p %3then%2 q %3else%2 r] %3then%2 a %3else%2 b = %3if%2 p %3then%2 [%3if%2 q %3then%2 a %3else%2 b] %3else%2 [%3if%2 r %3then%2 a %3else%2 b]%1 and %3if%2 p %3then%2 [%3if%2 q %3then%2 a %3else%2 b] %3else%2 c = %3if%2 q %3then%2 [%3if%2 p %3then%2 a %3else%2 c] %3else%2 [%3if%2 p %3then%2 b %3else%2 c]%1. When the expressions following %3then%1 and %3else%1 are sentences, then the conditional form can be replaced by a sentence according to %2[%3if%2 p %3then%2 q %3else%2 r] ≡ [p ∧ q] ∨ [¬p ∧ r]%1. These two rules permit eliminating conditional forms from sentences by first using distributivity to move the conditionals to the outside of any functions and then replacing the conditional form by a Boolean expression. Note that the elimination of conditional forms may increase the size of a sentence, because %2p%1 occurs twice in the right hand side of the above equivalence. In the most unfavorable case, %2p%1 is dominates the size of the expression so that writing it twice almost doubles the size of the expression. Suppose that %2a%1 and %2b%1 in %3if%2_p_%3then%2_a_%3else%2_b%1 are expressions that may contain the sentence %2p%1. Occurrences of %2p%1 in %2a%1 can be replaced by T%1, and occurrences of %2p%1 in %2b%1 can be replaced by F%1. This follows from the fact that %2a%1 is only evaluated if %2p%1 is true and %2b%1 is evaluated only if %2p%1 is false. This leads to a strengthened form of the law of replacement of equals by equals. The ordinary form of the law says that if we have %2e_=_e'%1, then we can replace any occurrence of %2e%1 in an expression by an occurrence of %2e'%1. However, if we want to replace %2e%1 by %2e'%1 within %2a%1 within %3if%2_p_%3then%2_a_%3else%2_b%1, then we need only prove %2p_⊃_e_=e'%1, and to make the replacement within %2b%1 we need only prove %2¬p_⊃_e_=_e'%1. Additional facts about conditional forms are given in (McCarthy 1963a) including a discussion of canonical forms that parallels the canonical forms of Boolean forms. Any question of equivalence of conditional forms is decidable by truth tables analogously to the decidability of Boolean forms. .ss Lambda-expressions. The only additional rule required for handling lambda-expressions in first order logic is called %2lambda-conversion%1, essentially %2[λx:e][a] =%1 <the result of substituting %2e%1 for %2x%1 in %2a%1>. As examples of this rule, we have %2[λx:%3a%2 x . y][u . v] = [%3a%2[u . v]] . y%1. However, a complication requires modifying the rule. Namely, we can't substitute for a variable and expression that has a free variable into a context in which that free variable is bound. Thus it would be wrong to substitute %2x_+_y%1 for %2x%1 in %2∀y:[x_+_y_=_z]%1 or into the term %2[λy:x_+_y][u_+_v]%1. Before doing the substitution, the variable %2y%1 would have to be replaced in all its bound occurrences by a fresh variable. Lambda-expressions can always be eliminated from sentences and terms by lambda-conversion, but the expression may increase greatly in length if a lengthy term replaces a variable that occurs more than once in %2e%1. It is easy to make an expression of length %2n%1 whose length is increased to 2%6n%1 by converting its %2n%1 nested lambda-expressions. .ss Algebraic axioms for S-expressions and lists. The algebraic facts about S-expressions are expressed by the following sentences of first order logic: %2∀x.(issexp x ⊃ %3at%2 x ∨ (issexp %3a%2 x ∧ issexp %3d%2 x ∧ x = (%3a%2 x . %3d%2 x)))%1 and %2∀x y.(issexp x ∧ issexp y ⊃ issexp(x.y) ∧ ¬%3at%2(x.y) ∧ x = %3a%2(x.y) ∧ y = %3d%2(x.y))%1. Here %2issexp e%1 asserts that the object %2e%1 is an S-expression so that the sentences used in proving a particular program correct can involve other kinds of entities as well. If we can assume that all objects are S-expressions or can declare certain variables as ranging only over S-expressions, we can simplify the axioms to %2∀x.[%3at%2 x ∨ x = [%3a%2 x . %3d%2 x]]%1 and %2∀x y.[¬%3at%2[x.y] ∧ x = %3a%2[x.y] ∧ y = %3d%2[x.y]]%1. The algebraic facts about lists are expressed by the following sentences of first order logic: %2∀x. islist x ⊃ x = NIL%2 ∨ islist %3d %2x%1, %2∀x y. islist y ⊃ islist[x . y]%1, %2∀x y. islist y ⊃ %3a%2[x . y] = x ∧ %3d%2[x.y] = y%1. We can rarely assume that everything is a list, because the lists usually contain atoms which are not themselves lists. These axioms are analogous to the algebraic part of Peano's axioms for the non-negative integers. The analogy can be made clear if we write Peano's axioms using %2n'%1 for the successor of %2n%1 and %2n%6-%1 for the predecessor of %2n%1. Peano's algebraic axioms then become %2∀n: n' ≠ 0%1, %2∀n: (n')%6-%2 = n%1, and %2∀n: n ≠ 0 ⊃ (n%6-%2)' = n%1. Integers specialize lists if we identify 0 with NIL%1 and assume that there is only one object (say 1) that can serve as a list element. Then %2n'_=_cons[1,n]%1, and %2n%6-%2_=_%3d%2 n%1. Clearly S-expressions and lists satisfy the axioms given for them, but unfortunately these algebraic axioms are insufficient to characterize them. For example, consider a domain of one element a%1 satisfying %3a%2 a = %3d%2 a = a . a = a%1. It satisfies the algebraic axioms for S-expressions. We can exclude it by an axiom %2∀x.(%3a%2 x ≠ x)%1, but this won't exclude other circular list structures that eventually return to the same element by some %3a-d%1 chain. Actually we want to exclude all infinite chains, because most LISP programs won't terminate unless every %3a-d%1 chain eventually terminates in an atom. This cannot be done by any finite set of axioms. .ss Axiom schemas of induction. In order to exclude infinite list structures we need axiom schemas of induction analogous to Peano's for the integers. Peano's induction schema is ordinarily written %2P(0) ∧ ∀n:(P(n) ⊃ P(n')) ⊃ ∀n:P(n)%1. Here %2P(n)%1 is an arbitrary predicate of integers, and we get particular instances of the schema by substituting particular predicates. It is called an axiom schema rather than an axiom, because we consider the schema, which is not properly a sentence of first order logic, as standing for the infinite collection of axioms that arise from it by substituting all possible predicates for %2P%1. Peano's induction schema can also be written %2∀n:(n = 0 ∨ P(n%6-%2) ⊃ P(n)) ⊃ ∀n:P(n)%1, and the equivalence of the two forms is easily proved. The S-expression analog is %2∀x:[issexp x ⊃ [%3at%2 x ∨ P[%3a%2 x] ∧ P[%3d%2 x] ⊃ P[x]]] ⊃ ∀x:[issexp x ⊃ P[x]]%1, or, assuming everything is an S-expression %2∀x:[%3at%2 x ∨ P[%3a%2 x] ∧ P[%3d%2 x] ⊃ P[x]] ⊃ ∀x:P[x]%1. The corresponding axiom schema for lists is %2∀u:[islist u ⊃ [%3n%2 u ∨ P[%3d%2 u] ⊃ P[u]]] ⊃ ∀u:[islist u ⊃ P[u]]%1. These schemas are called principles of %2structural induction%1, since the induction is on the structure of the entities involved. .ss Proofs by structural induction. Recall that the operation of appending two lists is defined by !!si2: %2u * v ← %3if n%2 u %3then%2 v %3else a%2 u . [%3d%2 u * v]%1. Let us assume that %2u * v%1 is defined for all %2u%1 and %2v%1, i.e. the computation described above terminates for all %2u%1 and %2v%1; we will show how to prove it later. Then we can replace ({[5] si2}) by the sentence !!si1: %2∀u v:[islist u ∧ islist v ⊃ [%2u * v = %3if n%2 u %3then%2 v %3else a%2 u . [%3d%2 u * v]]]%1. Now suppose we would like to prove %2∀v:[NIL%2 * v = v]%1. This is quite trivial; we need only substitute NIL%1 for %2x%1 in ({[5] si1}), getting →NIL%2 * v ∂(15)_= %3if n NIL %3then%2 v %3else a NIL%2 . [%3d NIL%2 * v] ∂(15)_= v%1. Next consider proving %2∀u:[u * NIL%2 = u]%1. This cannot be done by simple substitution, but it can be done as follows: First substitute %2λu:[u * NIL%2 = u]%1 for %2P%1 in the induction schema %2∀u:[islist u ⊃ [%3n%2 u ∨ P[%3d%2 u] ⊃ P[u]]] ⊃ ∀u:[islist u ⊃ P[u]]%1, getting %2∀u:[islist u ⊃ [%3n%2 u ∨ %2λu:[u * NIL%2 = u][%3d%2 u] ⊃ %2λu:[u * NIL%2 = u][u]]] ⊃ ∀u:[islist u ⊃ %2λu:[u * NIL%2 = u][u]]%1. Carrying out the indicated lambda conversions makes this !!si3: %2∀u:[islist u ⊃ [qn u ∨ qd u * qnil = qd u] ⊃ u * qnil = u] ⊃ ∀u:[islist u ⊃ u * qnil = u]%1. Next we must use the recursive definition of %2u*v%1. There are two cases according to whether qn %2u%1 or not. In the first case, we substitute qnil for %2v%1 and get qnil*qnil_=_qnil, and in the second case we use the hypothesis qd_u_*_qnil_=_qd_u and the third algebraic axiom for lists to make the simplification !!si4: %2qa u . [qd u * qnil] = qa u . qd u = u.%1 Combining the cases gives the hypothesis of ({eq si3}) and hence its conclusion, which is the statement to be proved. .ss First Order Theory of Partial Functions .BACK;