\newcommand\inductionrule{\index{induction rule}\mbox{induction} rule} \newcommand\inductionrules{\inductionrule s} \renewcommand\lessymbol{\ident{lessp}} \renewcommand\sizesymbol{\ident{count}} \newcommand\HopeParkSquare{\index{Hope Park}Hope Park Square} \newcommand\englishEBPURELISPMACHINE{ICL--4130} \newcommand\eineenglishEBPURELISPMACHINE{an \englishEBPURELISPMACHINE} \newcommand\englishdiesespapier{this article} \newcommand\englishDiesespapier{This article} \newcommand\englishDiesesPapier{This Article} \newcommand\englishdiesesPapier{this Article} \newcommand\figurewaterfall[1]{\begin{figure}[#1]% %\yestop \index{destructor elimination}% \index{simplification}% \index{generalization}% \index{destructor elimination}% \index{cross-fertilization}% \index{elimination of irrelevance}% \noindent\LINEnomath{\includegraphics [scale=.36,bb=0 0 1078 708]{waterfall.eps.gz}% }\caption {The \boyermooreWaterfall\label{figure waterfall}} \LINEnomath{\footnotesize Note that a formula falls back to the center pool after each successful application \hfill\mbox{}% \\[-1ex]% \mbox{}\hfill of one of the stages in the circle.} \yestop%\yestop \end{figure}} \newcommand\figuremerging[1]{\begin{figure}[#1]%\notop \LINEmaths{\begin{array}{l|l l l@{\hspace*{-1.7em}}r} &\mbox{pos.\ set~~} &\mbox{ind.\ var.s} &\mbox{step-case description} &%2 * \mbox{hitting\,ratio} \\\hline\headroom 1 &\{1\} &\{x\} &\displayset{\!\!\!\displaytrip {\!\!\domres\id{\{x,z\}}} {\{\mu_1\}} {\{x\tightnotequal\zeropp\}\!\!}\!\!\!} &1 \\2 &\{2\} &\{x\} &\displayset{\!\!\!\displaytrip{\!\!\domres\id{\{x,y\}}}{\{\mu_2\}} {\{x\tightnotequal\zeropp\}\!\!}\!\!\!} &1%2 \\3 &\{2\} &\{y\} &\displayset{\!\!\!\displaytrip{\!\!\domres\id{\{x,y\}}}{\{\mu_2\}} {\{y\tightnotequal\zeropp\}\!\!}\!\!\!} &1%2 \\4 &\{3\} &\{y\} &\displayset{\!\!\!\displaytrip{\!\!\domres\id{\{y,z\}}}{\{\mu_3\}} {\{y\tightnotequal\zeropp\}\!\!}\!\!\!} &1%2 \\5 &\{3\} &\{z\} &\displayset{\!\!\!\displaytrip{\!\!\domres\id{\{y,z\}}}{\{\mu_3\}} {\{z\tightnotequal\zeropp\}\!\!}\!\!\!} &1%2 \\6 &\{2\} &\{x,y\} &\displayset{\!\!\!\displaytrip{\!\!\domres\id{\{x,y\}}}{\{\mu_2\}} {\{x\tightnotequal\zeropp\comma y\tightnotequal\zeropp\}\!\!}\!\!\!} &2 \\7 &\{3\} &\{y,z\} &\displayset{\!\!\!\displaytrip{\!\!\domres\id{\{y,z\}}}{\{\mu_3\}} {\{y\tightnotequal\zeropp\comma z\tightnotequal\zeropp\}\!\!}\!\!\!} &2%4 \\8 &\{2,3\} &\{x,y,z\} &\displayset{\!\!\!\displaytrip{\!\!\domres\id{\{x,y,z\}}}{\{\mu_4\}} {\{x\tightnotequal\zeropp\comma y\tightnotequal\zeropp\comma z\tightnotequal\zeropp\}\!\!}\!\!\!} &4%8 \\9 &\{1,2,3\} &\{x,y,z\} &\displayset{\!\!\!\displaytrip{\!\!\domres\id{\{x,y,z\}}}{\{\mu_4\}} {\{x\tightnotequal\zeropp\comma y\tightnotequal\zeropp\comma z\tightnotequal\zeropp\}\!\!}\!\!\!} &5%9 \\\end{array}}{} \\\headroom\LINEnomath {\math{\mu_1=\{x\tight\mapsto\ppp x\comma z\tight\mapsto\ppp z\}}, \hskip 2em \math{\mu_2=\{x\tight\mapsto\ppp x\comma y\tight\mapsto\ppp y\}}, \nlnomath \math{\mu_3=\{y\tight\mapsto\ppp y\comma z\tight\mapsto\ppp z\}}, \hskip 2em and \hskip 2em \maths{\mu_4=\{x\tight\mapsto\ppp x\comma y\tight\mapsto\ppp y \comma z\tight\mapsto\ppp z\}}.} \\\LINEnomath{pos.\ % set = position%set ; \ \ \ \ ind.\ var.s = set of induction variables; \ \ \ \ hit.\ = hitting% % \nlnomath % \math{2 * \mbox{hit.\ ratio}} = hitting ratio multiplied by \nlbmaths 2 .}% \notop\halftop\caption{\protect\footroom The induction schemes of \examref{example merging 2}\label {figure induction schemes}}\notop\notop\end{figure}} \newcommand\footnoteonMetamathematicsUnitandMembersofUnivEB {\majorheadroom In the early 1970s, the \uniEB\ hosted most remarkable scientists, of which the following are relevant in our context (sources: \cite{meltzer-1975}, \cite{kowalski-1988}, \etc): \\\mbox{}\\\noindent\LINEnomath{\begin{tabular}{l|l l l} &\uniEBshort\ &\PhD &life time \\ &(time, \Dept) &(year, advisor) &(birth--death) \\\hline \michiename &(1965--1984, MI) &(1953, unknown) &\michielifetime \\ \meltzername &(1965--1978%Dec 31 %some say 1977 , CL) &(1953, {\namefont %Reinhold F\ue rth}) &\meltzerlifetime \\\popplestonename &(1965--1984, MI) &(no \PhD) &\popplestonelifetime \\\burstallname\ &(1965--2000, MI \& \Dept\,AI) &(1966, {\namefont Dudley}) &\burstalllifetime\ \\\kowalskiname &(1967%Oct --1974%Dec , CL) &(1970, \meltzer) &\kowalskilifetime \\\hayesname &(1967--1973, CL) &(1973, \meltzer) &\hayeslifetime \\\plotkinname\ &(1968--today, CL \& LFCS) &(1972, \burstall) &\plotkinlifetime\ \\\moorename &(1970--1973, CL) &(1973, \burstall) &\moorelifetime \\\gordonname\ &(1970--1978, MI) &(1973, \burstall) &\gordonlifetime \\\boyername &(1971--% % 1974% 1973% % Hi CP. Bob read the article -- at least he spent as % much time on it as he felt he could -- and only made % one suggestion: he believes that he and his family left % Edinburgh for California in 1973 (probably November or % December). (I know I left in December, 1973: I % celebrated New Years 1974 in Palo Alto.) , CL) &(1971, \bledsoe) &\boyerlifetime \\\bundyname &(1971--today, CL) &(1971, {\goodsteinindex\goodstein}) &\bundylifetime \\\milnername &(1973--1979, LFCS) &(no \PhD) &\milnerlifetime\ \\\end{tabular}}% \\[+3ex]\noindent \getittotheright{\begin{tabular}{@{}l@{~~}l@{~~}l@{}} CL &= &Metamathematics Unit (founded and headed by \meltzername) \\ &&(new name from late 1971 to \Oct\,1974: \Dept\ of Computational Logic) \\ &&(new name from \Oct\,1974: \Dept\ of \AI) \\MI &= &Experimental Programming Unit (founded and headed by \michiename) \\ &&(new name from 1966 to \Oct\,1974: \Dept\ for Machine Intelligence and Perception) \\ &&(new name from \Oct\,1974: Machine Intelligence Unit) \\LFCS &= &Laboratory for Foundations of Computer Science\footroom \\\end{tabular}}} \newcommand\footnotetextworkwithacomputerinearlyseventies {\footnotetext{% \majorheadroom Today's readers might have difficulty imagining the computing infrastructure in Scotland in the early 1970s. \par\boyer\ and \moore\ developed their software on \eineenglishEBPURELISPMACHINE, \hskip.1em with \nlbmath{64\kByte} (\nlbmath{128\kByte} in 1972) core memory (RAM)\@. \hskip.2em Paper tape was used for archival storage. \hskip.1em The machine was physically located in the \ForrestHillEB\ building of the University of \EB, \hskip.1em about 1\km\ from \HopeParkSquare. \hskip.15em A rudimentary time-sharing system allowed several users at once to run lightweight applications from teletype machines at \HopeParkSquare. \par During the day \boyer\ and \moore\ worked at \HopeParkSquare, with frequent trips by foot \nopagebreak or bicycle through \mbox{The Meadows} to \ForrestHillEB\ to make archival paper tapes \nopagebreak or to pick up line-printer output. \hskip.3em \nopagebreak\pagebreak During the night \nopagebreak ---~when they could often have \nopagebreak the \englishEBPURELISPMACHINE\ to themselves~--- \nopagebreak they often worked at \boyer's home where another \nopagebreak teletype was available.\par The only high-level programming language supported was {\sc POP--2}, \hskip.2em a simple stack-based list-processing language with an {\sc Algol}-like syntax, \cfnlb\ \cite{pop2}.\par Programs were prepared with a primitive text editor modeled on a paper-tape editor: A \nolinebreak disk file could be copied through a one byte buffer to an output file. \hskip.2em By halting the copying and typing characters into or deleting characters from the buffer one could edit a file ---~a process that usually took several passes. \hskip.3em Memory limitations of the \mbox\englishEBPURELISPMACHINE\ prohibited storing large files in memory for \nolinebreak editing. \par In \nolinebreak their very early collaboration, \hskip.1em \boyer\ and \moore\ solved this problem by inventing what has come to be called the ``piece table\closequotecommasmallextraspace whereby an edited document is represented by a linked list of ``pieces'' referring to the original file which remains on disk. \hskip.3em Their ``77-editor'' \cite{boyer-moore-davies-1973} \hskip.05em (written in 1971 and named for the disk track on which it resided) \hskip.1em provided an interface like \MIT's Teco, \hskip.1em but with {\sc POP--2} as the command language. It was thus with their own editor that \boyer\ and \moore\ wrote the code for the {\PURELISPTP}. \par The 77-editor was widely used by researchers at \HopeParkSquare\ until the \mbox\englishEBPURELISPMACHINE\ was decommissioned. When \moore\ went to Xerox PARC %CP (logicians and historians will not know where Xerox PARC is, % and then do not get the "Alto" reference below): in Palo Alto (CA) (\Dec\,1973), \hskip.2em the \boyermoore\ representation \cite{moore-1981} was adopted by \simonyiname\ \simonyilifetime\ for the Bravo editor on the Alto and subsequently found its way into Microsoft Word, \cfnlb\ \cite{simonyi-interview}.\majorfootroom% }} \newcommand\bigexampleformulaone {\exists\tight<\stopq\inparenthesesoplist{\! \forall\pair x y\stopq\inparentheses{\!\!\inpit{\plusppnoparentheses x y \tightequal\plusppnoparentheses y x} \nottight\antiimplies \forall\pair{x''}{y''}\,\tight<\,\pair x y\stopq\inpit {\plusppnoparentheses{x''}{y''} \tightequal\plusppnoparentheses{y''}{x''}}\!\!}\!\!\! \oplistund \!\Wellfpp<}}% \renewcommand\mindexsymbol[1]{w_{#1}} \renewcommand\Avignon{\mbox{A\hskip-.09em vignon}} \mathcommand\termsofdepthnovars[1]{{\mathcal T}_{#1}} \newcommand{\responsible}[1]{\protect\marginpar{\textbf{Res.:} #1}} \newenvironment{draft}{\begin{quote}\hrulefill\par\sl\textbf{Draft:}}{\hrulefill\par\end{quote}} \newcommand\frenchfont{}%{\sf} \newcommand\germanfont{}%{\fraknomath} \newcommand\germanfontfootnote{}%{\scriptscriptfrak} \renewcommand\namefont{} \newcommand\ednote[1]{{\red\Frak #1\marginpar{\huge\math\forall}}} \renewcommand\etc{etc.} \renewcommand\etalabbrev{{\it et al.}} \renewcommand\secondincompletenesstheorem{second \incompletenesstheorem} \renewcommand\secondIncompletenessTheorem{Second \IncompletenessTheorem} \renewcommand\udiff{if} \def\citep{\cite} \def\citet#1{\citeauthor{#1} \shortcite{#1}} \newenvironment{ack}{\section*{Acknowledgments}}{} \newcommand\qed {\relax\ifmmode\hskip2em \Box\else\unskip\nobreak\hskip1em $\Box$\fi} \newcommand\secondreaders[1] {\insert\footins{% \def\@thefnmark{$\ast$} \reset@font\footnotesize \interlinepenalty\interfootnotelinepenalty \splittopskip\footnotesep \splitmaxdepth \dp\strutbox \floatingpenalty \@MM \hsize\columnwidth \@parboxrestore \protected@edef\@currentlabel{% \csname p@footnote\endcsname \@thefnmark }% \color@begingroup \@makefntext{% \rule\z@\footnotesep\ignorespaces{Second Readers: #1} \@finalstrut\strutbox}% \color@endgroup}}