\documentclass[a4]{seminar}
\usepackage{advi}
\usepackage{color}

\slideframe{none}
\definecolor{slideblue}{rgb}{0,0,.5}
\definecolor{slidegreen}{rgb}{0,.5,0}
\definecolor{slidered}{rgb}{1,0,0}
\newpagestyle{fw}{}{\hfil\textcolor{slideblue}{\sf\thepage}\qquad\qquad}
\slidepagestyle{fw}
\newcommand{\sectiontitle}[1]{\centerline{\textcolor{slideblue}{\textbf{#1}}}
\par\medskip}
\newcommand{\slidetitle}[1]{{\textcolor{slideblue}{#1}}\par
\vspace{-1.2em}{\color{slideblue}\rule{\linewidth}{0.04em}}}
\newcommand{\dashskip}{\strut\enskip{ }}

\begin{document}\sf
\renewcommand{\sliderightmargin}{0mm}
\renewcommand{\slideleftmargin}{20mm}
\renewcommand{\slidebottommargin}{6mm}

\setcounter{slide}{-1}
\begin{slide}
\slidetitle{\Large aut}

Freek Wiedijk\\
University of Nijmegen

`35 years of Automath' workshop\\
Heriot-Watt University\\
Edinburgh

20020410, 16:00
\end{slide}

\begin{slide}
\slidetitle{an exercise by Knuth}

reimplementation of Automath\\
\adviwait
Christmas holiday (for fun) about five years ago
\adviwait

reduction strategy from paper by Zandleven\\
-- no new ideas there\\
-- $\beta\delta\eta$-reduction\\
-- program can trace reductions\\
-- program can limit number of reductions per type-check\\
-- program can keep statistics on number of reductions
\adviwait

implemented in C \quad -- portable, fast
\adviwait

both AUT-68 and AUT-QE\\
differences between AUT-68 and AUT-QE can be chosen independently
\adviwait

\textbf{not} AUT-SYNT\\
\adviwait
\textbf{not} `telescopes'
\vspace{-2em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{why you don't need it}

\adviwait
Automath is a dead language\\
\adviwait
-- if you want mathematics: use Mizar\\
\adviwait
-- if you want mathematics \textbf{and} automation of boring tasks: use HOL\\
\dashskip (or one of the `HOL clones': Isabelle, PVS)\\
\adviwait
-- if you want Automath: use Agda
\adviwait

Automath is still interesting in the spectrum of formal systems\\
-- many interesting ideas
\vfill
\end{slide}

\begin{slide}
\sectiontitle{repairing Jutting's Grundlagen}
\slidetitle{a stack of floppy floppies}

Jutting's formalization of Landau's `Grundlagen der Analysis'
\adviwait

corrupted electronic copy\\
-- a few bytes missing every kilobyte or so\\
-- no regularity in damage
\adviwait

using printed version: repair it \quad -- checker needed
\vfill
\end{slide}

\begin{slide}
\slidetitle{a Rosetta stone edition of the Grundlagen}

plan: to have an edition of the Grundlagen\\
-- left pages: German\\
-- right pages: Automath
\adviwait

already scanned/typed the German version\\
\adviwait
already labeled corresponding points in both files\\
\adviwait
still needed: {\TeX} hacking to merge the two texts in a nice layout
\vfill
\end{slide}

\begin{slide}
\slidetitle{the de Bruijn factor}

comparing sizes of informal math and formalization
\adviwait

\begin{center}
\begin{tabular}{ccc}
German {\TeX} &$\leftrightarrow$& Automath\\
\noalign{\vspace{-\smallskipamount}}
190K &3.9$\times$& 740K\\
\noalign{\bigskip}
compressed German {\TeX} &$\leftrightarrow$& compressed Automath\\
\noalign{\vspace{-\smallskipamount}}
42K &3.7$\times$& 160K
\end{tabular}
\end{center}
\adviwait
\medskip

for most formalizations:\\
de Bruijn factor turns out to be between 3 and 5
\adviwait

\textbf{fact to remember:}
\medskip
\begin{center}
\textcolor{slidegreen}{\Large de Bruijn factor {\large$\cong$} 4}
\end{center}
\vfill
\end{slide}

\begin{slide}
\sectiontitle{$\lambda$-typed versus $\Pi$-typed $\lambda$-calculus}
\slidetitle{Automath is incompatible with Coq}

PTS-style type theory:
$$x\;\vdash\; a : A : \mathord{*}\;\mbox{\quad then\quad}\vdash\;\lambda x.a : \Pi x.A : \mathord{*}$$
\adviwait
In Automath $\lambda$ and $\Pi$ are the same thing:
\vspace{-\smallskipamount}
$$\begin{array}{ccc}
\lambda x.a &\to& [x]a\\
\Pi x.A &\to& [x]A
\end{array}$$
\adviwait
In AUT-QE one has `type inclusion':
$$[x]A : [x]\mathord{*}{\quad\textbf{and}\quad}[x]A : \mathord{*}\medskip$$
\adviwait
not easy to `convert' AUT-QE $\lambda$-terms to Coq $\lambda$-terms\\
type theories are too different
\vspace{-2em}
\end{slide}

\begin{slide}
\slidetitle{$\lambda$-typed $\lambda$-calculus is the type theory from outer space}

in the later versions of de Bruijn's systems:\\
-- no type inclusion: not needed for Automath as a logical framework\\
-- binders never evaporate: $[x]A : [x]\mathord{*}$
\adviwait

advantages:\\
-- more regular than PTS-style\\
-- simpler than PTS-style \adviwait\quad $\to$ PTS-like presentation by de Groote
\adviwait

disadvantages:\\
-- predicative, but no straight-forward set theoretic model\\
\adviwait
-- for $\lambda$P as a logical framework there's correspondence theory\\
\dashskip for $\lambda$-typed type theory as a logical framework there's not
\adviwait
\medskip

I would like a `cross' of both systems:\\
$\lambda_0\equiv\lambda,\; \lambda_1\equiv\Pi,\; \lambda_2,\; \lambda_3,\; \ldots$
\vfill
\end{slide}

\begin{slide}
\sectiontitle{named variables, de Bruijn indices and term graphs}
\slidetitle{the two common approaches: named variables and de Bruijn indices}

two main implementation styles for $\lambda$-terms:
\begin{itemize}
\item[--] named variables:\\traditional logic, `first Automath', HOL Light, Agda, \dots
\item[--] de Bruijn indices:\\`second Automath', Mizar, Coq, \dots
\end{itemize}
\adviwait
\medskip

named variables often used with delayed substitutions
\vfill
\end{slide}

\begin{slide}
\slidetitle{term graphs where variables point back to $\lambda$s}

third implementation style: term graphs\\
variable points back at a $\lambda$
\adviwait

\textcolor{slidegreen}{if you have a hammer, everything looks like a nail}\\
-- not natural in functional programming languages\\
\dashskip ML, Haskell: they don't do it\\
-- natural in imperative programming languages\\
\dashskip C, Java\adviwait\quad $\to$ Martijn Oostdijk's Java implementation of Coq terms
\adviwait

no need for renumbering on substitutions
\adviwait

variables will sometimes point at $\lambda$s that don't `see' the variable!
\vfill
\end{slide}

\begin{slide}
\sectiontitle{Automath syntax}
\slidetitle{cutting lines into halves}

Automath `lines' have traditionally four `parts'\\
$f(x,y)\equiv c$
is written in Automath like
\begin{center}
\verb|  * x := --- : A|\\
\verb|x * y := --- : A|\\
\verb|y * f := c   : A|
\end{center}
\adviwait

`\verb|y *|' sets the context \adviwait \quad $\to$ becomes a first class citizen\\
\adviwait
\begin{center}
\verb|y * f := c : A|\qquad becomes two lines\quad\enspace
\begin{tabular}{c}\verb|y *|\\\noalign{\vspace{-\smallskipamount}}
\verb|f := c : A|\end{tabular}
\end{center}
\vfill
\end{slide}

\begin{slide}
\slidetitle{syntactic variants}

three ways to write `empty blocks' $=$ introduction of parameters
\begin{center}
\verb|x := EB  : A   f := c : A|\\
\verb|x := --- : A   f := c : A|\\
\verb|      [x : A]  f := c : A|\\
\end{center}
\adviwait
other notational differences:
\begin{center}
\begin{tabular}{ccc}
\verb|*| &$\leftrightarrow$& \verb|@|\\
\verb|:=| &$\leftrightarrow$& \verb|=|\\
\verb|:| &$\leftrightarrow$& \verb|_|\llap{\tt E}\rlap{\hspace{2cm}$\leftarrow$\quad`{\tt \_\^{}HE}'}\\
\verb|PN| &$\leftrightarrow$& \verb|'prim'|\\
\verb|[x,A]| &$\leftrightarrow$& \verb|[x:A]|\\
\verb|f := c : A| &$\leftrightarrow$& \verb|f : A := c|
\end{tabular}
\end{center}
\vspace{-2em}
\vfill
\end{slide}

\begin{slide}
\sectiontitle{extracting parts of an Automath book}
\slidetitle{extracting the minimal formalization that proves the theorem}

one of the features of the original Automath\\
`remove all lines that are not needed for a theorem'
\adviwait

example:
\begin{center}
\begin{tabular}{lr}
full Jutting formalization & 10691 lines\\
extract of `\verb|satz301f|' & 2825 lines
\end{tabular}
\end{center}
\adviwait
\medskip

\verb|satz301f|:
$$r + si = t + ui \;\Rightarrow\; s = u$$
\vfill
\end{slide}

\begin{slide}
\slidetitle{the primitive notions of the Grundlagen}

Automath axioms are called `primitive notions'\\
`what are the axioms of this formalization?'\\
-- minimal formalization that contains exactly the primitive notions

\adviwait
Grundlagen\\
-- 32 primitive notions
\adviwait
\begin{center}
\verb|con|, \verb|et|, \verb|is|, \verb|refis|, \verb|isp|, \verb|ind|, \verb|oneax|\\
\verb|fisi|, \verb|ot|, \verb|in|, \verb|inp|, \verb|otax1|, \verb|otax2|\\
\verb|pairtype|, \verb|pair|, \verb|first|, \verb|second|\\
\verb|pairis1|, \verb|firstis1|, \verb|secondis1|\\
\verb|set|, \verb|esti|, \verb|setof|, \verb|estii|, \verb|estie|, \verb|isseti|\\
\verb|nat|, \verb|1|, \verb|suc|, \verb|ax3|, \verb|ax4|, \verb|ax5|
\end{center}
\vfill
\end{slide}

\begin{slide}
\sectiontitle{the de Bruijn principle and `Automath-single line' terms}
\slidetitle{an analogy}

\begin{center}
\begin{tabular}{ccc}
machine code &$\leftrightarrow$& $\lambda$-term\\
\noalign{\vspace{-\smallskipamount}}
`binary' && `proof object'\\
\noalign{\bigskip}
assembler &$\leftrightarrow$& Automath, Coq\\
\noalign{\vspace{-\smallskipamount}}
&& `line based'\\
\noalign{\bigskip}
Pascal, C, Java &$\leftrightarrow$& Mizar, Isabelle/Isar\\
\noalign{\vspace{-\smallskipamount}}
&& `block structured'
\end{tabular}
\end{center}
\vfill
\end{slide}

\begin{slide}
\slidetitle{generating huge $\lambda$-terms}

de Bruijn's AUT-SL or AUT-$\Delta\Lambda$\adviwait
\quad $\to$ Nederpelt and de Groote
\adviwait

a whole `book' as one big $\lambda$-term
\adviwait

a directed graph with 5 kinds of nodes:

\begin{tabular}{cc}
& out-degree:\\
local definition & 3\\
$\lambda$-abstraction & 2\\
application & 2\\
variable & 1\\
`type' & 0
\end{tabular}
\adviwait
\medskip

de Bruijn indices: starting from 0, writing 0 with 0 digits
\adviwait

\textcolor{slidered}{{\tt aut -Q -g 320 grundlagen.aut}}: 1.8M of proof term
\adviwait
\adviembed{autterm}
\vspace{-2em}
\vfill
\end{slide}

\begin{slide}
\sectiontitle{performance of proof assistants}
\slidetitle{procedural versus declarative proof checkers}

proof styles: who does the proof?\\
-- procedural: the computer, directed by the human\\
\dashskip interactive, `tactics'\\
-- declarative: the human, checked by the computer\\
\dashskip batch
\adviwait

most current systems are procedural
\adviwait

declarative systems: Automath, Agda, Mizar
\vfill
\end{slide}

\begin{slide}
\slidetitle{performance figures: Automath, Metamath, Mizar, Coq}

speed in lines checked per second:
\begin{center}
aut\\\textcolor{slidegreen}{\quad 30$\times$ as fast as\quad}\\Mizar\\
\textcolor{slidegreen}{\quad 30$\times$ as fast as\quad}\\Coq
\end{center}
\adviwait

aut checks the Grundlagen in 0.6 seconds:
\adviwait
\adviembed{autterm}
\adviwait

however: aut has never been stress-tested\\
(maybe forgets to check something or checks it wrong)\\
\adviwait
(I don't hope so!)
\adviwait
\adviembed{autterm}
\adviwait

Norman Megill's Metamath:\\
similar program (also written in C), similar speed\\
-- a few seconds to check the whole Metamath library
\vspace{-2em}
\vfill
\end{slide}

\begin{slide}
\sectiontitle{Automath and the fourteen provers of the world}
\slidetitle{where do the current provers differ from Automath?}

properties Automath doesn't have:
\adviwait

-- calculations can be proved automatically, `Poincar\'e principle'\\
\adviwait
\vspace{-\smallskipamount}%
\dashskip (HOL, PVS, Coq, Otter, Isabelle, ACL2, PhoX, IMPS, Theorema,\\
\dashskip Lego, Nuprl)\\
\adviwait
-- extensible/programmable by the user\\
\adviwait
\dashskip (HOL, PVS, Coq, Isabelle, Nuprl)\\
\adviwait
-- powerful automation\\
\adviwait
\dashskip (HOL, PVS, Otter, Isabelle, ACL2, Theorema)\\
\adviwait
-- readable proof input files\\
\adviwait
\dashskip (Mizar, Isabelle, ACL2, Theorema)\\
\adviwait
-- large mathematical standard library\\
\adviwait
\dashskip (HOL, Mizar, PVS, Coq, Isabelle, IMPS, Nuprl)

%so: improvements in current systems\\
%-- automation, especially of `calculations'\\
%-- a more human proof input language\\
%-- big library
\vspace{-2em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{what can the current provers learn from Automath?}

\adviwait
-- $\lambda$-typed $\lambda$-calculus is a beautiful logical framework\\
\adviwait
-- graph representation of $\lambda$-terms works well\\
\adviwait
-- very big `de Bruijn principle' proof terms are possible\\
\adviwait
-- very fast checkers are possible\\
\adviwait
\dashskip maybe with the help of `proof caching'
\vfill
\end{slide}

\begin{slide}
\slidetitle{will the Automath/QED dream ever come true?}

\adviwait
I expect: yes!\\
\adviwait
I expect: not soon!\\
\adviwait
but even when not yet usable for mathematical practice:
\begin{center}
\textcolor{slidegreen}{formalizing mathematics is the best computer game there is}
\end{center}
\adviwait
the beauty of programming\dots$\,$but without fear of bugs!\\
\adviwait
the beauty of mathematics\dots$\,$and the computer takes care of all details!
\vfill
\end{slide}

\end{document}