\documentclass[landscape,12pt]{slides}\usepackage[]{color}\begin{document}\begin{slide}        \begin{center}                        \textcolor{red}{SOME LISP HISTORY AND SOME                        PROGRAMMING LANGUAGE IDEAS} \\                        John McCarthy, Stanford University \\                        Berlin, 2002 June 19                        \vspace{0.3in}                \end{center}                 $\bullet$ I suppose I'm here because of Lisp, although I haven't  been involved in the Lisp community for a very long time.  $\bullet$ Lisp is actively used, e.g. on the Deep Space 1 spacecraft and in the Orbitz airline reservation system, but I don't know any details.  $\bullet$ Fritz Kunze's Franz Inc. makes quite a good common Lisp, called Allegro Common Lisp.   $\bullet$ Some important aspects of Lisp are not available in other  programming languages and systems.  I don't know if they are used in  the above applications.   $\bullet$ The original idea was to combine 1956 list processing as done by Newell, Simon and Shaw with ideas from John Backus's Fortran.   $\bullet$ Herbert Gelernter at IBM undertook to implement Marvin Minsky's  idea for a plane geometry theorem prover, and I proposed list  processing in Fortran.  Gelernter and Carl Gerberich developed FLPL.  $\bullet$ In 1958 Lisp was started at M.I.T. using recursion, which  was not feasible in Fortran.  Lisp was intended for AI programming.  $\bullet$ Lisp was intended to be compiled at first.  However, I wrote a universal Lisp function $eval$ in 1959 to show that Lisp was a neater language for computability theory than Turing machines.  Steve Russell pointed out that the universal function could be taken as an interpreter for pure Lisp, and hand-compiled it in IBM 704 machine language.  \vfill \end{slide} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\begin{slide}        \begin{center}                \textcolor{red}{DIFFERENTIATION---the motivating example} \\                \vspace{0.3in}                \end{center} The following example motivated  $\bullet$  recursion using conditional expressions  $\bullet$  lisp notation for algebraic expressions  $\bullet$ allowing functions as arguments with $\lambda$-expression  syntax  $\mbox{diff}(e,v) \leftarrow \mbox{if}\ \mbox{at}\ e\ \mbox{then}\  \\\ [\mbox{if}\ e = v\ \mbox{then}\ 1\ \mbox{else}\ 0\ ] \\\mbox{else if}\ \mbox{car}\ e\ = PLUS\ \mbox{then}\ PLUS\ .\ maplist(cdr\ e, \lambda u. diff(car\ u,v)) \\\mbox{else if}\ \mbox{car}\ e\ = TIMES\ \mbox{then}\ PLUS\ .\ maplist(cdr \ e,\lambda u. TIMES\ .\\ maplist(cdr\ e, \lambda w. \ \ \mbox{if}\ u\ \ \mbox{eq}\ w\ \mbox{then}\ diff(car\ u,v) \ \ \mbox{else}\ car\ w)))$ \vfill \end{slide} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  \begin{slide}        \begin{center}                        \textcolor{red}{ASPECTS OF LISP} \\                        \vspace{0.3in}                \end{center} $\bullet$ Lisp lists including lists of list are the appropriate  representation of symbolic expressions for computation---better than  strings---and better than XML.  $\bullet$ Lisp programs are Lisp data.  Put abstractly, Lisp has  functions for its own \emph{abstract syntax.}  $\bullet$ Lisp programs, most conveniently pure Lisp functional programs, are are described extensionally by first order sentences.  $\bullet$ Many important properties of the functions can be proved by first order reasoning.  $\bullet$ Other important properties require \emph{derived functions.}   \vfill \end{slide} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{slide}        \begin{center}                        \textcolor{red}{EXAMPLES OF LISP FUNCTIONAL PROGRAMS} \\                        \vspace{0.3in}                \end{center} $\bullet$ \\ (defun append (u v) \\   $\quad\quad\quad \quad\quad\quad\quad $      (if\\   \quad\quad\quad\quad (null u)\\   \quad\quad\quad\quad v \\\quad\quad\quad\quad    (cons (car u) (append (cdr u) v))))           $\bullet$ $u\ *\ v \leftarrow \mathbf{if}\ \mathbf{n}\ u\  \mathbf{then}\ v\ \mathbf{else}\ \mathbf{a}\ u\ .\ [\mathbf{d}\ u\ *  v]$ is a pure LISP functional program.   $\bullet$ $(\forall u\ v)(u\ *'\ v = \mathbf{if}\ \mathbf{n}\ u\  \mathbf{then}\ v\ \mathbf{else}\ \mathbf{a}\ u\ .\ [\mathbf{d}\ u\ *'  v])$ is an equation for the function computed by the program.  The  close correspondence is very convenient but sometimes confusing.  $\bullet$ The pure Lisp functional program as an equation permits  convenient proofs in a first order theory that Lisp programs meet  their specifications.  For example, it is easy to prove by list induction that  $\forall u\ v.(u * v) * w = u * (v * w))$, i.e. that appending lists is an  associative operation. \vfill \end{slide} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\begin{slide}        \begin{center}                        \textcolor{red}{LISP AND OTHER LANGUAGES} \\                        \vspace{0.3in}                \end{center} $\bullet$ Garbage collection, conditional expressions and recursive  programs have been taken into other languages.  $\bullet$ LISP data structures have been imitated clumsily in XML.  (BUY item1 Item2 Item3)  $<$BUY$>$ item1 item2 item3 $<$/BUY$>$ $\bullet$ LISP programs having access to the abstract syntax of the program has not been imitated.  This represents a lack of imagination, but I admit I don't have convincing examples of its use. \vfill \end{slide} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%    \begin{slide}        \begin{center}                        \textcolor{red}{DERIVED FUNCTIONS} \\                        \vspace{0.3in}                \end{center}The computational cost of a Lisp functional recursive program is not determined by the extension of the function.  We have\\%$f91(x) \leftarrow\ \mbox{if}\ x > 100 \ \mbox{then}\ x - 10\ \ \mbox{else}\ f91(f91(x + 11))$\\%and%$ff91(x) \leftarrow\ \mbox{if}\ x > 100 \ \mbox{then}\ x - 10\\ \mbox{else}\ 91$.We have $\forall x.f91'(x) = ff91'(x))$, but clearly the functional programs are different computationally.  Suppose we are interestedin how many times the + operation is executed in evaluating $f91(x)$.This is given by $f91p'(x)$, where$f91p(x) \leftarrow\ \mbox{if}\ x > 100 \ \mbox{then}\ 0 \ \mbox{else}\ 1 + f91p(f91(x + 11)) + f91p(x + 11)$. \vfill \end{slide} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  \begin{slide}        \begin{center}                        \textcolor{red}{ELEPHANT 2000: a programming                         language for the year 2010} \\                        www.formal.stanford.edu/jmc/elephant.html                        \vspace{0.3in}                \end{center}                 $\bullet$ \textcolor{blue}{An elephant never forgets.} An Elephant program can say, ``A passenger has a reservation in a situation $s$ if he has made a reservation and not cancelled it. The Elephant program need not specify a data structure to remember  reservations.  The compiler must provide the necessary data  structures so that whether a passenger has a reservation can be  determined. \begin{equation}\begin{array}[l]{l}          Has(passenger,reservation,s) \equiv \\     (\exists s' < s) Occurs(Makes(passenger, reservation),s) \\     \land \lnot (\exists s'') (s < s'' < s' \land      Occurs(Cancel(Passenger,reservation),s'')     \end{array}     \label{eq:} \end{equation}�  $\bullet$ \textcolor{blue}{An elephant is faithful one hundred percent.} A reservation is a promise to let the passenger on the airplane if he has one when he shows up.  One kind of Elephant output statement is a promise, and correct Elephant programs fulfill their promises.  $\bullet$ The Elephant language includes program statements called  commitments generalizing Floyd assertions, because they can refer to  the future,  A correct Elephant program fulfills its commitments.  \begin{equation}        \label{eq:}        \begin{array}{l}         (\forall s > Now) (Value(X,s) > Value(X,Now))          \end{array}         \end{equation}$\bullet$ Elephant i-o input output statments are speech acts, e.g. questions, requests, acceptances of proposals, answers to questions.  Answers to questions should be true and responsive.   \vfill \end{slide} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  \begin{slide}        \begin{center}                        \textcolor{red}{ALGOL 48} \\                        \vspace{0.3in}                \end{center} If we introduce time explicitly as distinct from the program counter, Algolic programs can be written as sets of equations.  Here's anAlgol 60 program for computing the product $mn$ of two natural numbers.%\begin{eqnarray}start:&& \nonumber \\i & := & n; \nonumber \\p & := & 0; \nonumber \\loop: && if\ i = 0\ then\ go\ to\ done; \nonumber \\i & := & i - 1; \nonumber  \\go to&& loop; \nonumber \\done: && \nonumber \end{eqnarray}\newpageHere's what mathematicians might have written in 1948, before programming languages existed.%\begin{eqnarray}pc(0) &=& 0; \nonumber \\i(t + 1) &=& \mbox{if}\ pc(t) = 0\ \mbox{then} \ n \nonumber \\ \nonumber  \mbox{else if}\ pc(t) = 4\\mbox{ then}\ i(t) - 1\ \mbox{else}\ i(t); \nonumber \\p(t + 1) &=& \mbox{if}\ pc(t) = 1\ \mbox{then}\ 0 \nonumber \\\mbox{else if}\ pc(t) = 5\ \mbox{then}\ p(t) + m\ \mbox{else}\ p(t) \nonumber  \\pc(t+1) &=& \mbox{if}\ pc(t) = 2 \land i(t) = 0\ \mbox{then}\ 6 \nonumber \\\mbox{else if}\ pc(t) = 5\ \mbox{then}\ 2\ \mbox{else}\  pc(t) + 1; \nonumber \\\end{eqnarray} \vfill \end{slide}  The proof that $\exists t.  (t \geq 0 \land pc(t) = 6 \land p(t) = mn)$ follows from the sentences expressing the program and the laws of arithmetic, i.e. no theory of program correctness is needed.  However, the proof ideas are essentially the same as those used to prove that an algolic program terminates and that the outputs have the correct relation to the inputs.  Amir Pnueli and Nissim Francez had this idea before I did, but they mistakenly abandoned it for temporal logic. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  \end{document}Boyer-Moore, Scott and Milnerwhat's missing?Cartwright and me.Ask CarolynIan Mason and dirty Lisp - locally dirty, globally clean.