perm filename LSPDOC[206,LSP]2 blob sn#257206 filedate 1977-01-06 generic text, type C, neo UTF8
C00001 00001
C00004 00002	.device xgp
C00011 00005	.ss Atoms.
C00013 00006	.ss List structures.
C00019 00007	.ss S-expressions.
C00028 00008	.ss The basic functions and predicates of LISP.
C00041 00009	.ss Conditional expressions.
C00048 00010	.ss Boolean expressions.
C00052 00011	.ss Recursive function definitions.
C00070 00012	.ss Lambda expressions and functions with functions as arguments.
C00082 00013	.ss Label.
C00085 00014	.ss Numerical computation.
C00098 00016	.ss Simple list recursion.
C00106 00017	.ss Simple S-expression recursion.
C00109 00018	.ss Other structural recursions.
C00112 00019	.<<\\M0NGR25\M1BDJ25\M2BDR25X\M3SUB\M4NGR30\M5NGR40\M6SUP%1 >>
C00127 00020	.ss Game trees.
C00139 00021	.sec COMPILING IN LISP
C00143 00022	.ss Some facts about the PDP-10.
C00149 00023	.ss Code produced by LISP compilers.
C00153 00025		Note  that all three compilers produce the same first line of
C00156 00026	.ss Listings of LCOM0 and LCOM4
C00157 00027	.SKIP TO LINE 1
C00158 00028	.SKIP TO LINE 1
C00171 00029	.SKIP TO LINE 1
C00172 00030	.sec COMPUTABILITY
C00200 00032	.ss First order logic with conditional forms and lambda-expressions.
C00212 00033	.ss Conditional forms.
C00218 00034	.ss Lambda-expressions.
C00220 00035	.ss Algebraic axioms for S-expressions and lists.
C00224 00036	.ss Axiom schemas of induction.
C00226 00037	.ss Proofs by structural induction.
C00229 00038	.STANDARD BACK
C00230 ENDMK
.device xgp
.evenleftborder ← oddleftborder ← 1000;
.require "pubmac[206,LSP]" source_file
.standard front(I, 1)
.font 1 "baxl30" <<text>>
.font 2 "bdr30" <<sym>>
.font 3 "baxm30" <<var>>
.font 4 "basb30" <<bold>>
.font 5 "bdr30" <<const>>
.font 6 "sub"
.font 7 "sup"
.font A "fix40"
.font B "fix30"
.font C "grfx25"
.font D "grfx35"
.NARROW 0,200-81;
.INDENT 0,0,0;
.turn on "%#π" ;
.every heading(, {SECNAME}, {page}) ;
.AT 8 ⊂"%1        %*"⊃ ;
.AT 16 ⊂"%1                %*"⊃ ;
.skip 20
.CB by John McCarthy
.skip 20
.cb Stanford University
.skip 5
.cb Copyright 1976 by John McCarthy
.skip 10
.once center
.TURN ON "{}"
This version printed at {time} on {date}.
.TURN OFF "{}"
.sec                  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

	The most common form of S-expression is the  list,  and  here
are some lists:

The list
	%5(A B C E)
%1has four elements.

The list
	%5(A B (C D) E)
%1has four elements one of which is itself a list.

The list
%1has one element.

The list
	%5((A B C D))
%1also has one element which itself is a list.

The list
%1has no elements; it is also written
%1The list
	%5(PLUS X Y)
%1has three elements and may be used to represent the expression
	%3x%2 + %3y.

%1The list
	%5(PLUS (TIMES X Y) X 3)
%1has four elements and may be used to represent the expression
	%3xy%2 + %3x%2 + %53.

%1The list
	%5(EXIST X (ALL Y (IMPLIES (P X) (P Y))))
%1may be used to represent the logical expression

%1The list
%1may be used to represent the expression


%1The list
	%5((A B) (B A C D) (C B D E) (D B C E) (E C D F) (F E))
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.

                ≤'  ~  `≥
            B ≤'    ~    `≥ E
  A ααααααααα'      ~      `ααααααααα F
             ≥             ≤
              `≥    ~    ≤'
                `≥  ~  ≤'

                             Figure 1

	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

	%5(A B(C  D)    E)


	%5(A B (C D) E)

%1are regarded as the same.

.ss Atoms.

	The expressions %5A, B, X, Y, 3, PLUS, %1and %5ALL%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


%1and from these we can form lists like

	((345 3.14159 -47) A307B THE-LAST-TRUMP -45.21).
.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   %5(PLUS
(TIMES  X  Y)  X  3)%1   which may represent the expression  %3xy%2 + %3x%2 + %53  is
shown in figure 2.

        ⊂αααπααα⊃     ⊂αααπααα⊃     ⊂αααπααα⊃     ⊂αααπααα⊃
  ααααα→~   ~   εαααα→~   ~   εαααα→~   ~   εαααα→~   ~   εααααααα⊃
        %απα∀ααα$     %απα∀ααα$     %απα∀ααα$     %απα∀ααα$       ~
          ↓             ~             ~             ↓             ~
         PLUS           ~             ~             3             ~
                        ~  ⊂αααπααα⊃  ~  ⊂αααπααα⊃     ⊂αααπααα⊃  ~
                        %α→~   ~   εααβα→~   ~   εαααα→~   ~   ~  ~
                           %απα∀ααα$  ~  %απα∀ααα$     %απα∀απα$  ~
                             ↓        ~    ~             ↓   ~    ~
                           TIMES      %απαα$             Y   %ααπα$
                                        ↓                       ↓
                                        X                      NIL

                              Figure 2.

	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 are 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

	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  %5NIL%1.

	A  list  is  referred  to  by giving 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  %5PLUS%1, while its d-part points to the
list  %5((TIMES X Y) X 3)%1.  The second word contains the list structure
representing  %5(TIMES X Y)%1  in  its  a-part  and  the  list  structure
representing  %5(X 3)%1  in its d-part.  The last word points to the atom
%53%1  in its a-part and has a pointer to the atom  %5NIL%1  in its  d-part.
This is consistent with the convention that  %5NIL%1  represents the null

.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  %5NIL%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

<S-expression> ::= <atom> | (<S-expression> . <S-expression>).

Examples of S-expressions are

	(A . B)
	(A . (B . A))
	(PLUS (X . (Y . NIL)))
	(3 . 3.4)

%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
%5(A.B),  (A.(B.A))%1,  and  %5(PLUS.(X.(Y.NIL)))%1,  but if we wrote %5(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  %5(A.B),  (A.(B.A))%1, and  %5(PLUS.(X.(Y.NIL))) %1
are represented by the list structures of figure 3.

        ⊂αααπααα⊃                             ⊂αααπααα⊃     ⊂αααπααα⊃
        ~   ~   ~                             ~   ~   εαααα→~   ~   ~
        %απα∀απα$                             %απα∀ααα$     %απα∀απα$
          ↓   ↓                                 ~             ↓   ~
          A   B                                 ~             B   ~
                                                ~                 ~
                                                ~                 ~

        ⊂αααπααα⊃     ⊂αααπααα⊃     ⊂αααπααα⊃
        ~   ~   εαααα→~   ~   εαααα→~   ~   ~
        %απα∀ααα$     %απα∀ααα$     %απα∀απα$
          ↓             ↓             ↓   ↓
         PLUS           X             Y  NIL

                              Figure 3.

	Note that the list %5(PLUS X Y)%1 and the S-expression
%5 (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. %5((A . B) (C . D) (3))%1.

	In general, the list %2(%3a b . . .  z%2)%1 may be regarded
as an abbreviation of the S-expression %2(%3a%2 . (%3b%2 . (%3c%2 .
(... (%3z . %5NIL%2) ...)))%1.

	1. If we represent sums and products as indicated  above  and
use  %5(MINUS X),  (QUOTIENT X Y)%1, and  %5(POWER X Y)%1  as representations
of  %2-%3x%1,  %3x%2/%3y%1, and  %3x%7y%1  respectively, then

	a. What do the lists 



	%5(PLUS -2 (MINUS 2) (TIMES X (POWER Y 3.3)))


	b.    How    are    the   expressions   %3xyz%2+%53%2(%3u%2+%3v%2)%7-3%1   and
%2(%3xy%2-%3yx%2)/(%3xy%2+%3yx%2)%1 to be represented?

	2. In the above  mentioned  graph  notation,  what  graph  is
represented by the list

	%5((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 %5((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:
	a. (A . NIL)
	b. (A . B)
	c. ((A . NIL) . B)
	d. ((A . B) . ((C . D) . NIL).

	5. Prove that the number of "shapes" of S-expressions
with %3n%1 atoms is %3(2n - 2)!/(n!(n - 1)!)%1.  (The two shapes
of S-expressions with three atoms are %5(A.(B.C))%1 and %5((A.B).C)%1).

	6. The above result can also be obtained by writing %3S#=#A#+#S%4x%3S%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 %3S%72%3#-#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 %3A%7n%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 %3form%1.  LISP functions are constructed
from LISP %3forms%1 which are written in two languages - %3publication
language%1 and %3internal 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 %3object 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

	First,  we have two functions %4a%1 and %4d%1.  %4a %3x%1 is
the a-part of the S-expression %5x%1.  Thus,  %4a%5(A . B) %2= %5A%1,
and %4a%5((A . B) . A) %2= %5(A . B)%1.  %4d %3x%1 is the d-part of
the S-expression %3x%1. Thus %4d%5(A . B) %2= %5B%1, and
%4d%5((A . B) . A) %2= %5A%1.  %4a %3x%1 and %4d %3x%1 are undefined in
basic LISP when %3x%1 is an atom, but they may have a meaning in some
implementations.  The internal forms of %4a %3x%1 and %4d %3x%1 are
%5(CAR X)%1 and %5(CDR X)%1 respectively.  The names %5CAR%1 and %5CDR%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 %5A%1
could either stand for itself or stand for a variable %5A%1 whose
value is wanted.  Even %5(CAR X)%1 is ambiguous since sometime the
S-expression %5(CAR X)%1 itself must be referred to and not the
result of evaluating it.  Internal language avoids the ambiguity
by using %5(QUOTE %3e%5)%1 to stand for the S-exression %3e%1.
Thus the publication language form %4a %5(A B)%1 corresponds
to the internal language form %5(CAR (QUOTE (A.B)))%1 and both
have the value %5A%1 obtained by taking the %4a%1-part of the
S-expression %5(A.B)%1.

	Since  lists  are  a  particular  kind  of  S-expression, the
meanings of  %4a%1  and  %4d%1  for lists are also determined  by  the  above
definitions.  Thus, we have

	%4a%5(A B C D) %2=%4 A


	%4d%5(A B C D) %2= %5(B C D),

%1and we see that, in general,  %4a %3x%1  is the first element of  the  list
 %3x%1, and  %4d %3x%1  is the rest of the list, deleting that first element.

	Notice  that  for S-expressions, the definitions of  %4a %3x%1  and
%4d %3x%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   %4a%1   and   %4d%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  %3cons%2[%3x%2, %3y%2]%1  forms the S-expression whose
a-part and d-part are  %3x%1  and  %3y%1  respectively.  Thus

	%3cons%2[%5(A.B), A%2] = %5((A.B).A).

	%1We  see  that  for  lists,   %3cons%1   is a prefixing operation.
Namely,  %3cons%2[%3x%2, %3y%2]%1  is the list obtained by putting the  element   %3x%1##
onto the front of the list  %3y%1.  Thus

	%3cons%2[%5A, (B C D E)%2] = %5(A B C D E).

%1If we want  %3cons%2[%3x%2, %3y%2]%1  to  be  a  list,  then   %3y%1   must  be  a  list
(possibly the null list  %5NIL%1), and  %3x%1  must be a list or an atom.  In
the case of S-expressions in general, there is no restriction on  the
arguments  of   %3cons%1.   Usually,  we  shall  write   %3x . y%1   instead of
%3cons%2[%3x%2, %3y%2]%1  since this is briefer.

	The internal language form of %3cons[x,y]%1 is %5(CONS X Y)%1.  The name
"CONS" comes from "construct" referring to the way %3cons[x,y]%1 is constructed
from the free storage list.

	The  first  predicate  is   %4at %3x%1.   %4at %3x%1   is  true  if   the
S-expression  %3x%1  is atomic and false otherwise.
The internal form is %5(ATOM X)%1.

	The  second  predicate  is equality of atomic symbols written
%3x %4eq %3y%1. Equality of S-expressions is tested by a  program  based  on
%4eq%1.   Actually   %4eq%1  does a bit more than testing equality of atoms.
Namely,  %3x %4eq %3y%1  is true if and only if the addresses  of  the  first
words  of  the  S-expressions   %3x%1   and  %3y%1  are equal.  Therefore, if
%3x %4eq %3y%1, then  %3x%1  and %3y%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 %5(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.

	%4n %3x%1   is  an  abbreviation for  %3x %4eq %5NIL%1.  It rates a special
notation because  %5NIL%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  %5NIL%1.
Its internal form is %5(NULL X)%1.

    The notation %3list%2[%3x1, x2, . . . , xn%2]%1 is used to denote the
composition of %3cons%1's that forms a list from its elements.  Thus

	%3list[x, y, z] = cons[x, cons[y, cons[z, %5NIL%3]]]%1

and forms a list of three elements out of the quantities %3x, y, %1 and
%3z%1.  We often write %2<%3x y . . . z%2>%1 instead of %3list%2[%3x, y, .
 . . , z%2]%1 when this will not cause confusion.  The experienced
implementer of programming languages will expect that since %3list%1 has a
variable number of arguments, its implementation will pose problems.  He
will be right.  The internal form of %3<x y ... z>%1 is %5(LIST X Y ...

	Compositions of %4a%1 and %4d%1 are written by concatenating the
letters %4a%1 and %4d%1.  Thus, it is easily seen that %4ad %3x%1 denotes
the second element of the list %3x%1, and %4add %3x%1 denotes the third
element of that list.  The internal forms of these functions are %5CADR%1
and %5CADDR%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 %3subst%1 taking three arguments has been defined.
It may be used in forms like %3subst[x,y,z]%1 having internal form
%5(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 %3subst[x,y,%4a z%3] . subst[x,y,%4d %3z]%1 involving
a user defined function %3subst%1.  Its internal form is
.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 %3conditional form%1)

	%4if %3p %4then %3a %4else %3b

%1is evaluated as follows:  First  %3p%1  is evaluated and determined to be
true or false.  If  %3p%1  is true, then  %3a%1  is evaluated and  its  value
is  the  value  of  the  expression.   If   %3p%1   is false, then  %3b%1  is
evaluated and its value is the value of the expression.  Note that if
%3p%1  is true,  %3b%1  is never evaluated, and if  %3p%1  is false, then  %3a%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

	%2|%3x%2| = %4if %3x%2<%50 %4then %2-%3x %4else %3x.

%1A more general form of conditional expression is

	%4if %3p %4then %3a %4else if %3q %4then %3b . . .  %4else if %3s %4then %3d %4else %3e.

%1There  can  be  any  number  of  terms;  the  value  is determined by
evaluating the propositional terms  %3p,  q%1, etc. until a true term  is
found;  the value is then that of the term following the next %4then%1.
If none of the propositional terms is true, then the value is that of
the term following the %4else%1.

	The function graphed in figure 4 is described by the equation

	%3tri%2[%3x%2] = %4if %3x%2<-%51 %4then %50 %4else if %3x%2<%50 %4then %51%2+%3x
%4else if %3x%2<%51 %4then %51%2-%3x %4else %50.
.NARROW 0,-1000

∞                                    ~
∞                                    ~
∞                                    ~
                                 ≤'∞ ~∞ `≥
                               ≤'∞   ~∞   `≥
                             ≤'∞     ~∞     `≥
                            '∞       ~∞       `
∞                        (-1,0)      ~      (1,0)
∞                                    ~
∞                                    ~

                                Figure 4.

	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

	%5(COND (p1 e1) (p2 e2) ... (pn en))%1

with any number of terms.  Its value is determined by evaluating the
%5p%1's successively until one is found which is true.  Then the
corresponding %5e%1 is taken as the value of the conditional expression.
If none of the %5p%1's is true, then the value of the conditional
expression is undefined.  Thus all the %5e%1's are treated the same
which makes programs for interpreting or compiling conditional
expressions easier to write.  Putting parentheses around each %5p-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  %5(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

	%4if n %3x %4then %5NIL %4else %4a %3x . append[%4d %3x,y]%1

involving a yet to be defined function %3append%1.  The internal
form of this is

%5(COND ((NULL X) NIL) (T (CONS (CAR X) (APPEND (CDR X) Y))))%1.

One would normally have expected to write %5(QUOTE NIL)%1 and
%5(QUOTE T)%1, but there is a special convention that %5NIL%1
and %5T%1 may be written without %5QUOTE%1.  This means that
these symbols cannot be used as variables.  The value of %5T%1
is the propositional constant %4true%1, i.e. it is always true
so that it is impossible to "fall off the end" of a conditional
expression with %5T%1 as its last %5p%1.  It is the translation
into internal form of the final %4else%1 of a conditional
.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   %2∧%1,  %2∨%1, and  %2¬%1  respectively, for these
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:

	%5T%2∧%5T %2= %5T
	T%2∧%5F %2= %5F
	F%2∧%5T %2= %5F
	F%2∧%5F %2= %5F

	T%2∨%5T %2= %5T
	T%2∨%5F %2= %5T
	F%2∨%5T %2= %5T
	F%2∨%5F %2= %5F

 	%2¬%5T %2= %5F
	%2¬%5F %2= %5T.

	Since both ∧ and ∨ are associative we can write Boolean forms
like %3p1∧p2∧p3%1 without worrying about grouping.  The internal forms
are %5(AND p1 p2 ... pn)%1, %5(OR p1 p2 ... pn)%1 and %5(NOT p)%1.
It is also customary to use %5NIL%1 instead of %5F%1, because in most
LISP systems both Boolean %4false%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

	%1The  Boolean  operators  can  be  described  by   conditional
expressions in the following way:

	%3p%2∧%3q %2= %4if %3p %4then %3q %4else %5F
	%3p%2∨%3q %2= %4if %3p %4then %5T %4else %3q
	%2¬%3p %2= %4if %3p %4then %5F %4else %5T.

%1Note that if  %3p%1  is false  %3p%2∧%3q%1  is false independent of the value  of
%3q%1,  and  likewise  if  %3p%1  is true, then  %3p%2∨%3q%1  is true independent of
%3q%1.  If  %3p%1  has been evaluated and found to be false, then   %3q%1   does
not  have  to  be evaluated at all to find the value of  %3p%2∧%3q%1, and, in
fact, LISP does not evaluate  %3q%1  in this case.  Similarly,  %3q%1  is not
evaluated  in  evaluating   %3p%2∨%3q%1  if  %3p%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

	%4 if n %3x ∨ %4n d %3 x %4then %3x %4else %4a %3x . alt %4dd %3x%1

the internal form of which is

    %5(COND ((OR (NULL X) (NULL (CDR X))) X) (T (CONS (CAR X) (ALT (CDDR

.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 %4go to%1's.  In LISP, programs are mainly expressed  in  the
form of recursively defined functions.  We begin with an example.

	The  function   %3alt%2[%3x%2]%1   gives  a  list  whose  elements  are
alternate elements of the list  %3x%1  beginning with the first.  Thus

	%3alt%2[%5(A B C D E)%2] = %5(A C E),

	%3alt%2[%5(((A B) (C D))%2] = %5((A B)),

	%3alt%2[%5(A)%2] = %5(A),
	%3alt%2[%5NIL%2] = %5NIL.

	 In LISP %3alt%1 is defined by the equation

    %3alt[x] ← %4if n %3x ∨ %4n d %3x %4then %3x %4else a %3x . alt[%4dd

In case you need a review of our precedence conventions, fully bracketed
it looks like

	%3alt[x] ← %4if %3[%4n%3[x] ∨ %4n%3[%4d%3[x]]] %4then%3 x %4else%3
[%4a%3[x] . alt[%4dd%3[x]]]%1.

	This definition uses no ways of forming expressions that we
haven't introduced previously, but it uses the function %3alt%1 in
the right hand side of its own defining equation.  To get the value of
%3alt x%1 for some particular list, we evaluate the right hand side of
the definition substituting that list for %3x%1 whenever %3x%1 is
encountered and re-evaluating the right hand side with a new %3x%1
whenever a form %3alt e%1 is encountered.

	This process is  best  explained  by  using  it to
evaluate some expressions.

	Consider evaluating %3alt[%5NIL%2]%1.
We do it by evaluating the expression to the right of the  %2←%1  sign
remembering that the variable  %3x%1  has the value  %5NIL%1.  A  conditional
expression  is  evaluated by first evaluating the first propositional
term ¬ in this case  %4n %3x %2∨ %4n d %3x%1. This expression is a disjunction and
in  its evaluation we first evaluate the first disjunct, namely  %4n#%3x%1.
Since  %3x %2= %5NIL,  %4n %3x%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   %3x%1,  and  its  value  is
%5NIL%1,  so the value of  %3alt%2[%5NIL%2]%1  is  %5NIL%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   %4n d %3x%1   or
%3alt%2[%4dd %3x%2]%1, and since  %3x%1 is  %5NIL%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   %3alt%2[%5(A  B)%2]%1.   Since  neither
%4n %3x%1 nor %4n d %3x%1 is true in this case, the disjunction %4n %3x %2∨ %4n d %3x
%1is  false  and  the  value  of  the  expression  is  the   value   of
%4a %3x . alt%2[%4dd %3x%2].     %4a %3x%1 has the value  %5A%1, and %4dd %3x%1 has the value
%5NIL%1, so we must now evaluate  %3alt%2[%5NIL%2]%1, and we already know that the
value   of   this   expression  is   %5NIL%1.  Therefore,  the  value  of
%3alt%2[%5(A B)%2]%1  is that of  %5A.NIL%1  which is  %5(A)%1.

	We can describe this  evaluation  in  a  less  wordy  way  by

	%3alt%2[%5(A B)%2] = %4if n%5(A B) %2∨ %4n d%5(A B) %4then %5(A B) %4else
			%4a%5(A B).%3alt%2[%4dd%5(A B)%2]

		   = %4if %5NIL %2∨ %4n d%5(A B) %4then %5(A B) %4else
			%4a%5(A B).%3alt%2[%4dd%5(A B)%2]

		   = %4if %5NIL %4then %5(A B) %4else
			%4a%5(A B).%3alt%2[%4dd%5(A B)%2]

		   = %4a%5(A B).%3alt%2[%4dd%5(A B)%2]

		   = %5A.%3alt%2[%5NIL%2]

		   = %5A%2.[%4if n%5NIL %2∨ %4nd%5NIL %4then %5NIL %4else

 		   = %5A%2.[%4if %5T %2∨ %4nd%5NIL %4then %5NIL %4else

 		   = %5A%2.[%4if %5T %4then %5NIL %4else

		   = %5A%2.[%5NIL%2]

		   = %5(A).
	%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

	%3alt%2[%5(A B C D E)%2] = %5A.%3alt%2[%5(C D E)%2]

			= %5A%2.[%5C.%3alt%2[%5(E)%2]]

			= %5A.%2[%5C.(E)%2]

			= %5(A C E).

	%1Here are three more examples of recursive functions and their
application: We define  %3last%1  by

	%3last%2[%3x%2] ← %4if n d %3x %4then a %3x %4else %3last%2[%4d %3x%2],

%1and we compute

	%3last%2[%5(A B C)%2] = %4if nd%5(A B C) %4then a%5(A B C) %4else %3last%2[%4d%5(A B C)%2]

		      = %3last%2[%5(B C)%2]

		      = %3last%2[%5(C)%2]

		      = %5C.

%1Clearly   %3last%1   computes  the  last element of a list.  %3last%2[%5NIL%2]%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

	The function  %3subst%1  is defined by

	%3subst%2[%3x, y, z%2] ← %4if at %3z %4then %2[%4if %3z %4eq %3y %4then %3x %4else %3z%2]
%4else %3subst[x,y,%4a %3z].subst[x,y,%4d %3z]%1.

We have

	%3subst%2[%5(A.B), X, ((X.A).X)%2] =

		= %3subst%2[%5(A.B), X, (X.A)%2]%3subst%2[%5(A.B), X, X%2]

		= [%3subst%2[%5(A.B), X, X%2].%3subst%2[%5(A.B), X, A%2]].%5(A.B)

		%2= [[%5(A.B)%2].%5A%2].%5(A.B)%2]

		= %5(((A.B).A).(A.B)).

%3subst%1  computes the result of substituting the S-expression   %3x%1   for
the  atom  %3y%1  in the S-expression  %3z%1.  This operation is important
in all kinds of symbolic computation.

	The function %3append[x,y]%1 which gives the  concatenation  of the lists
%3x%1 and %3x%1 is also important.  It is also denoted by the
infixed expression  %3x%2*%3y%1  since it
is associative.  We have the examples

	%5(A B C)%2*%5(D E F) %2= %5(A B C D E F),


	%5NIL%2*%5(A B) %2= %5(A B) %2= %5(A B)%2*%5NIL,

%1and the formal definition

	%3x%2*%3y %2← %4if n %3x %4then %3y %4else %2[%4a %3x].[[%4d %3x%2]*%3y%2].

	%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  %3equal%1  by

	%3equal[x,y] ← x %4eq %3y ∨ [¬%4at %3x ∧ ¬%4at %3y ∧
equal[%4a %3x,%4a %3y] ∧ equal[%4d %3x, %4d %3y]]%1.

%3equal[x,y]%1 is true if and only if   %3x%1   and   %3y%1   are  the  same
S-expression,  and  the  use  of this predicate makes up for the fact
that the basic predicate  %4eq%1  is guaranteed  to  test  equality  only
when  one  of the operands is known to be an atom.  We shall also use
the infixes  %2=%1  and  %2≠%1.

 	Membership of an S-expression  %3x%1  in a list  %3y%1  is tested by

	%3member%2[%3x, y%2] ← ¬%4n %3y %2∧ [[%3x %2= %4a %3y%2] ∨ %3member%2[%3x, %4d %3y%2]].

%1This relation is also denoted by %3x#ε#y%1.  Her? are some computations:

	%3member%2[%5B, (A B)%2] = ¬%4n %5(A B) %2∧ [[%5B %2= %4a %5(A B)%2]
			    ∨ %3member%2[%5B, %4d %5(A B)%2]],

			= %3member%2[%5B, (B)%2]

			= %5T.
	%1Sometimes  a  function  is defined with the help of auxiliary
functions.  Thus, the reverse of a list  %3x%1 , (e.g.   %3reverse%2[%5(A B C
D)%2] = %5(D C B A)%1), is given by

	%3reverse%2[%3x%2] ← %3rev%2[%3x, %5NIL%2]


	%3rev%2[%3x, y%2]   ← %4if n %3x %4then %3y %4else %3rev%2[%4d %3x%2, [%4a %3x%2].%3y%2].

%1A computation is

	%3reverse%2[%5(A B C)%2] = %3rev%2[%5(A B C), NIL%2]

 			 = %3rev%2[%5(B C), (A)%2]

			 = %3rev%2[%5(C), (B A)%2]

			 = %3rev%2[%5NIL, (C B A)%2]

			 = %5(C B A).

	%1A more elaborate example of recursive definition is given by

	%3flatten%2[%3x%2] ← %3flat%2[%3x, %5NIL%2]

	%3flat%2[%3x, y%2] ← %4if at %3x %4then %3x.y
			      %4else %3flat%2[%4a %3x, flat%2[%4d %3x, y%2]].

%1We have

	%3flatten%2[%5((A.B).C)%2] = %3flat%2[%5((A.B).C), NIL%2]

			   = %3flat%2[%5(A.B), %3flat%2[%5C, NIL%2]]

			   = %3flat%2[%5(A.B), (C)%2]

			   = %3flat%2[%5A, %3flat%2[%5B, (C)%2]]

			   = %3flat%2[%5A, (B C)%2]

			   = %5(A B C).
%1The  reader  will see that the value of  %3flatten%2[%3x%2]%1  is a list of the
atoms  of  the  S-expression   %3x%1    from   left   to   write.    Thus
%3flatten%2[%5((A B) A)%2] = %5(A B NIL A NIL)%1.

	Many  functions  can be conveniently written in more than one
way.  For example, the function   %3reverse%1   mentioned  above  can  be
written without an auxiliary function as follows:

	%3reverse%2[%3x%2] ← %4if n %3x %4then %5NIL %4else %3reverse%2[%4d %3x%2]*%5<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:

	%3n%2! ← %4if %3n%2=%50 %4then %51 %4else %3n%2(%3n%2-%51%2)!


	%3gcd%2(%3m, n%2) ← %4if %3m%2>%3n %4then %3gcd%2(%3n, m%2) %4else if %3m%2=%50 %4then %3n
			%4else %3gcd%2(%3n mod m, m%2)
%1where  %3n mod m%1  denotes the remainder when  %3n%1  is divided by  %3m%1   and
may itself be expressed recursively by

	%3n mod m %2← %4if %3n%2<%3m %4then %3n %4else %2(%3n%2-%3m%2) %3mod 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

	%5(DE <function name> <list of variables> <right hand side>)%1.

In these LISPs, the above definition of %3subst%1 is

	%5(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 %3alt%1 is

	%5(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 %5DEFPROP%1 notation
will be explained after λ-expressions have been introduced.

%1                              Exercises

	1. Consider the function  %3drop%1  defined by

	%3drop%2[%3x%2] ← %4if n %3x %4then %5NIL %4else %2<%4a %3x%2>.%3drop%2[%4d %3x%2].

%1Compute (by hand)  %3drop%2[%5(A B C)%2]%1.  What does  %3drop%1  do  to  lists  in
general?  Write %3drop%1 in internal notation using %5DE%1.

	2. What does the function

	%3r2%2[%3x%2] ← %4if n %3x %4then %5NIL %4else %3reverse%2[%4a %3x%2].%3r2%2[%4d %3x%2]

%1do to lists of lists?  How about

	%3r3%2[%3x%2] ← %4if at %3x %4then %3x %4else %3reverse%2[%3r4%2[%3x%2]]

	%3r4%2[%3x%2] ← %4if n %3x %4then %5NIL %4else %3r3%2[%4a %3x%2].%3r4%2[%4d %3x%2]?

	%13. Compare

	%3r3'%2[%3x%2] ← %4if at %3x %4then %3x %4else %3r3'%2[%4d %3x%2]*<%3r3'%2[%4a %3x%2]>

%1with the function  %3r3%1  of the preceding example.

	4. Consider  %3r5%1  defined by

	%3r5%2[%3x%2] ← %4if n %3x %2∨ %4n d %3x %4then %3x
		%4else %2[%4a %3r5%2[%4d %3x%2]]
			. %3r5%2[%4a %3x . r5%2[%4d %3r5%2[%4d %3x%2]]].
%1Compute  %3r5%2[%5(A B C D)%2]%1.  What does  %5r5%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.

	It is common to use phrases like "the function  2%3x%2+%3y%1".   This
is  not a precise notation because we cannot say  2%3x%2+%3y%2(%53, 4%2)%1  and know
whether the desired  result  is   2%Bπ.%13+4   or   2%Bπ.%14+3   regarding  the
expression  as a function of two variables.  Worse yet, we might have
meant a one-variable function of  %3x%1  wherein  %3y%1   is  regarded  as  a

	The problem  of  giving  names  to  functions  is  solved  by
Church's   λ-notation.    In   the  above  example,  we  would  write
%2λ%3x y%2: %52%3x%2+%3y%1  to denote  the  function  of  two  variables  with  first
argument   %3x%1   and  second  argument   %3y%1  whose value is given by the
expression  2%3x%2+%3y%1.  Thus,

	%2[λ%3x y%2: %52%3x%2+%3y%2][%53, 4%2] = %510%1.

%1Likewise,   %2[λ%3y x%2: %52%3x%2+%3y%2][%53, 4%2] = %511%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   %2λ%3x y%2: %52%3x%2+%3y%1   represents  the  same   function   as
%2λ%3y x%2: %52%3y%2+%3x%1 or %2λ%3u v%2: %52%3u%2+%3v%1 , but in the function of one argument
%2λ%3x%2: %52%3x%2+%3y%1 , we cannot replace the variable  %3x%1  by %3y%1 , though we could
replace it by  %3u%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(%52%3x%2+%51%2)%74%2+%53%2(%52%3x%2+%51%2)%73%1  can be written
%2[λ%3w%2: %3w%74%2+%53%3w%73%2][%52%3x%2+%51%2]%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

	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  %3f%1  to each element  of  the  list.
This can be done using the function  %3mapcar%1  defined by

	%3mapcar%2[%3x, f%2] ← %4if n %3x %4then %5NIL %4else %3f%2[%4a %3x%2]
 . %3mapcar%2[%4d %3x, f%2].

%1Suppose the operation we want to perform is squaring, and we want  to
apply it to the list  %5(1 2 3 4 5 6 7)%1.  We have

	%3mapcar%2[%5(1 2 3 4 5 6 7), %2λ%3x%2: %3x%72%2] = %5(1 4 9 16 25 36 49).

	%1A more generally useful operation than  %3mapcar%1 is %3maplist%1
in  which  the  function is applied to the successive sublists of the
list rather than to the elements.  %3maplist%1  is defined by

	%3maplist%2[%3x, f%2] ← %4if n %3x %4then %5NIL %4else %3f%2[%3x%2]
 . %3maplist%2[%4d %3x, f%2].

	%1As  an  application  of  %3maplist%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

	<expression> ::= <variable> | <integer> |
			 (PLUS <explist>) | (TIMES <explist>)

	<explist>    ::= <expression> | <expression><explist>
Here,  %5PLUS%1  followed by a list of arguments denotes the sum of these
arguments and  %5TIMES%1  followed by a list of arguments  denotes  their
product.   The  function   %3diff%2[%3e, v%2]%1  gives the partial derivative of
the expression  %3e%1  with respect to the variable  %3v%1. We have

	%3diff%2[%3e, v%2] ← %4if at %3e %4then %2[%4if %3e %4eq %3v %4then %51 %4else %50%2]
		%4else if a %3e %4eq %5PLUS %4then
			%5PLUS . %3mapcar%2[%4d %3e%2, λ%3x%2: %3diff%2[%3x, v%2]_]
		%4else if a %3e %4eq %5TIMES %3then
			%5PLUS.%3maplist%2[%4d %3e%2, λ%3x%2: %5TIMES
  			      .	%3maplist%2[%4d %3e%2, λ%3y%2: %4if %3x %4eq %3y %4then
					%3diff%2[%4a %3y, v%2] %4else a %3y%2]].
%1The  term  that  describes  the  rule  for  differentiating  products
corresponds to the rule
.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)

	%2∂/∂%3v    %3e%6i%2 =       [%4if %3i%2=%3j %4then %2∂%3e%6j%2/∂%3v %4else %3e%6j%2].
.COMMENT  ******************************************!!!!!!!!!!!!**********

and   %3maplist%1   has  to be used rather than  %3mapcar%1  since whether to
differentiate in forming the product is determined by equality of the
indices   %3i%1   and   %3j%1   rather  than equality of the terms  %3e%6i%1  and

	Two more useful functions with functions as arguments are the
predicates  %3andlis%1  and  %3orlis%1  defined by the equations

	%3andlis%2[%3u, p%2] ← %4n %3u %2∨ [%3p%2[%4a %3u%2] ∧ %3andlis%2[%4d %3u, p%2]]


	%3orlis%2[%3u, p%2] ← ¬%4n %3u %2∧ [%3p%2[%4a %3u%2] ∨ %3orlis%2[%4d %3u, p%2]].

	The internal form for a λ-expression is

	%5(LAMBDA <list of variables> <expression to be evaluated>)%1.

Thus %2λ x: diff[x,v]%1 is written %5(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 %5FUNCTION%1.  Thus the above definition of %3diff%1 translates

		((ATOM E) (COND ((EQ E V) 1) (T 0)))
(LAMBDA (X) (DIFF X V))))))
(COND ((EQ X Y) (DIFF (CAR Y) V)) (T (CAR Y))))))))))))))%1.

	Another way of writing function definitions in internal notation
uses %5LAMBDA%1 to make a function of the right side of a definition.

It is like writing %3subst%1 and %3alt%1 as

	%3subst = λx y z.[%4if at %3z %4then %3[%4if %3z %4eq%3 y %4then%3 x
%4else %3z] %4else %3subst[x,y,%4a%3 z] . subst[x,y,%4d%3 z]]%1


	%3alt = λx.[%4if n %3x ∨ %4n d %3x %4then%3 x %4else a %3x .alt %4dd%3 x]%1.

The definitions of %3subst%1 and %3alt%1 take the forms

(T (CONS (SUBST X Y (CAR Z)) (SUBST X Y (CDR Z)))))))%1,


(T (CONS (CAR X) (ALT (CDDR X)))))))%1.

	The general form is %5(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  %3diff%2[%5(TIMES X (PLUS Y 1) 3), X%2]%1  using  the  above
definition  of  %3diff%1.  Now do you see why algebraic simplification is

	2. Compute  %3orlis%2[%5((A B) (C D) E), %4at%2]%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  %4label%2[%3f, e%2]%1  to denote the expression  %3e%1  but where
occurrences of  %3f%1  within  %3e%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

	%3glub%2[%5((A B C) (A B C D) (X Y Z))%2] = %5((A C) (A C) (X Z)).%1

We can make the definition

	%3glub%2[%3x%2] ← %3mapcar%2[%3x, %4label%2[%3alt%2, λ%3x%2: %4if n %3x %2∨ %4n d %3x %4then %3x
					%4else a %3x . alt%2[%4dd %3x%2]]].

	The internal form of %3label[<name>,<function expression>]%1
is %5(LABEL <name> <function expression>)%1, so that the internal form
of the definition of %3glub%1 is

(NULL X) (NULL (CDR X))) X) (T (CONS (CAR X) (ALT (CDDR X))))))))%1.

	The identifier  %3alt%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
%5(1 3 5)%1, %5(3.5 6.1 -7.2E9)%1, and %5(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 %5E%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 %5(1 . 2)%1
is wanted, the spaces around the dot distinguish it from the
list %5(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 %3x%7y%1 when typographically convenient and
the linear Algol notation %3x↑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

	%3length u ← %4if n %3u %4then %50 %4else %51 %3+ length %4d %3u%1.

	The internal notation for numerical functions is that used
in the examples given: %5(PLUS X Y ... Z)%1 for %3x+y+...+z%1,
%5(TIMES X ... Z)%1 for %3xy...z%1, %5(MINUS X)%1 for %3-x%1,
%5(DIFFERENCE X Y)%1 for %3x-y%1, %5(QUOTIENT X Y)%1 for %3x/y%1,
and %5(POWER X Y)%1 for %3x%7y%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 %5EQUAL, 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 %3numberp%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 %3association list%1, having the form

(<variable1>.<value1>) ... (<variablen>.<valuen>)),

e.g. %5((X . 5) (Y . 9.3) (Z . 2.1))%1.

	The function is

	%3numval[e,a] ← %4if %3numberp e %4then %3e
%4else if at %3e %4then d %3assoc[e,a]
%4else if a %3e %4eq %5PLUS %4then %3evplus[%4d %3e,a]
%4else if a %3e %4eq %5TIMES %4then %3evtimes[%4d %3e,a]%1


	%3evplus[u,a] ← %4if n %3u %4 then %50 %4else %3numval[%4a %3u,a] +
evplus[%4d %3u,a]%1,

	%3evtimes[u,a] ← %4if n %3u %4 then %51 %4else %3numval[%4a %3u,a] +
evtimes[%4d %3u,a]%1,


	%3assoc[x,a] ← %4if n %3a %4 then %5NIL
%4else if aa %3a %4eq %3x %4then da %3a %4else %3assoc[x,%4d %3a]%1.

.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  %3n%2!%1.  For
what argument is the value of the function immediate.   Clearly,  for
%3n %2= %50  or  %3n %2= %51%1, the value is immediately seen to be  1.  Moreover,
we can get the value for an arbitrary  %3n%*  if we know  the  value  for
%3n%2-%51.   Also, we see that knowing the value for  %3n %2= %51  is redundant,
since it can be obtained from the  %3n %2= %50  case by the  same  rule  as
gets  it  for  a  general  %3n%*  from the value for  %3n%2-%51%1.  All this talk
leads to the simple recursive formula:

	%3n%2! ← %4if %3n %2= %50 %4then %51 %4else %3n%2(%3n%2-%51%2)!.

	%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 %3top-down%1 and %3bottom-up%1 programming
with %3static%1 corresponding to %3top-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  %3n%2!:

	%4integer procedure %3factorial%2(%3n%2); %4integer %3s%2;
	%3s %2:= %51%2;
%3loop%2:	%4if %3n %2= %50 %4then go to %3done%2;
	%3s %2:= %3n%2*%3s%2;
	%3n %2:= %3n%2-%51%2;
	%4go to %3loop%2;
%3done%2:	%3factorial %2:= %3s%2;
	%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:

	%3n%2! ← %3fact%2(%3n%2, %3s%2),


	%3fact%2(%3n%2, %3s%2) ← %4if %3n %2= %50 %4then %3s %4else %3fact%2(%3n%2-%51%2, %3n%2*%3s%2).

%1In  fact,  compilers should produce the same object code from the two
.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 %4d%*-part of
that argument.  Consider, for example,  %3u%2*%3v%1, the concatenation of the
lists  %3u%*  and %3v%*.  The result is immediate for  the  case   %4n %3u%1   and
otherwise depends on the result for  %4d %3u%1.  Thus, we have

	%3u%2*%3v %2← %4if n %3u %4then %3v %4else a %3u %2. [%4d %3u %2* %3v%2].

%1On the other hand, if we had tried to recur on  %3v%1  rather than on  %3u%1
we would not have been successful.  The result would be immediate for
%4n %3v%1, but  %3u%2*%3v%1  cannot be constructed in any direct way from   %3u%2*%4d %3v%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  %3cons%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.

	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

	%5((X . (PLUS A B)) (Y . C) (Z . (TIMES U V)),

%1which would print as

	%5((X PLUS A B)) (Y . C) (Z TIMES U V)),

%1pairs  %5X%1  with  %5(PLUS A B),  Y%1  with  %5C%1, etc. We need a  function  to
tell  whether  anything  is  associated  with  the  atom   %3x%1   in the
association list  %3a%1, and, if so, to tell us what. We have

	%3assoc%2[%3x, a%2] ← %4if n %3a %4then %5NIL %4else if %3x %4eq aa %3a %4then a %3a
		%4else %3assoc%2[%3x, %4d %3a%2].
%1Its value is   %5NIL%1   if  nothing  is  associated  with   %3x%1   and  the
association pair otherwise.  E.g.  %3assoc%2[%5X, ((X.W) (Y.V))%2] = %5(X.W)%1.

	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 %5NIL%1.  Thus

	%3reverse%2[%3u%2] ← %3rev1%2[%3x, %5NIL%2],


	%3rev1%2[%3u, v%2] ← %4if n %3u %4then %3v %4else %3rev1%2[%4d %3u, %4a %3u . v%2].

%3reverse%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

	%3reverse%2[%3u%2] ← %4if n %3u %2∨ %4n d %3u %4then %3u %4else
		a %3reverse%2[%4d %3u%2] . %3reverse%2[%4a %3u. %3reverse%2[%4d %3reverse%2[%4d %3u%2]]].


	1. Using the function  %3member%2[%3x, u%2]%1  defined in Chapter I
which  may also be written  %3x %2ε %3u%1, write function definitions for the
union  %3u %2∪ %3v%1  of lists  %3u%1  and  %3v%1, the intersection  %3u %2∩ %3v%1,  and  the
set  difference   %3u%2-%3v%1.    What  is  wanted  should  be clear from the

	%5(A B C) %2∪%5 (B C D) %2=%5 (A B C D),

	(A B C) %2∩%5 (B C D) %2=%5 (B C),


	%5(A B C) %2-%5 (B C D) %2=%5 (A).

%1Pay  attention  to getting correct the trivial cases in which some of
the arguments are %5NIL%1.  In general, it  is  important  to  understand
clearly the trivial cases of functions.

	2.  Suppose   %3x%1   takes  numbers  as  values and  %3u%1  takes as
values lists of numbers in ascending order, e.g.  %5(2 4 7)%1.   Write  a
function   %3merge%2[%3x, u%2]%1   whose  value  is obtained from that of  %3u%1  by
putting     %3x%1     in     %3u%1     in    its    proper    place.     Thus
%3merge%2[%53, (2 4)%2] = %5(2 3 4)%1, and  %3merge%2[%53, (2 3)%2] = %5(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   %3merge%1, write a function  %3sort%1  that transforms an
unordered list into an ordered list.

	5. Write a function  %3goodsort%1  that  sorts  a  list  using  a
number  of  comparisons  proportional  to   %3n log n%1, where  %3n%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   %3subst%1
was defined by

	%3subst%2[%3x, y, z%2] ← %4if at %3z %4then %2[%4if %3z %4eq %3y %4then %3x %4else %3z%2]
			%4else %3subst%2[%3x, y, %4a %3z%2] . %3subst%2[%3x , y , %4d %3z%2].
	%1Two other examples are  %3equal%1  which gives  the  equality  of
S-expressions  and   %3flat%1  which spreads an S-expression into a list
of atoms:  They are defined by

	%3x%2=%3y %2← %3x %4eq %3y %2∨ [¬%4at %3x %2∧ ¬%4at %3y %2∧ %4a %3x %2= %4a %3y %2∧ %4d %3x %2= %4d %3y%2],


	%3flat%2[%3x%2] ← %3flata%2[%3x, %5NIL%2]


	%3flata[x,u] ← %4if at %3x %4then %3x.y %4else %3flata[%4a %3x,flata[%4d %3x,y]]%1.

.if lines < 7 then skip to column 1

	1. Write a predicate to tell whether a given atom occurs in a
given S-expression, e.g.  %3occur[%5B, ((A.B).C)%2] = %5T%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

	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  %5(PLUS X Y)%1  and  %5(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:

	%3value%2[%3e, a%2] ← %4if at %3e %4then d %3assoc%2[%3e, a%2]
		%4else if a %3e %4eq %5PLUS %4then %3value%2[%4ad %3e, a%2] + %3value%2[%4add %3e, a%2]
		%4else if a %3e %4eq %5TIMES %4then %3value%2[%4ad %3e, a%2] * %3value%2[%4add %3e, a%2].
%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:

	%3value%2[%3e, a%2] ← %4if at %3e %4then d %3assoc%2[%3e, a%2]
			%4else if a %3e %4eq %5PLUS %4then %3vplus%2[%4d %3e, a%2]
			%4else if a %3e %4eq %5TIMES %4then %3vtimes%2[%4d %3e, a%2].


	%3vplus%2[%3u, a%2] ← %4if n %3u %4then %50 %4else %3value%2[%4a %3u, a%2] + %3vplus%2[%4d %3u, a%2],


	%3vtimes%2[%3u, a%2] ← %4if n %3u %4then %51 %4else %3value%2[%4a %3u, a%2] * %3vtimes%2[%4d %3u, a%2].
%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.
.<<\\M0NGR25;\M1BDJ25;\M2BDR25X;\M3SUB;\M4NGR30;\M5NGR40;\M6SUP;%1 >>
.ss Tree search recursion.

	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

	%3search p %2← %4if %3lose p %4then %1LOSE
			 %4else if %3ter p %4then %3p %4else %3searchlis%2[%*successors p%2]%1


	%3searchlis u %2← %4 if n %3u %4then %1LOSE %4else %3%2{%*search %4a
 %3u%2}[%*λx%2:%* %4if %3x %2= %1LOSE %4then %3searchlis %4d %3u %4else %3x%2]%*.%1

In the applications, we  start with a position %3p%60%1,  and we
are looking for  a win in the successor tree of %3p%60%1.  Certain
positions lose and  there is  no point looking  at their  successors.
This is decided  by the predicate %3lose%1. A position  is a win if
it  doesn't  lose  and  it  satisfies  the  predicate %3ter%1.  The
successors of a position  is given by the  function %3successors%1,
and  the  value  of %3search  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
%3successors%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

	%3lose p %2← %4a %3p %2ε %4d %3p,

	ter p %2← [%4a %3p %2=%* final%2]%*, %1


	%3successors p %2←%* mapcar%2[%4d %3assoc%2[%4a %3p, graph%2]%*, λx%2:%* x.p%2]%*.%1

	Another example is the so-called %3Instant 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 %3search%1 for this purpose,
we must define the representation of positions and give the functions
%3lose, ter, %1and %3successors%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 %3puzz%1.

	We now have

	%3p%60%1 %2=%* (NIL NIL NIL NIL),

	%3lose p %2←%* orlis%2[%*p, λu%2:%* %4a %3u %2ε %4d %3u%2]%*,

	ter p %2← [%*length %4a %3p %2=%* 4%2]%1,


	%3successors p %2←%* mapcar%2[%4a %3nth%2[%*puzz, 1 + length %4a %3p%2]%*
, λx%2:%* mapcar2%2[%*p, x, λyz%2:%* z.y%2]]%*, %1


	%3mapcar2%2[%*u, v, f%2] ← %4if n %3u %4then %1NIL %4else
f%2[%4a %3u, %4a %3v%2]%* . mapcar2%2[%4d %3u, %4d %3v, f%2]%*.%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: 

	%3puzz1 %2← %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\.

	%3puzz2 %2←%* cycles%2[%1(2 3 4 5)%2]%*%2*%*%3cycles%2[%*(%1(2 5 4 3)%2]%*%2*%*
%3cycles%2[%*(1 2 6 4)%2]%*
	          %2*%*cycles%2[%*(1 4 6 2)%2]%*%2*%*cycles%2[%*(1 3 6 5)%2]%*%2*%*cycles%2[%*(1 5 6 3)%2]%*, %1

where the function %3cycles%1 is defined by

	%3cycles u %2←%* maplist%2[%*u, λx%2:%* x%2*%*upto%2[%*u, x%2]]%1

with the auxiliary function

	%3upto%2[%*u, x%2] ← %4if %3x %4eq %3u %4then %1NIL %4else a
 %3u . upto%2[%4d %3u, x%2]%*.%1

Next we create for each block a list of substitutions expressing the
colors of the six numbered faces.  We have

	%3puzz3 %2←%* mapcar%2[%*puzz1, λx%2:%* prup%2[%1(1 2 3 4 5 6), %3x%2]]%*, %1

and we use these substitutions to get for each block the list of 24 orientations
of the block. Thus

	%3puzz4 %2←%* mapcar%2[%*puzz3, λs%2:%* sublis%2[%*s, puzz3%2]]%*.

puzz4%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 seventeen.  So
we finally get

	%3puzz %2← (%4a %3nth%2[%4a %3puzz4, 1%2] %4a %3nth%2[%4a %3puzz4, 9%2]
%4a %3nth%2[%4a %3puzz4, 17%2]) . %4d %3puzz4.%1

The program when compiled runs about 11 seconds on the PDP-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 %4or%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 %4and%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 %3puzz%1 can be formed from the
old one by the assignment

	%3puzza %2←%* mapcar%2[%*puzz, λx%2:%* mapcar%2[%*x, zap%2]]%*, %1


	%3zap v %2← %4if n %3v %4then %50 %4else %3poo %4a %3v %2+
16 * %3zap %4d %3v, %1\.


	%3poo x %2← %4if %3x%2=%1R %4then %31 %4else if %3x%2=%1W %4then
 %12 %4else if %3x%2=%1G %4then %14 %4else %18.

Now we need the new functions %3lose, ter, %1and
%3successors%1.  These are

	%3lose p %2← %4false%3,

	%3ter p %2← [%*length p %2=%* 5%2]%*, %1


	%3successors p %2←%* mapchoose%2[%4a %3nth%2[%*puzza, length p%2]%*,
λx%2:%* %4a %3p %4and %3x %2=%* 0, λx%2:%* %2[%4a %3p %4or %3x%2]%* . p%2]%*.%1


	%3mapchoose%2[%*u, pred, fn%2] ← %4if n %3u %4then %1NIL
		%4else if
%3pred %4a %3u %4then %3fn%2[%4a %3u%2]%* . mapchoose%2[%4d %3u
, pred, fn%2] %4
		else %3mapchoose%2[%4d %3u, pred, fn%2]%*.%1

%3lose%1 is trivial, because the %3mapchoose%1 is used to make sure
that only non-losing new positions are generated by %3successors%1.
This version runs in a little less than one second on the PDP-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.

	%3search%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 %3allsol%1 that uses
the same %3lose, ter, %1and %3successors%1 functions as does %3search%1.
The simplest way to write %3allsol%1 is

	%3allsol p %2← %4if %3lose p %4then %1NIL %4else if %3ter p
 %4then %3(p) %4else %3mapapp%2[%*successors p, allsol%2]%*, %1


	%3mapapp%2[%*u, fn%2] ← %4if n %3u %4then %1NIL %4else
%3fn%2[%4a %3u%2]%* . mappap%2[%4d %3u, fn%2]%*.%1

This form of the function is somewhat inefficient because of all the
%3append%1ing.  A more efficient form uses an auxiliary function as follows: 

	%3allsol p %2←%* allsola%2[%*p, %1NIL%2]%*

	%3allsola%2[%*p, found%2] ← %4if %3lose p %4then %3found
					%4else if %3ter p %4then %3p . found
					%4else %3allsolb%2[%*successors p, found%2]%*,

	%3allsolb%2[%*u, found%2] ← %4if n %3u %4then %3found
%4else %3allsolb%2[%4d %3u, allsola%2[%4a %3u, found%2]]%*.%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.

	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

	The   simplest  situation  is  characterized  by  a  function
%3successors%1 that gives the positions that can be reached in  one
move,  a  predicate  %3ter%1  that  tells  when a position is to be
regarded  as  terminal  for  the  given  analysis,  and  a   function
%3imval%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  %3imval%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
%3valmax%1 and %3valmin%1 that give a value to a position
by using %3imval%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: 

	%3maxlis%2[%*u, f%2] ← %4if n %3u %4then %3-%2∞%* %4else %3
max%2[%*f%2[%4a %3u%2]%*, maxlis%2[%4d %3u, f%2]]%*, %1


	%3minlis%2[%*u, f%2] ← %4if n %3u %4then %3%2∞%* %4else %3
min%2[%*f%2[%4a %3u%2]%*, minlis%2[%4d %3u, f%2]]%*.%1

In these functions, -%2∞%* and %2∞%* represent numbers that are smaller and
larger than any actual values that will occur in evaluating %3f%1.
If these numbers are not available, then it is necessary to prime
the function with the values of %3f%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 %3maxlis%1, namely

	%3maxlis%2[%*u, f%2] ←%* maxlisa%2[%*u, -%2∞%*, f%2]%*, %1


	%3maxlisa%2[%*u, x, f%2] ← %3if n %3u %4then %3x %4else
%3maxlisa%2[%4d %3u, max%2[%*x, f%2[%4a %3u%2]]%*, f%2]%*.%1

We now have

	%3valmax p %2← %4if %3ter p %4then %3imval p %4else
%3maxlis%2[%*successors p, valmin%2]%1, 


	%3valmin p %2← %4if %3ter p %4then %3imval p %4else
%3minlis%2[%*successors p, valmax%2]%1.

The best move is now chosen by

	%3movemax p %2←%* bestmax%2[%*succesors p, valmin%2]%*, %1


	%3movemin p %2←%* bestmin%2[%*succesors p, valmax%2]%*, %1


	%3bestmax%2[%*u, f%2] ←%* bestmaxa%2[%4d %3u, %4a %3u, f%2[%4a %3u%2]%*, f%2]%*,

	%3bestmaxa%2[%*u, sofar, valsofar, f%2] ← %4if n %3u %4then %3sofar
		%4else if %3f%2[%4a %3u%2] ≤ %3bestsofar %4then
%3bestmaxa%2[%4d %3u, sofar, bestsofar, f%2]%*
		%4else %3bestmaxa%2[%4d %3u, %4a %3u, f%2[%4a %3u%2]%*, f%2]%*,

	%3bestmin%2[%*u, f%2] ←%* bestmina%2[%4d %3u, %4a %3u, f%2[%4a %3u%2]%*, f%2]%*, %1


	%3bestmina%2[%*u, sofar, valsofar, f%2] ← %4if n %3u %4then %3sofar
		%4else if %3f%2[%4a %3u%2] ≥ %3bestsofar %4then
%3bestmina%2[%4d %3u, sofar, bestsofar, f%2]%*
		%4else %3bestmina%2[%4d %3u, %4a %3u, f%2[%4a %3u%2]%*, f%2]%*.%1

	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.

            ≤ 8
      max ≤'
         αααα 1
  min ≤'  `≥
    ≤'      ` 6
    `≥      ≤ 9
      `≥  ≤'
         αααα X
            ` X

↔%DFigure 2.6%1

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: 

	%3maxval p %2←%* maxval1%2[%*p, -%2∞%*, %2∞%*%2]%*,

	  maxval1%2[%*p, α, β%2] ← %4if %3ter p %4then %3max%2[%*α, min%2[%*β, imval p%2]]%*
 %4else %3maxval2%2[%*successors p, α, β%2]%*, 

	  maxval2%2[%*u, α, β%2] ← {%*minval1%2[%4a %3u, α, β%2]}[%*λw%2:%* %4if %3w %2=%* β %4then
 %3β %4else %3maxval2%2[%4d %3u, w, β%2]]%*, 

	%3minval p %2←%* minval1%2[%*p, -%2∞%*, %2∞%*%2]%*,

	  minval1%2[%*p, α, β%2] ← %4if %3ter p %4then %3max%2[%*α, min%2[%*β, imval p%2]]%*
 %4else %3minval2%2[%*successors p, α, β%2]%*, 

	  minval2%2[%*u, α, β%2] ← {%*maxval1%2[%4a %3u, α, β%2]}[%*λw%2:%* %4if %3w %2=%* α %4then
 %3α %4else %3minval2%2[%4d %3u, α, w%2]%*.%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 %3n%1 moves
deep on a tree that has %3k%1 successors to each position, then minimax looks
at %3k%7n%1 positions while αβ looks at about only %3k%7n/2%1.  Thus a
program that looks at 10%74%1 moves with αβ might have to look at 10%78%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 %3successors%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 %3a posteriori%1 obvious
even though it is %3a priori%1 very difficult.

.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
%3read%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 %3fname%1 SUBR) where
%3fname%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.
.AT 24 ⊂""⊃
.TURN ON "∂"
.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) %2=%* 0 then go to <ef>
JUMPN			∂(I)if c(ac) %2≠%* 0 then go to <ef>
CAME			∂(I)if c(ac) %2=%* c(<ef>) then <skip next instruction>
CAMN			∂(I)if c(ac) %2≠%* 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 
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
	These instructions are adequate for compiling basic LISP code
with  the addition of the subroutine calling pseudo-instrucion. (CALL
%3n%* (E <subr) S) is used for calling the LISP subroutine <subr> with  %3n%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.
Examples of output of LCOM0, LCOM4, and the regular Lisp compiler

For the file containing:



LCOM0 produces the following code:

(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) 
(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) 
(SUB P (C 1 0 1 0)) 

LCOM4 produces the following code:

(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) 
(SUB P (C 1 0 1 0)) 


The ILISP compiler produces the following code:

       (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) 

	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 %3cons%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 #%4a %3u%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.


Annotated listing of LCOM0:


~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.

  (PROG	(Z)
	       (CONS (QUOTE DSK:)
		     (LIST (CONS (CAR FILE) (QUOTE LAP))))))
	       (PROG (PROG)
		     (SETQ PROG
			   (COND ((EQ (CAR Z) (QUOTE DE))
				  (COMP	(CADR Z)
					(CADDR Z)
					(CADDDR Z)))
				  (COMP	(CADR Z)
					(CADR (CADDR Z))
					(CADDR (CADDR Z))))))
		     (OUTC T NIL)
		     (OUTC NIL NIL)

~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.

	    (MKPUSH N 1)
	     (LIST (QUOTE SUB) (QUOTE P) (LIST (QUOTE C) N 0 N 0)))
	    (QUOTE ((POPJ P) NIL))))

~PRUP returns an A-LIST formed by pairing successive elements of
~   VARS with consecutive integers beginning with N.


~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.

	       (MKPUSH N (PLUS M 1))))))

~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.

  (COND	((NULL EXP) (QUOTE ((MOVEI 1 0))))          ~NIL

	((EQ EXP T) (QUOTE ((MOVEI 1 (QUOTE T)))))  ~T

	((ATOM EXP)                                 ~variable
		(QUOTE P))))

	((OR (EQ (CAR EXP) (QUOTE AND))             ~boolean expression
	     (EQ (CAR EXP) (QUOTE OR))
	     (EQ (CAR EXP) (QUOTE NOT)))
	 ((LAMBDA(L1 L2)
		  (LIST (QUOTE JRST) 0 L2)
		  (QUOTE (MOVEI 1 0))

	((EQ (CAR EXP) (QUOTE COND))               ~COND

	((EQ (CAR EXP) (QUOTE QUOTE))              ~QUOTE

	((ATOM (CAR EXP))                          ~function call
	     (LIST (QUOTE SUB) (QUOTE P) (LIST (QUOTE C) N 0 N 0)))
		   (QUOTE S)))))

	((EQ (CAAR EXP) (QUOTE LAMBDA))           ~LAMBDA expression
	     (CADDAR EXP)
	     (LIST (QUOTE SUB) (QUOTE P) (LIST (QUOTE C) N 0 N 0)))))

	(T NIL)))                                 ~oops

~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.

		 (QUOTE ((PUSH P 1)))

~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.

	       (LOADAC (PLUS N 1) (PLUS K 1))))))

~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.

		   (COMCOND (CDR U) M L VPR)))

~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.

  (COND	((ATOM P)                                        ~simple variable

	((EQ (CAR P) (QUOTE AND))                        ~conjunction
			  (LIST L1)))

	((EQ (CAR P) (QUOTE OR))                         ~disjunction
			  (LIST L1)))

	((EQ (CAR P) (QUOTE NOT))                        ~negation

	(T                                               ~other expression

~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).


.ss The function %3eval%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 %3eval%1 is a universal LISP function in the
sense that any computation done by any LISP function can be done by
%3eval%1 when %3eval%1 is given suitable arguments.

	%3eval%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 %3eval%1, and we can start our computations with
the second argument NIL.

	To illustrate this, suppose we want to apply the function %3alt%1
to the list (A B C D E), i.e. we wish to evaluate %3alt%2[%5(A B C D E)%2]%1.
This can be obtained by computing

	%3eval%2[%5((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%2]%1, 
and gives the expected result (A C E).
The second argument of %3eval%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

	%3eval%2[%5(CAR X), ((X.(B.C)) (Y.A) (X.B))%2] = %5B%1, 

i.e. we have evaluated %4a %3x%1 with %3 x%2 = %5(B.C)%1.  The value associated
with a variable in such a list of pairs is computed by the auxiliary function
%3assoc%1 which has the recursive definition

	%3assoc%2[%3v, a%2] ← %4if n %3a %4then %5NIL %4else if aa %3a
%4 eq %3v %4then a %3a %4else %3alt%2[%3v, %4d %3a%2]%1.

Thus we have %3assoc%2[%5X, ((X.(B.C)) (Y.A) (X.B))%2] = %5(X.(B.C))%1.

	A simplified version of the usual LISP %3eval%1 is the following:

%3eval%2[%3e, a%2] ←
	%4if at %3e %4then %2[%4if %3numberp %3e %2∨ %3e
 %4eq %5NIL %2∨ %3e %4eq %5T %4then %3e %4else%3 assoc%2[%3e, a%2]]
	%4else if at a%3 e %4then
		%2[%4if a %3e%4 eq %5CAR %4then a %3eval%2[%4ad %3e, a%2]
		%4else if a %3e%4 eq %5CDR %4then d %3eval%2[%4ad %3e, a%2]
		%4else if a %3e%4 eq %5CONS %4then %3eval%2[%4ad %3e, a%2]
 . %3eval%2[%4add %3e, a%2]
		%4else if a %3e%4 eq %5ATOM %4then at %3eval%2[%4ad %3e, a%2]
		%4else if a %3e%4 eq %5EQ %4then at %3eval%2[%4ad %3e, a%2]
 %4eq %3eval%2[%4add %3e, a%2]
		%4else if a %3e%4 eq %5QUOTE %4then ad %3e
		%4else if a %3e%4 eq %5COND %4then %3evcon%2[%4d %3e, a%2]
		%4else if a %3e%4 eq %5LIST %4then %3mapcar%2[%4d %3e, 
λ%3x%2: %3eval%2[%3x, a%2]]
		%4else %3eval%2[%4d %3assoc%2[%4a %3e, a%2] . %4d %3e, a%2]]
	%4else if aa %3e %4eq %5LAMBDA %4then
 %3eval%2[%4adda %3e, prup%2[%4ada %3e, mapcar%2[%4d %3e, %2λ%3x%2: %3eval%2[%3x, a%2]]] * %3a%2]
	%4else if aa %3e %4eq %5LABEL %4then
%3eval%2[%4adda %3e . %4d %3e, %2[%4ada %3e . %4a %3e%2] . %3a%2]%1, 

where the auxiliary function %3evcon%1 is defined by

	%3evcon%2[%3u, a%2] ← %4if %3eval%2[%4aa %3u, a%2] %4then %3eval%2[%4ada %3u, a%2]
 %4else %3evcon%2[%4d %3u, a%2]%1, 
and the auxiliary function %3prup%1 used for pairing up the elements of two
lists of equal length is defined by

	%3prup%2[%3u, v%2] ← %4if n %3u %4then %5NIL %4else %2[%4a %3u
 . %4a %3v%2] . %3prup%2[%4d %3u,%4d %3v%2].%1
	The way %3eval%1 works should be clear; atoms are either immediately
evaluable or have to be looked up on the list %3a%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; %3list%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 %3a%1 and substituted for their names; when a function is specified
by a λ, the inner expression is evaluated with a new %3a%1 which is obtained
by evaluating the arguments and pairing them up with the variables and putting
them on the front of the old %3a%1; and finally, %4label%1 is handled by
pairing the name of the function with the expression on %3a%1 and replacing
the whole function by the λ-part.

	%3eval%1 plays both a theoretical and a practical role in LISP.
Historically, the list notation for LISP functions and %3eval%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
%3eval%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 %3eval%1 has remained a feature of most LISP systems.

	The way %3eval%1 handles arguments corresponds to the call-by-value
method of parameter passing in ALGOL and similar languages.  There is also
a form of %3eval%1 that corresponds to call-by-name.  Here it is:

	%3neval%2[%3e, a%2] ← %4if at %3e%4 then
		%2[%4if %3e %4eq %5T %4 then %5T
		%4else if %3e %4eq %5NIL %4then %5NIL
		%4else if %3numberp e %4then %3e
		%4else %3neval%2[%4ad %3assoc%2[%3e, a%2], %4dd %3 assoc%2[%3e, a%2]]]

	%4else if at a %3e %4 then
		%2[%4if a %3e %4eq %5CAR %4then a %3neval%2[%4ad %3e, a%2]
		%4else if a %3e %4eq %5CDR %4then d %3neval%2[%4ad %3e, a%2]
		%4else if a %3e %4eq %5CONS %4then %3neval%2[%4ad %3e, a%2]
 . neval%2[%4add %3e, a%2]
		%4else if a %3e %4eq %5ATOM %4then at %3neval%2[%4ad %3e, a%2]
		%4else if a %3e %4eq %5EQ %4then %3neval%2[%4ad %3e, a%2]
 %4eq %3neval%2[%4add %3e, a%2]
		%4else if a %3e %4eq %5QUOTE %4then ad %3e
		%4else if a %3e %4eq %5COND %4then %3nevcon%2[%4d %3e, a%2]
		%4else if a %3e %4eq %5LIST %4then %3mapcar%2[%4d %3e
%2, λ%3x%2: %3neval%2[%3x, a%2]]
		%4else %3neval%2[%4d %3assoc%2[%4a %3e, a%2] . %4d %3e, a%2]]

	%4else if aa %3e %4eq %5LAMBDA %4then %3neval%2[%4adda %3e, 
nprup%2[%4ada %3e, %4d %3e%2,  %3a%2]]

	%4else if aa %3e %4eq %5LABEL %4then %3neval%2[%4adda %3e
 . %4d %3e, %2[%4ada %3e . %4a %3e%2] . %3a%2], %1

where the auxiliary function %3nevcon%1 is given by

	%3nevcon%2[%3u, a%2] ← %4if %3neval%2[%4aa %3u, %3a%2] %4then
 %3neval%2[%4ada %3u, %3a%2] %4else %3nevcon%2[%4d %3u, %3a%2].%1

and nprup is

	%3nprup%2[%3u, v,a%2] ← %4if n %3u %4then %3a %4else %2[%4a %3u
 . %2[%4a %3v . a%2]] . %3nprup%2[%4d %3u, %4d %3v,a%2].%1
	The difference between %3eval%1 and %3neval%1 is only in two terms.
%3eval%1 evaluates a variable by looking it up on the association list whereas
%3neval%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, %3eval%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 %3neval%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 %3neval%1
gives a result in some cases in which %3eval%1 loops.  An example is
obtained by evaluating %3F%2[2, 1]%1 where %3F%1 is defined by

	%3F%2[%3x, y%2] ← %4if%3 x%2=0 %4then %20 %4else %3F%2[%3x%2-1, %3F%2[%3y%2-2, %3x%2]].%1

	1. Write %3neval%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

	%3loop x %2← %3loop x%1

and attempt to compute %3loop%2[%3x%2]%1 for any %3x%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 %3f%1 is a LISP function and %3a%1 is an S-expression, 
and we would like to know whether the computation of %3f%2[%3a%2]%1 terminates.
Suppose %3f%1 is represented by the S-expression %3f*%1 in the usual
S-expression notation for LISP functions.  Then the S-expression %5(f* (QUOTE a))%1
represents %3f%2[%3a%2]%1.  Define the function %3term%1 by giving
%3term%2[%3e%2]%1 the value %4true%3 if %3e%1 is an S-expression of the
form %5(f* (QUOTE a))%1 for which %3f%2[%3a%2]%1 terminates and %4false%1 otherwise.
We now ask whether %3term%1 is a LISP function, i.e. can it be constructed
from %3car, cdr, cons, atom, %1 and %3eq%1 using λ, %4label%1, and
conditional expressions?  Well, it can't, as we shall shortly prove, 
and this means that it is not %3computable%1 whether a LISP calculation
terminates, since if %3term%1 were computable by any computer or in any
recognized sense, it could be represented as a LISP function.  Here is the

	Consider the function %3terma%1 defined from %3term%1 by

	%3terma u %2← %4if%3 term list%2[%3u, list%2[%5QUOTE%3, u%2]] %4then%3 loop u
 %4else true%1, 

and suppose that %3f%1 is a LISP function and that %3f*%1 is its
S-expression representation.  What is %3terma f*%1?
Well %3terma f*%1 tells us whether the computation of %3f%2[%3f*%2]%1
terminates, and it tells us this by going into a loop if %3f%2[%3f*%2]%1
terminates and giving %4true%1 otherwise.  Now if %3term%1 were
a LISP function, then %3terma%1 would also be a LISP function.  Indeed if
%3term%1 were represented by the S-expression %3term*%1, then
%3terma%1 would be represented by the S-expression

	%3terma* %5= (LAMBDA (U) (COND ((%3term*%5 (LIST U

Now consider %3terma%2[%3terma*%2]%1.  According to the definition of %3terma%1, 
this will tell us whether %3terma%2[%3terma*%2]%1 is defined, i.e. it tells
about itself.  However, it gives this answer in a contradictory way; namely
%3terma%2[%3terma*%2]%1 looping tells us that %3terma%2[%3terma*%2]%1 terminates, 
and %3terma%2[%3terma*%2]%1 being %4true%1 tells us that %3terma%2[%3terma*%2]%1
doesn't terminate.  This contradiction tells us that %3term%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 %3t%1 that sometimes says calculations terminate, 
sometimes says they don't terminate, and sometimes runs on indefinitely.
We shall further assume that when %3t%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 %3t%2[%3e%2]%1
with a computation of %3eval%2[%3e, %5NIL%2]%1 doing the computations
alternately.  If the %3eval%2[%3e, %5NIL%2]%1 computation ever terminates, 
then the new function asserts termination.

	Given such a %3t%1, we can always find a calculation that
does not terminate but %3t%1 doesn't say so.  The construction is just like that
used in the previous proof.  Given %3t%1, we construct

	%3ta u %2← %4if%3 t list%2[%3u, list%2[%5QUOTE%3, u%2]] %4then%3 loop u
 %4else true%1, 

and then we consider %3ta%2[%3ta*%2]%1.  If this had the value %4true%1, 
then it wouldn't terminate so therefore it doesn't terminate but is
not one of those expressions which %3t%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

	%3t%61%2[%3e%2] ← %4if%3 e %2= %3ta* %4then %5DOESN'T-TERMINATE
 %4else%3 t%2[%3e%2]%1.

Of course, %3t%61%1 isn't much better than %3t%1, since it can decide
only one more computation, but we can form %3t%62%1 by applying the same
process, and so forth.  In fact, we can even form %3t%6∞%1 which
decides all the cases decided by any %3t%6n%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.

.AT "#" ⊂NEXT ITEM;(ITEM!);⊃;

#. Write a function that gives %3t%6n+1%1 in terms of %3t%6n%1.

#. Write a function that gives %3t%6∞%1 in terms of %3t%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.

	In this chapter we will introduce techniques for proving
LISP programs correct.
The techniques will mainly be limited to what we may call %3clean%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
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.  Ideally, we would use a general theory of recursive
definition to prove theorems about LISP functions.  However,
the general theory is not well enough developed, so we have had
to introduce some methods limited to LISP functions defined by
particular kinds of recursion schemes.

.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
certain recursive definitions directly as formulas of the logic.
Unfortunately, we will not be able to treat all recursive definitions
in this system, but only those which we can be sure are defined for
all values of the arguments.  Moreover, we will be unable to prove
definedness within the system, so we will be restricted to classes
of recursive definitions which we can prove always defined by
an argument outside the system.  Fortunately, many interesting
LISP functions meet these restrictions including all the important
functions so far used except for %3eval%1 and its variants.

	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.

%4Constants%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

%4Variables%1: We will use the letters %3u%1 thru %3z%1 with or
without subscripts as variables.

%4Function symbols%1: The letters %3f%1, %3g%1 and %3h%1 with or
without subscripts are used as function symbols.
The LISP function symbols %4a%1, %4d%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.

%4Predicate symbols%1: The letters %3p%1, %3q%1 and %3r%1 with or
without subscripts are used as predicate symbols.  We will
also use the LISP predicate symbol %4at%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.

	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 %5T%1 or %5F%1.
Terms are used in making sentences, and sentences occur in
terms so that the definitions are %3mutually recursive%1 where
this use of the word %3recursive%1 should be distinguished from
its use in recursive definitions of functions.
Function expressions are also involved in the mutual recursion.

%4Terms%1: Constants are terms, and variables are terms.  If
%3f%1 is a function expression taking %3n%1 arguments, and %3t%61%3,#...#,t%6n%3%1
are terms, then %3f[t%61%3,#...#,t%6n%3]%1 is a term.  If %3p%1 is
a sentence and %3t%61%3%1 and %3t%62%1 are terms, then
%4if%3#p#%4then%3#t%61%3#%4else%3#t%62%1%1 is a term.  We soften the
notation by allowing infix symbols where this is customary.

If %3p%1 is a predicate expression taking %3n%1 arguments and
%3t%61%3,#...#,t%6n%3%1 are terms, then %3p[t%61%3,#...#,t%6n%3]%1 is
a sentence.  Equality is also used as an infixed predicate
symbol to form sentences, i.e. %3t%61%3#=#t%62%1%1 is a sentence.
If %3p%1 is a sentence, then %3¬p%1 is also a sentence.  If
%3p%1 and %3q%1 are sentences, then %3p∧q%1, %3p∨q%1, %3p⊃q%1,
and %3p≡q%1 are sentences.  If %3p%1, %3q%1 and %3r%1 are
sentences, then %4if%3#p#%4then%3#q#%4else%3#r%1 is a sentence.
If %3x%61%3,#...,#x%6n%3%1 are variables, and %3p%1 is a term, then
%3∀x%61%3#...#x%6n%3:t%1 and %3∀x%61%3#...#x%6n%3:t%1 are sentences.

%4Function expressions%1: A function symbol is a function expression.
If %3x%61%3,#...#,x%6n%3%1 are variables and %3t%1 is a term, then
%3[λx%61%3,#...#,x%6n%3:t]%1 is a function expression.

%4Predicate expressions%1: A predicate symbol is a predicate expression.
If %3x%61%3,#...#,x%6n%3%1 are variables and %3p%1 is a sentence, then
%3[λx%61%3,#...#,x%6n%3:p]%1 is a predicate expression.

	An occurrence of a variable %3x%1 is called bound if
it is in an expression of one of the forms %3[λx%61%3#...#x%6n%3:t]%1,
%3[λx%61%3#...#x%6n%3:p]%1, %3[∀x%61%3#...#x%6n%3:p]%1 or %3[∃x%61%3#...#x%6n%3:p]%1
where %3x%1 is one
of the numbered %3x%1's.  If not bound an occurrence is called free.

	The %3semantics%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

	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:

	%3∀x%61%3#...#x%6n%3:e%1 is assigned true if and only if %3e%1 is assigned
true for all assignments of elements of the domain to the %3x%1's.  If
%3e%1 has free variables that are not among the %3x%1's, then the
truth of the sentence depends on the values assigned to these remaining
free variables.  %3∃x%61%3#...#x%6n%3:e%1 is assigned true if and only if %3e%1
is assigned true for %3some%1 assignment of values in the domain to
the %3x%1's.  Free variables are handled just as before.

	%3λx%61%3#...#x%6n%3:u%1 is assigned a function or predicate according
to whether %3u%1 is a term or a sentence.  The value of
%3[λx%61%3#...#x%6n%3:u][t%61%3,...,t%6n%3] is obtained by evaluating the 
%3t%1's and using these values as values of the %3x%1's in the
evaluation of %3u%1.  If %3u%1 has free variables in addition to the %3x%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
%3first order lambdas%1.
.ss Conditional forms.

	All the properties we shall use of conditional forms follow
from the relation

	%3[p ⊃ [%4if%3 p %4then %3a %4else%3 b] = a] ∧ [¬p ⊃ [%4if%3 p %4then%3 a
%4else%3b] = 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

	%4if%5#T#%4then%3#a#%4else%3#b%3 = a%1


	%4if%5#F#%4then%3#a#%4else%3#b%3 = b%1.

	Next we have a %3distributive law%1 for functions applied
to conditional forms, namely

	%3f[%4if%3 p %4then%3 a %4else%3 b] = %4if%3 p %4then%3 f[a] %4else%3 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.


	%4if%3 [%4if%3 p %4then%3 q %4else%3 r] %4then%3 a %4else%3 b =
%4if%3 p %4then%3 [%4if%3 q %4then%3 a %4else%3 b] %4else%3 [%4if%3 r
%4then%3 a %4else%3 b]%1


	%4if%3 p %4then%3 [%4if%3 q %4then%3 a %4else%3 b] %4else%3 c =
%4if%3 q %4then%3 [%4if%3 p %4then%3 a %4else%3 c] %4else%3 [%4if%3 p
%4then%3 b %4else%3 c]%1.

	When the expressions following %4then%1 and %4else%1 are
sentences, then the conditional form can be replaced by a sentence
according to

	%3[%4if%3 p %4then%3 q %4else%3 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 %3p%1 occurs twice in the right
hand side of the above equivalence.  In the most unfavorable case,
%3p%1 is dominates the size of the expression so that writing it
twice almost doubles the size of the expression.

	Suppose that %3a%1 and %3b%1 in
are expressions that may contain the sentence %3p%1.  Occurrences
of %3p%1 in %3a%1 can be replaced by %5T%1, and occurrences of %3p%1
in %3b%1 can be replaced by %5F%1.  This follows from the fact that
%3a%1 is only evaluated if %3p%1 is true and %3b%1 is evaluated only
if %3p%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 %3e#=#e'%1, then we can replace any occurrence of %3e%1
in an expression by an occurrence of %3e'%1.  However, if we want
to replace %3e%1 by %3e'%1 within %3a%1 within
then we need only prove %3p#⊃#e#=e'%1, and to make the replacement
within %3b%1 we need only prove %3¬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 %3lambda-conversion%1, essentially

	%3[λx:e][a] =%1 <the result of substituting %3e%1 for %3x%1 in %3a%1>.

As examples of this rule, we have

	%3[λx:%4a%3 x . y][u . v] = [%4a%3[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 %3x#+#y%1 for %3x%1 in %3∀y:[x#+#y#=#z]%1 or into
the term %3[λy:x#+#y][u#+#v]%1.  Before doing the substitution, the
variable %3y%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 %3e%1.  It is easy to make an expression of length %3n%1 whose
length is increased to 2%7n%1 by converting its %3n%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:

	%3∀x.(issexp x ⊃ %4at%3 x ∨ (issexp %4a%3 x ∧ issexp %4d%3 x
∧ x = (%4a%3 x . %4d%3 x)))%1


	%3∀x y.(issexp x ∧ issexp y ⊃ issexp(x.y) ∧ ¬%4at%3(x.y)
∧ x = %4a%3(x.y) ∧ y = %4d%3(x.y))%1.

Here %3issexp e%1 asserts that the object %3e%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

	%3∀x.[%4at%3 x ∨ x = [%4a%3 x . %4d%3 x]]%1


	%3∀x y.[¬%4at%3[x.y] ∧ x = %4a%3[x.y] ∧ y = %4d%3[x.y]]%1.

	The algebraic facts about lists are expressed by the following
sentences of first order logic:

	%3∀x. islist x ⊃ x = %5NIL%3 ∨ islist %4d %3x%1,

	%3∀x y. islist y ⊃ islist[x . y]%1,

	%3∀x y. islist y ⊃ %4a%3[x . y] = x ∧ %4d%3[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 %3n'%1 for the successor of %3n%1
and %3n%7-%1 for the predecessor of %3n%1.  Peano's algebraic axioms
then become

	%3∀n: n' ≠ 0%1,

	%3∀n: (n')%7-%3 = n%1,


	%3∀n: n ≠ 0 ⊃ (n%7-%3)' = n%1.

Integers specialize  lists if we identify 0 with %5NIL%1 and assume that
there is only one object (say 1) that can serve as a list element.
Then %3n'#=#cons[1,n]%1, and %3n%7-%3#=#%4d%3 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
%2a%1 satisfying

	%4a%3 a = %4d%3 a = a . a = a%1.

It satisfies the algebraic axioms for S-expressions.  We can exclude
it by an axiom %3∀x.(%4a%3 x ≠ x)%1, but this won't exclude other
circular list structures that eventually return to the same element
by some %4a-d%1 chain.  Actually we want to exclude all infinite
chains, because most LISP programs won't terminate unless every
%4a-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 axioms
of induction analogous to Peano's induction axiom.  Peano's axiom
is ordinarily written

	%3P(0) ∧ ∀n:(P(n) ⊃ P(n')) ⊃ ∀n:P(n)%1.

Here %3P(n)%1 is an arbitrary predicate of integers, and we get particular
instances of the axiom by substituting particular predicates.

Peano's induction schema can also be written 

	%3∀n:(n = 0 ∨ P(n%7-%3) ⊃ P(n)) ⊃ ∀n:P(n)%1,

and the equivalence of the two forms is easily proved.

	The S-expression analog is

	%3∀x:[issexp x ⊃ [%4at%3 x ∨ P[%4a%3 x] ∧ P[%4d%3 x] ⊃ P[x]]] ⊃
∀x:[issexp x ⊃ P[x]]%1,

or, assuming everything is an S-expression

	%3∀x:[%4at%3 x ∨ P[%4a%3 x] ∧ P[%4d%3 x] ⊃ P[x]] ⊃ ∀x:P[x]%1.

	The corresponding axiom schema for lists is

	%3∀u:[islist u ⊃ [%4n%3 u ∨ P[%4d%3 u] ⊃ P[u]]] ⊃ ∀u:[islist u
⊃ P[u]]%1.

	These schemas are called principles of %3structural 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:	%3u * v ← %4if n%3 u %4then%3 v %4else a%3 u . [%4d%3 u * v]%1.

Because %3u*v%1 is defined for all %3u%1 and %3v%1, i.e. the computation
described above terminates for all %3u%1 and %3v%1, we can replace ({[5] si2})
by the sentence

!!si1:	%3∀u v:[islist u ∧ islist v ⊃
[%3u * v = %4if n%3 u %4then%3 v %4else a%3 u . [%4d%3 u * v]]]%1.

Now suppose we would like to prove %3∀v:[%5NIL%3 * v = v]%1.  This is
quite trivial; we need only substitute %5NIL%1 for %3x%1 in ({[5] si1}),

→%5NIL%3 * v ∂(15)#= %4if n %5NIL %4then%3 v %4else a %5NIL%3 . [%4d %5NIL%3 * v]

∂(15)#= v%1.

Next consider proving %3∀u:[u * %5NIL%3 = u]%1.  This cannot be done by
simple substitution, but it can be done as follows:  First substitute
%3λu:[u * %5NIL%3 = u]%1 for %3P%1 in the induction schema

	%3∀u:[islist u ⊃ [%4n%3 u ∨ P[%4d%3 u] ⊃ P[u]]] ⊃ ∀u:[islist u
⊃ P[u]]%1,


	%3∀u:[islist u ⊃ [%4n%3 u ∨ %3λu:[u * %5NIL%3 = u][%4d%3 u]
⊃ %3λu:[u * %5NIL%3 = u][u]]] ⊃ ∀u:[islist u
⊃ %3λu:[u * %5NIL%3 = u][u]]%1.

Carrying out the indicated lambda conversions makes this

!!si3:	%3∀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 %3u*v%1.  There
are two cases according to whether qn %3u%1 or not.
In the first case, we substitute qnil for %3v%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:	%3qa 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.