\documentclass[landscape,12pt]{slides}
\usepackage[]{color}
\begin{document}
\begin{slide}
\begin{center}
\textcolor{red}{BEYOND LISP} \\
John McCarthy, Stanford University \\
Stanford June 22, 2005 \\
http://www-formal.stanford.edu/jmc/ \\
jmc@cs.stanford.edu\\
\textcolor{red}{MAIN POINTS}
\end{center}
$\bullet$ Lisp programs are Lisp data---abstract syntax. \\
\quad\quad Programming languages need functions for their abstract syntax.\\
$\bullet$ English is important for its semantics---not its syntax\\
$\bullet$ The largest piece of cake---Kleene $\mu$ operator\\
$\bullet$ An elephant never forgets and is faithful.\\
$\bullet$ Resolution considered harmful.\\
$\bullet$ Special provers are just strategies---Davis-Putnam\\
$\bullet$ Programs as logical formulas---Algol 48 and Algol 50
\vfill\end{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}
\begin{center}
\textcolor{red}{PROGRAMS AS DATA---ABSTRACT SYNTAX} \\
\vspace{0.3in}
\end{center}
$\bullet$ Sums may be represented as (+ x y), x + y, $3^x7^y$ as text.
$\bullet$ $issum(exp)$, $s1(exp)$, $s2(exp)$, $mksum(exp1,exp2)$
$\bullet$ Programming languages (even Java and Curl) need their
abstract syntaxes defined and function in the language for the
abstract syntax.
$\bullet$ Lisp is close to its abstract syntax, but needs it anyway.
$\bullet$ Input syntax, print syntax, compute with it syntax. $x + 3$,
$ \textcolor{red}{x} \textcolor{blue}{+} 3$, (+ x 3). \emph{I should have given the
list structure.}
$\bullet$ $issubroutine(exp)$, $body(exp)$, $isjavaprogram(exp)$
$\bullet$ http://www-formal.stanford.edu/jmc/towards.html (1962)
\vfill\end{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}
\begin{center}
\textcolor{red}{ENGLISH AS A PROGRAMMING
LANGUAGE---IT'S THE SEMANTICS THAT'S IMPORTANT} \\
\vspace{0.3in}
\end{center}
$\bullet$ COBOL: add 3 to x, FORTRAN: x = x + 3, Algol 60: x := x + 3;
trivial variants
$\bullet$ ``the largest piece of cake'', Kleene $\mu$ operator
$\bullet$ ``I need to be at a meeting in Monterrey, Mexico from
November 15 to 17'' followed by dialog about details.
$\bullet$ ``The U.S. wants Iraq to become a non-aggressive,
prosperous, democracy''---Plan government policy. [to be done without
a precise definition of democracy].
\vfill\end{slide}
\begin{slide}
\begin{center}
\textcolor{red}{INCLUDE LOGICAL SENTENCES IN LISP} \\
\vspace{0.3in}
\end{center}
$\bullet$ (assert `(on block1 ,x)), (assert '((forall boy)((exists
girl)((loves girl (only boy))))))
$\bullet$ Also include a theorem prover-problem solver
$\bullet$ Resolution considered harmful.
$\bullet$ Special provers are just tactics in general provers to be
used on subproblems, e.g. Davis-Putnam used when only the outer
propositional structure is considered. [\textcolor{red}{confession:} I
can't do this yet.
\vfill\end{slide}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}
\begin{center}
\textcolor{red}{ELEPHANT} \\
\vspace{0.3in}
\end{center}
$\bullet$ Elephants never forget. An elephant is faithful, 100
percent.
$\bullet$ A passenger has a reservation if he has made one and it
hasn't been cancelled. Passengers with reservations should be on
the passenger list at flight time.
$\bullet$ A necessary condition for program correctness is that a
program fulfill its promises.
$\bullet$ Alas, Elephant 2000 is not ready to be implemented.
$\bullet$ http://www-formal.stanford.edu/jmc/elephant.html
\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 an
Algol 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}
\newpage
Here'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.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}
\begin{center}
\textcolor{red}{PROVING LISP PROGRAMS CORRECT} \\
\vspace{0.3in}
\end{center}
\vfill\end{slide}
\end{document}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{slide}
\begin{center}
\textcolor{red}{} \\
\vspace{0.3in}
\end{center}
\vfill\end{slide}
1. programs are data---abstract syntax
a pl should have access to its a.s.
there are three formats for programs
2. English is important for its semantics, not for its syntax
cobol example
3. the largest piece of cake, Kleene mu operator
4. elephant
5. algol50 and algol 48
adding FOL sentences to Lisp
resolution considered harmful
special provers are just strategies for FOL provers
Davis Putnam