\documentclass[namedreferences]{kluwer}
\usepackage{amssymb,url}
\usepackage[all]{xypic}
\begin{document}
\begin{opening}
\title{A new implementation of Automath}
\author{Freek \surname{Wiedijk} \email{freek@cs.kun.nl} \thanks{Research supported by EU working group `TYPES' and EU network `Calculemus'.}}
\institute{Department of Computer Science, University of Nijmegen, the Netherlands}
\begin{abstract}
This paper presents \texttt{aut}, a modern Automath checker.
It is a straight-forward re-implementation of the Zandleven Automath checker from the seventies.
It was implemented about five years ago, in the programming language C.
It accepts both the AUT-68 and AUT-QE dialects of Automath.
This program was written to restore a damaged version of Jutting's translation of Landau's \emph{Grundlagen}.
%
Some notable features:
\begin{itemize}
\item
It is fast.
% It is 30 times as fast as Mizar, which itself is 30 times as fast as Coq.
On a 1GHz machine it will check the full Jutting formalization (736K of non-whitespace Automath source) in 0.6 seconds.
\item
Its implementation of $\lambda$-terms does not use named variables or de Bruijn indices (the two common approaches) but instead uses a graph representation.
In this representation variables are represented by pointers to a binder.
\item
The program can compile an Automath text into one big `Automath single line' style $\lambda$-term. It outputs such a term using de Bruijn indices.
(These $\lambda$-terms cannot be checked by modern systems like Coq or Agda, because the $\lambda$-typed $\lambda$-calculi of de Bruijn are different from the $\Pi$-typed $\lambda$-calculi of modern type theory.)
\end{itemize}
The source of \texttt{aut} is freely available on the Web at the address
\url{}.
\end{abstract}
\keywords{Automath, formalized mathematics, proof objects, type theory.}
\end{opening}
\section{Introduction}
\subsection{Automath}
This paper describes an implementation of the mathematical language
Automath.
The Automath project was the first significant attempt to use a
computer to verify the correctness of mathematical texts that
have been spelled out in full detail.
The Automath languages were designed by N.G.~de Bruijn in the
late sixties.
The Automath project was very active during the seventies,
but it died when its funding stopped.
However, Automath keeps having a strong influence on the current
practice of mathematical
proof checking.
The standard reference about Automath is \cite{ned:geu:vri:94}.
This is a compilation of almost all important Automath publications.
It contains as (A.3) a good introduction to Automath, \cite{daa:73}.
The main important Automath paper that is missing from this collection is
the paper \cite{bru:91} about telescopes.
The Automath language has several variants.
The main dialects of the language are AUT-68, AUT-QE, AUT-SYNT,
AUT-$\Pi$, AUT-SL and AUT-$\Delta\Lambda$.
The first two have been implemented.
The third and fourth are improvements of the
first two that never have been implemented, although texts have
been written in them.
The last two are variants that are not intended for writing texts,
but for compiling texts into.
\subsection{Grundlagen}
The largest existing Automath formalization is the translation of a small
mathematics book.
The book is \emph{Grundlagen der Analysis} by Edmund Landau \cite{lan:30}.
It treats the definition of the field of complex numbers.
It consists of 161 pages of German text, which is divided in 301 `S\"atze'
(theorems).
The translation was done by Bert van Benthem Jutting.
It is reported on in his PhD thesis \cite{jut:79}.
The \emph{Grundlagen} consists of five chapters, which correspond
to $\mathbb{N}^+$, $\mathbb{Q}^+$, $\mathbb{R}^+$,
$\mathbb{R}$ and $\mathbb{C}$.
There are two translations of chapter 4.
The first translation follows the German original and defines
$\mathbb{R}$ as the union of two disjoint copies of $\mathbb{R}^+$ (for
the positive and negative numbers) and
of a singleton set (for the zero).
The second translation, which is called 4a,
defines $\mathbb{R}$ as equivalence classes
of pairs of elements of $\mathbb{R}^+$, where two pairs are considered
equivalent if they have the same difference.
The structure of the Automath translation of the \emph{Grundlagen} is:
$$
\xymatrix{
1\ar@{-}[r] & 2\ar@{-}[r] & 3\ar@{-}[r]\ar@{-}[dr] & 4\setbox0=\hbox{a}\hspace{\wd0}&\\
&&&4\hbox{a}\ar@{-}[r]&5
}
$$
This means that the translation of chapter 5 should be checked as a
continuation of the
second translation of chapter 4.
The file \texttt{grundlagen.aut} consists of the concatenation of
1, 2, 3, 4a and 5.
It contains 10702 lines of Automath and its size is 736K.
A {\TeX} version of the German original is 189K.
This means that the Automath version of the book is a factor of $3.9$ larger
than the original.
The Automath file does not contain any whitespace so it
makes more sense to compare the sizes of these files when
they are compressed with \texttt{gzip}.
In that case the factor becomes $\mbox{155K}/\mbox{42K} = 3.7$.
In \cite{wie:00} this factor is called the \emph{de Bruijn factor}.
(For the other formalizations that are investigated in \cite{wie:00}
the de Bruijn factor also lies around 4.)
\subsection{A new implementation}
In the early nineties, I got a stack of $5{1\over 4}$-inch `soft' floppy disks
containing a copy of the Automath files of the
\emph{Grundlagen}
through my friend Hans Mulder,
who at that time was sharing an office with Bert van Benthem Jutting.
These files had been copied from computer to computer during the
years, and somehow had gotten corrupted.
At several points in the files some bytes would be missing, apparently without
any discernible pattern.%
\footnote{Specifically there were
$14+15+33+35+32+59+36+35+27+53+64+33+35+21+42=534$ bytes missing.
Because of this, five lines had been joined.}
Together with the floppies I got a copy of \cite{jut:76},
which is a five volume technical report containing a full print-out of the
non-corrupted files.
The original Automath checkers already were no
longer functional at that time.
They had been written in a programming language that did not exist
anymore, for a computer that did not exist anymore.
A simple \texttt{yacc} parser quickly pointed out most of the corruption,
after which I typed in the missing pieces from the print-out.
However, to be sure that I had repaired the files correctly, I needed a new Automath
checker.
\subsection{Modern systems}
\cite{wie:02:1} is a comparison of
fifteen systems
for formalization of mathematics in the spirit of
the Automath project.
These systems are HOL, Mizar, PVS, Coq, Otter, Isabelle, Agda, ACL2, PhoX,
IMPS, Metamath, Theorema, Lego, Nuprl and $\Omega$mega.
Of these systems Coq, Agda and Lego are closest to Automath.
However they are sufficiently different from Automath, that they
are not usable for checking the Automath version of the \emph{Grundlagen}.
See Sections \ref{diffs} and \ref{qe-pts} below for a description of the difference between the
type system of Automath and that of the modern systems.
Several of these systems -- HOL, PVS, Coq, Isabelle, PhoX, Lego and Nuprl --
are also descendants of the LCF system \cite{gor:mil:wad:79}.
They are interactive systems that operate on a `proof state'
by applying `tactics'.
This is very different from Automath, where one writes $\lambda$-terms
that are checked by a non-interactive checker.
The Agda system from Sweden, implemented by Catarina Coquand,
uses a combination of the Automath
approach and the LCF approach.
Its tactics do not operate on a proof state, but build the $\lambda$-term
in the text.
Both its type theory and its `user experience'
are the closest that one can get to Automath in a serious modern system.
The Coq system from France \cite{coq:02},
originally implemented by G\'erard Huet
and Thierry Coquand, and now being developed by a team under direction
of Christine Paulin, is the most popular of the Automath descendants.
Various pieces of mathematics have been formalized in Coq.
For instance there are:
a development of real analysis by Micaela Mayero,
a development of category theory by Amokrane Sa\"\i bi,
a proof of the correctness of Buchberger's algorithm by
Laurent Th\'ery and Henrik Persson,
a constructive proof of
the fundamental theorem of algebra by Herman Geuvers, Randy Pollack, Freek Wiedijk and
Jan Zwanenburg,
and a significant part of the proof of the four color theorem by
George Gonthier and Benjamin Werner.
\section{The program}
We will now describe the \texttt{aut} program.
We will first present a fragment of Automath to give an impression of
the language that the program checks.
Then we will describe the implementation of the program
and list its features.
\subsection{Example of a fragment of Automath}
Here is the text of `Satz 137' (both the statement and the proof)
from page 75 of the German version of the \emph{Grundlagen}:
\begin{quote}
\textbf{Satz 137:}
\textit{Aus
$$\xi > \eta,\quad \zeta > \upsilon$$
folgt
$$\xi + \zeta > \eta + \upsilon.$$}
\textbf{Beweis:}
Nach Satz 134 ist
$$\xi + \zeta > \eta + \zeta$$
und
$$\eta + \zeta = \zeta + \eta > \upsilon + \eta = \eta + \upsilon,$$
also
$$\xi + \zeta > \eta + \upsilon.$$
\end{quote}
\noindent
The statement of `Satz 134' that this proof refers to is
`Aus $\xi > \eta$ folgt $\xi + \zeta > \eta + \zeta$.'
And here is the Automath translation of `Satz 137',
which is called \texttt{satz137}:%
\footnote{The Automath fragment that is shown here corresponds to lines
3330, 3379, 3405, 3553, 3844--3849
of the file \texttt{grundlagen.aut}.}
\begin{verbatim}
* ksi := --- ; cut
ksi * eta := --- ; cut
eta * zeta := --- ; cut
zeta * upsilon := --- ; cut
upsilon * m := --- ; more(ksi,eta)
m * n := --- ; more(zeta,upsilon)
\end{verbatim}
\begin{verbatim}
+3137
n * t1 := satz134(ksi,eta,zeta,m)
; more(pl(ksi,zeta),
pl(eta,zeta))
n * t2 := ismore12(pl(zeta,eta),pl(eta,zeta),
pl(upsilon,eta),pl(eta,upsilon),
compl(zeta,eta),compl(upsilon,eta),
satz134(zeta,upsilon,eta,n))
; more(pl(eta,zeta),
pl(eta,upsilon))
-3137
\end{verbatim}
\begin{verbatim}
n * satz137 := trmore(pl(ksi,zeta),pl(eta,zeta),
pl(eta,upsilon),t1".3137",t2".3137")
; more(pl(ksi,zeta),
pl(eta,upsilon))
\end{verbatim}
From this example it will be clear that an Automath text or \emph{book}
consists of \emph{lines}.
Each of these lines has four parts: a \emph{context} part,
an \emph{identifier} part, a \emph{middle} part and a \emph{category} part.
There are three kinds of lines: \emph{block opening} lines (these are
the lines that have \texttt{---} as the middle part), \emph{primitive
notion} lines (these are lines that have \texttt{PN} as the middle part,
which do not occur in this example) and \emph{abbreviation} lines.
Note that the identifier of a block opening line does not just denote
a variable, but also a whole context.
A block opening line extends such a context with a new variable.
For instance when used in the context part,
the identifier \texttt{zeta} represents the context
$\texttt{ksi}, \texttt{eta}, \texttt{zeta} \vdash \ldots$
The text contains a small \emph{paragraph} called \texttt{3137}
(this identifier is a combination of chapter 3 and `Satz' 137).
The line \texttt{+3137} opens it and the line \texttt{-3137} closes it
again.
The \emph{index} \texttt{".3137"} is used to refer to identifiers inside
the paragraph.
This Automath fragment defines the three functions \texttt{t1(ksi,eta,}\penalty100\texttt{zeta,upsilon,m,n)}, \texttt{t2(ksi,eta,zeta,upsilon,m,n)} and \texttt{satz137}\penalty100\texttt{(ksi,eta,zeta,upsilon,m,n)}.
These correspond to the three steps in the proof of `Satz 137'.
We will now briefly explain the meaning of the function \texttt{t1}.
The meanings of \texttt{t2} and \texttt{satz137} are similar.
The meanings of the functions occurring
in the middle parts of their definitions can be guessed by looking at the
German original of this text.
In Automath, mathematical objects have types, and their types have type \texttt{TYPE}.
Proofs also have types (corresponding to propositions), and these propositional types have
type \texttt{PROP}.
In this example the variable \texttt{ksi} represents a positive
real number, and its type \texttt{cut} (an abbreviation of `Dedekind cut')
represents the type of positive real numbers.
The type of the type \texttt{cut} itself is \texttt{TYPE}.
The function \texttt{t1} represents
a proof of the statement $\xi + \zeta > \eta + \zeta$.
It is a `proof object' with type \texttt{more(pl(ksi,zeta),pl(eta,zeta))}.
This type represents a proposition and has itself type \texttt{PROP}.
The expression \texttt{t1(ksi,eta,zeta,upsilon,m,n)} is an abbreviation
of the expression \texttt{satz134(ksi,eta,zeta,m)}.
Both expressions have the same type: \texttt{more(pl(ksi,zeta),pl(eta,zeta))}.
This abbreviation means that whenever a well-typed expression
$\texttt{t1(}\xi\texttt{,}\eta\texttt{,}\zeta\texttt{,}\upsilon\texttt{,}m\texttt{,}n\texttt{)}$ is encountered,
it behaves exactly as if it had been the expression $\texttt{satz134(}\xi\texttt{,}\eta\texttt{,}\zeta\texttt{,}m\texttt{)}$.
Not all arguments of \texttt{t1} are ordinary mathematical objects: the
last two arguments are \emph{proof objects}.
In contrast with classical mathematics, in Automath these can be used as
arguments of functions.
The argument \texttt{m} is a proof object of the propositional type \texttt{more(ksi,eta)} and \texttt{n} is a proof object of type \texttt{more(zeta,upsilon)}.
Therefore \texttt{t1} maps proofs of $\xi > \eta$ and $\zeta > \upsilon$
to a proof of $\xi + \zeta > \eta + \zeta$
(the second proof argument
is not used in the body of \texttt{t1}, and it is not needed
for the inference, but it is present in the parameter list).
In logical terms this means that \texttt{t1} corresponds to the sequent:
$$\xi > \eta\,,\;\; \zeta > \upsilon \;\vdash\; \xi + \zeta > \eta + \zeta$$
Note that Automath is a rather primitive language.
An Automath text just consists of a sequence of abbreviations of $\lambda$-terms.
There is no proof automation at all.
Still the Grundlagen translation manages to faithfully follow the German
original.
\subsection{Implementation}
The \texttt{aut} checker is a straight-forward re-implementation of
the program that is described in \cite{zan:73}.
Algorithmically it does not contain any new ideas.
\texttt{aut} is written in highly portable ANSI C.
It is a one pass batch program that reads an Automath book from the standard
input stream and prints error messages on the standard error stream.
For the lexer and parser of \texttt{aut},
the standard tools \texttt{flex} and \texttt{yacc}
have been used.
The source code of the \texttt{aut} is 3048 lines long, including the
input files for \texttt{flex} and \texttt{yacc}.
Writing the program took about one month of work.
It was written about five years ago in the spare time of the author,
and took most of a Christmas vacation.
\subsection{Features}
The \texttt{aut} program has the following features:
\begin{itemize}
\item
\texttt{aut} knows both the AUT-68 and AUT-QE languages.
See Section \ref{lang} below for the details of the languages
that \texttt{aut} can check.
\item
To type check, \texttt{aut} has to check the convertibility of
certain types (the type of a term versus the type that the context
of that term expects).
To establish this convertibility, \texttt{aut} applies
$\beta$-, $\delta$- and $\eta$-reductions.
It follows
a similar reduction strategy to the one in the Zandleven checker.
\texttt{aut} can trace reductions with the \texttt{-t} flag.
It can turn off the $\eta$-reductions with the \texttt{-e} flag.
\item
The \texttt{aut} program can print various summaries.
The flags that are related to this are:
\begin{center}
\begin{tabular}{ll}
\emph{flag} & \emph{information printed} \\
\hline
\texttt{-d} & duration of the check in seconds \\
\texttt{-l} & counts of the various kinds of lines in the book \\
\texttt{-m} & amount of memory used \\
\texttt{-r} & reduction counts for the various kinds of reduction \\
\texttt{-v} & version of the program
\end{tabular}
\end{center}
The \texttt{-Z} flag is an abbreviation of the combination \texttt{-dlmrv}.
With this flag, for the file \texttt{grundlagen.aut} the summary that will
be printed is:%
\footnote{The `\texttt{0} \texttt{seconds}' means that the check stayed
within the same second.}
{
\makeatletter
\def\verbatim@font{\footnotesize\tt}
\makeatother
\begin{verbatim}
8583 beta reductions, 20004 delta reductions, 2 eta reductions
32 + 6878 = 6910 definitions, 4297 + 6910 = 11207 lines
96 blocks = 3069 kilobytes
0 seconds = 0 minutes 0 seconds
aut 4.2, (c) 1997 by satan software
\end{verbatim}
}
\item
If an Automath text is not correct, the correctness check will generally
take a very long time.
This means that Automath correctness, although theoretically decidable,
is in practice only semi-decidable.
A correct line generally can be checked with only a few reductions%
\footnote{The most complicated line in \texttt{grundlagen.aut} is line 9832,
which needs 74 reductions.}
but to establish the incorrectness of
an incorrect line, \texttt{aut} will often need many reductions,
and for all practical purposes the check will behave as if the program
hangs.
(The reason why Automath has this problem and more modern systems
do not, is that in Automath definitions are `transparent' by default.
Therefore Automath will keep expanding definitions for a long time when
a line is not well typed.)
\texttt{aut} can limit the number of reductions per type check with the
\texttt{-n} flag.
If the number of reductions for a type check
exceeds this limit, the program will
give a message that the line probably is incorrect and then will continue
with the rest of the file.
\item
The \texttt{aut} program offers the possibility to have a definition be `opaque':
in that case it will not be used in $\delta$-reductions
(transparent and opaque function definitions are also present in the Coq system).
Opaque abbreviation lines are
indicated by a \texttt{\~{}} symbol in front of
the middle part of the line.
With the \texttt{-f} flags these opaque definitions are considered
to be transparent again.
\item
The \texttt{aut} program will print the Automath book in a standard form
on the output
if it is given the \texttt{-y} flag.
This is not a pretty-printer, as the printed Automath will not contain
any white space.
With the \texttt{-k} flag the user can control whether implicit arguments
should be omitted or printed (see Section \ref{excerpt:satz1} below
for a discussion of implicit arguments).
The original Automath from the seventies could extract an \emph{excerpt}
for a line in an Automath book.
\texttt{aut} will do this if it is given the \texttt{-x} flag.
See Section \ref{excerpt} below for an example of such an excerpt.
\texttt{aut} can also generate an excerpt for all
primitive notion lines (the `axioms') in the Automath book.
\item
\texttt{aut} will `compile' an Automath book to one big $\lambda$-term
if it is given the \texttt{-g} flag.
See Section \ref{compile} below for a description of this feature.
\end{itemize}
\section{The languages}\label{lang}
The \texttt{aut} program both knows the AUT-68 and AUT-QE dialects
of the Automath language, but it also can check languages
that are `in between' AUT-68 and AUT-QE.
There are various flags that control various features of the
language that is checked as described in Section \ref{dialects} below.
With all flags in the `AUT-68 position' \texttt{aut} will check
AUT-68, with all flags in the `AUT-QE position' \texttt{aut}
will check AUT-QE, but with some flags in one position and
some in the other, \texttt{aut} will check a language that
is in between these two languages.
\subsection{Language flags}
There are four flags that affect the type theory of the language that
\texttt{aut} checks.
\begin{itemize}
\item[\texttt{-a}]
\emph{Allow abstractions of degree one.}
This flag has to be chosen for AUT-QE.
Without this flag, there are no $\lambda$-abstractions allowed
of which the body has degree one, i.e., of which the body is \texttt{TYPE}
or \texttt{PROP}.
In \texttt{grundlagen.aut} such an abstraction occurs for instance in
lines 221--222, which is the definition
of the universal quantifier:
\begin{center}
\begin{verbatim}
* sigma := --- ; TYPE
sigma * p := --- ; [x,sigma]PROP
p * all := p ; PROP
\end{verbatim}
\end{center}
The term \texttt{[x,sigma]PROP} in the second line
is not allowed without the \texttt{-a} flag.
(The Automath notation \texttt{[x,sigma]}
both is used for $\lambda$- and $\Pi$-abstraction.
See Section \ref{diffs} below for a discussion of the identification of
$\lambda$ and $\Pi$ in Automath.)
\item[\texttt{-b}]
\emph{Omit abstractions when calculating categories of degree one.}
This flag has to be chosen for AUT-68.
Consider the following fragment of the AUT-68 text (D.1) from
page 689 of \cite{ned:geu:vri:94}:
\begin{quote}
\begin{verbatim}
{1.1} * bool := PN ; TYPE
{1.2} * x := --- ; bool
{1.3} x * TRUE := PN ; TYPE
\end{verbatim}
\begin{verbatim}
{1.4} * CONTR := [v,bool]TRUE(v) ; TYPE
\end{verbatim}
\end{quote}
The expression \texttt{TRUE(v)} has category \texttt{TYPE}.
Without the \texttt{-b} flag the expression \texttt{[v,bool]TRUE(v)}
gets the category \texttt{[v,bool]TYPE}.
With the \texttt{-b} flag the abstraction \texttt{[v,bool]} is
omitted and it gets the correct category \texttt{TYPE}.
\item[\texttt{-p}]
\emph{Allow the \emph{\texttt{PROP}} type.}
This flag has to be chosen for AUT-QE.
Automath has two basic `types of types' called \texttt{TYPE} and \texttt{PROP}.
The reason for distinguishing between the two is that without this
distinction the `propositions as types' interpretation
causes the double negation law to behave like a Hilbert choice operator.
Without the \texttt{-p} flag only \texttt{TYPE} is allowed.
With this flag, also \texttt{PROP} may be used.
\item[\texttt{-q}]
\emph{Allow type inclusion.}
This flag has to be chosen for AUT-QE.
The AUT-QE language has type inclusion.
An expression that has category \texttt{[x$_1$,A$_1$]$\ldots$[x$_n$,A$_n$]TYPE}, also
is correct for category \texttt{[x$_1$,A$_1$]$\ldots$[x$_k$,A$_k$]TYPE}
when $k < n$.
With the \texttt{-q} flag \texttt{aut} checks the text with type inclusion.
\end{itemize}
\subsection{Some other flags}
There are some other flags that affect the language that \texttt{aut} checks.
However, these flags are not type related.
\begin{itemize}
\item[\texttt{-c}]
\emph{Put context parameters in front of other definitions.}
Consider the following Automath fragment:
\begin{quote}
\begin{verbatim}
* A := PN ; TYPE {1}
* x := --- ; A {2}
x * y := --- ; A {3}
+p {4}
* x := PN ; A {5}
y * f := x ; A {6}
-p {7}
\end{verbatim}
\end{quote}
The \texttt{x} on the sixth line, is it the \texttt{x} from the
second line or is it the \texttt{x} from the fifth line?
The \texttt{aut} program uses the same name space for the identifiers in
all three kinds of lines.
Therefore the \texttt{x} in the definition of \texttt{f}
is taken to be the \texttt{x} from the fifth line, because
that is the last definition of \texttt{x} that is in scope.
However to be able to check the \emph{Grundlagen} translation correctly,
the parameters of the definition have to be given priority over the order of
the definitions in the file.
Therefore with the \texttt{-c} flag, \texttt{aut} considers the
\texttt{x} from the second line to be the meaning of the \texttt{x}
in the definition of \texttt{f}.
\item[\texttt{-o}]
\emph{Disallow explicit paragraph references in parameters.}
With this flag, a parameter of a function definition is not
allowed to be explicitly qualified with an index that refers
to a paragraph.
\item[\texttt{-s}]
\emph{Disallow paragraph re-openers without a star.}
With this flag, \texttt{aut} will insist on the \texttt{*}
in the \texttt{+*p} line that re-opens a
paragraph \texttt{p} that has been closed before.
\end{itemize}
\subsection{AUT-68, AUT-QE, AUT-$\Delta\Lambda$}\label{dialects}
The three Automath languages that are relevant for \texttt{aut} are
AUT-68, AUT-QE and AUT-$\Delta\Lambda$.
\texttt{aut} will accept a language that is in the intersection
of AUT-68 and AUT-QE if it is invoked with no flags at all.
\texttt{aut} will check the input as AUT-68 with the \texttt{-b} flag.
\texttt{aut} will check the input as AUT-QE with the \texttt{-Q} flag.
This is an abbreviation of the combination of flags \texttt{-acopqs}.
However the \emph{Grundlagen} translation already will be accepted
with only the \texttt{-acpq} flags.
\texttt{aut} cannot check AUT-$\Delta\Lambda$.
However, it can compile its input to an AUT-$\Delta\Lambda$ term,
as described in Section \ref{compile} below.
This term will only make sense as AUT-$\Delta\Lambda$ for the language
that \texttt{aut} checks with the \texttt{-a} flag.
\subsection{Syntactical variants}
In the Automath literature one finds various syntactical conventions.
\texttt{aut} tries to be forgiving in this respect, and accepts
different notations for the same notions.
For instance, it accepts as alternatives:
\begin{center}
\begin{tabular}{lcll}
\texttt{*} &$\leftrightarrow$& \texttt{@} \\
\texttt{:=} &$\leftrightarrow$& \texttt{=} \\
\texttt{---} &$\leftrightarrow$& \texttt{EB} \\
\texttt{PN} &$\leftrightarrow$& \texttt{PRIM} \\
\texttt{;} &$\leftrightarrow$& \texttt{:} \\
\texttt{;} &$\leftrightarrow$& \texttt{\underline{E}} & \rlap{(to be typed as `\texttt{\_\^{}HE}')} \\
\texttt{[x,A]} &$\leftrightarrow$& \texttt{[x:A]} \\
\texttt{TYPE} &$\leftrightarrow$& \texttt{'type'} \\
\texttt{.} &$\leftrightarrow$& \texttt{-}
\end{tabular}
\end{center}
Furthermore \texttt{aut} allows one to switch the order of the
middle and category parts.
Instead of writing:
\begin{center}
\texttt{x * f := t : A}
\end{center}
one is allowed to write:
\begin{center}
\texttt{x * f : A := t}
\end{center}
This is the natural way to write this line
considering its AUT-$\Delta\Lambda$ translation, because in that translation
a binder \texttt{[f:A]} occurs.
Finally, \texttt{aut} considers the context part of a line to be a first
class citizen that stands on itself.
At each point in the text there will be a `natural' context.
A line:
\begin{center}
\texttt{x * f := t : A}
\end{center}
will consist of two `halves':
\begin{center}
\quad\framebox{\texttt{x *}}\quad\framebox{\texttt{f := t : A}}
\end{center}
that can occur separately on their own.
The first half `sets' the context to \texttt{x}.
The second half defines the function \texttt{f} in the context that
is current at that point
(note that this line does not have a \texttt{*} at the start).
If there are several successive abbreviation lines without a context part, they
share the same context.
After a block opening line the context will be set to
the variable that is introduced in that line.
A block opening line (now without context part):
\begin{center}
\texttt{x := --- : A}
\end{center}
also may be written:
\begin{center}
\texttt{[x:A]}
\end{center}
The idea of first class context parts and the alternative syntax
for block opening lines both
have been taken from the \emph{Grundlagen} files.
See Section \ref{excerpt:satz1} below for an example of
an Automath text in this style.
When the context part does not need to be written for all lines,
it becomes ambiguous what the contexts are when one changes paragraphs.
Consider the following Automath fragment (as not all lines in this fragment have
a context part, not all of these lines have a \texttt{*}):
\begin{quote}
\begin{verbatim}
* A := PN ; TYPE
x := --- ; A
+p
y := --- ; A
-p
f := PN ; TYPE
* z := --- ; A
+*p
g := PN ; A
-p
\end{verbatim}
\end{quote}
\noindent
There are different choices possible for the `natural' contexts of \texttt{f} and \texttt{g}.
\texttt{aut} takes the context after the first \texttt{-p} to be the context
before the \texttt{+p} (instead of the context from `inside' the paragraph \texttt{p}), and the context after the \texttt{+*p} to be
the context just before this \texttt{+*p} (instead of `remembering' the old context from inside the paragraph \texttt{p}).
This means that it takes
the context of \texttt{f} to be \texttt{x} and the context of \texttt{g}
to be \texttt{z}.
This is consistent with the way that contexts behave in the \emph{Grundlagen} files.
\section{Efficiency}
We will compare the speed of the \texttt{aut} checker with the
checkers from the seventies.
We will then discuss some implementation issues that affect the
efficiency of the \texttt{aut} checker.
\subsection{Reduction counts and timings}
The \texttt{grundlagen.aut} file contains 32 primitive notion lines,
4297 block opening lines and 6878 abbreviation lines.
Here are some statistics on the number of reductions and the checking
times needed for this file, for the two Automath checkers from the seventies
and for the \texttt{aut} checker:
\begin{center}
\begin{tabular}{lccc}
\hline
& first checker & second checker & \texttt{aut} checker \\
\hline
$\alpha$-reductions & 8952 & -- & -- \\
$\beta$-reductions & 5485 & 6362 & 8583 \\
$\delta$-reductions & 16912 & 18939 & 20004 \\
$\eta$-reductions & 2 & 2 & 2 \\
\hline
checking time & 2112.8\rlap{ s} & 4116.1\rlap{ s} & 0.6\rlap{ s} \\
\hline
\end{tabular}
\end{center}
The second checker from the seventies
and the \texttt{aut} checker both do not use a named representation
of bound variables in $\lambda$-terms, so they do not need $\alpha$-reductions.
The difference in reduction counts are caused by the difference in reduction
strategies of those checkers.
Clearly the computers have become much faster since the seventies!
The speed of \texttt{aut} is compatible with the speed of the Metamath
system \cite{meg:97}, which is able to check its whole library in seconds.
This system also is a one pass batch checker for a simple proof language and it
is also written in C.
\subsection{Term representation}
The two common approaches to implement a type checker for typed
$\lambda$-calculus is using \emph{named variables} or using \emph{de Bruijn
indices}.
These are the natural choices when using a functional programming language
like ML or Haskell.
The \texttt{aut} checker takes the less common approach (in
type checking of typed $\lambda$-calculi) of using a \emph{term graph
representation}.
This is the natural choice when using a procedural programming language
like C or Java.
Here is the $K$ combinator $\lambda x y.x$ in these three different
representations
(in this paper we count de Bruijn indices from zero, cf.~item \ref{bound} in Section \ref{deltalambda} below, so the middle representation
has a 1 instead of a 2):
$$
\xymatrix{
\lambda x\ar[d] \\
\lambda y\ar[d] \\
x
}
\hspace{2cm}
\xymatrix{
\lambda\ar[d] \\
\lambda\ar[d] \\
1
}
\hspace{2cm}
\xymatrix{
\lambda\ar[d] \\
\lambda\ar[d] \\
\cdot\ar@/_2pc/[uu]
}
$$
An advantage of this third representation is that one does not
need to be concerned with $\alpha$-conversions, and also that
one does not need to renumber de Bruijn indices when substituting
a term inside another term.
An interesting property of the term graph representation is that one
will get terms in which variables point to $\lambda$-nodes that
do not `see' these variables.
I.e., variables will not always be
in the sub-term that is `under' their $\lambda$-node.
%
For instance, suppose we have a term $\lambda x.(\lambda y.y) x$,
and want to calculate the $\beta$-reduct of the
sub-term $(\lambda y.y) x$. Now if we do
not reduce the full term but just calculate the reduct of
the sub-term, then the term graph that will be in memory
after the reduction will be:
$$
\xymatrix{
& \lambda\ar[d] \\
& @\ar[dl]\ar[d]\ar@{.>}[rrrr]_{\beta} &&&& \cdot\ar@/_.8pc/[ullll] \\
\cdot\ar@/^1pc/[uur] & \lambda\ar[d] \\
& \cdot\ar@/_1.5pc/[u]
}
$$
(The dotted arrow does not correspond to something in memory:
it just shows where the $\beta$-reduction has happened.)
The node for the result of the reduction, $x$, will still point
to the original $\lambda x$-node, but it will
not be in the sub-term that is under this $\lambda$.
\texttt{aut} treats its term graphs in a purely functional way:
it will only generate new nodes, but it will never modify parts of
the graph that already exist.
\subsection{Memory management}
The \texttt{aut} checker is a non-interactive one pass program.
This means that its memory management can be extremely simple.
It does not need a garbage collector.
It also does not need to free memory block-by-block.
The \texttt{aut} program allocates memory on a stack.
It will never free memory blocks explicitly, so this stack will just grow.
When it finishes parsing a line and starts the type check of that line,
it remembers the current position of the stack pointer.
Then when it finishes type checking the line it resets the
stack pointer to this remembered position, effectively
freeing all memory that was used during the type check, and moves
on to the next Automath line.
This means that the memory consumption of the program will grow
in a `saw tooth' pattern.
It also means that memory allocation and
de-allocation will be fast.
\section{Printing excerpts}\label{excerpt}
The \texttt{aut} program can extract an \emph{excerpt} of a
line in an Automath book.
This is the minimal subset of the lines in the book that
contains the given line and in which all references from the lines
in the subset point to lines in the subset.
We will present an example of such an excerpt.
\subsection{Excerpt of Satz 1}\label{excerpt:satz1}
Here is the text of `Satz 1' (both the statement and the proof)
from page 27 of the German version of the \emph{Grundlagen}:
\begin{quote}
\textbf{Satz 1:}
\textit{Aus
$$x \ne y$$
folgt
$$x' \ne y'.$$}
\textbf{Beweis:}
Sonst w\"are
$$x' = y'$$
also nach Axiom 4
$$x = y.$$
\end{quote}
This `Axiom 4' that this proof refers to is the fourth Peano axiom.
And here is the excerpt of \texttt{satz1}%
\footnote{The definition of \texttt{satz1} is line 980 of the file \texttt{grundlagen.aut}.}
from the Automath translation:
\begin{verbatim}
+l
[a:PROP][b:PROP]
imp:=[x,a]b:PROP
[c:PROP][i:imp(a,b)][j:imp(b,c)]
trimp:=[x,a]<i>j:imp(a,c)
@con:=PRIM:PROP
a@not:=imp(con):PROP
+imp
b@[n:not(b)][i:imp(a,b)]
th3:=trimp(con,i,n):not(a)
-imp
@[sigma:TYPE]
+e
[s:sigma][t:sigma]
is:=PRIM:PROP
+st
+eq
+landau
+n
@nat:=PRIM:TYPE
[x:nat][y:nat]
is:=is(nat,x,y):PROP
nis:=not(is(x,y)):PROP
@suc:=PRIM:[x,nat]nat
ax4:=PRIM:[x,nat][y,nat][u,is(suc,suc)]is(x,y)
[x:nat][y:nat][n:nis(x,y)]
+21
[i:is(suc,suc)]
t1:=ax4:is(x,y)
-21
satz1:=th3"l-imp"(is(suc,suc),is(x,y),n,[u,is(suc
,suc)]t1"-21"(u)):nis(suc,suc)
-n
-landau
-eq
-st
-e
-l
\end{verbatim}
This is a correct AUT-QE text on its own.
When printing an Automath text, by default \texttt{aut}
omits as many implicit arguments as possible.
Implicit arguments are an Automath feature:
one is allowed to omit initial arguments to a function if they happen to coincide with
the corresponding parameters in the definition of the function.
For instance consider the term \texttt{imp(con)} in the definition
of the \texttt{not} function.
This really is the term \texttt{imp(a,con)} but because \texttt{imp}
is defined in the form \texttt{imp(a,b)},
the first argument of
definition and usage are the same and so the \texttt{a} may be omitted.
In this specific example the usage of implicit arguments is only confusing,
but implicit arguments become essential in Automath
when one works with many function
definitions that share a large part of their context.
This excerpt shows that Automath has two kinds of function application.
There is function application on the level of the $\lambda$-calculus
(for instance in the term \texttt{<i>j}, which means `$j(i(x))$'), and there is instantiation
of defined functions (for instance in the term \texttt{imp(a,b)}).
The first kind is written with angular brackets,
it has only one argument, and this argument precedes the function
(cf.~item \ref{apporder} in Section \ref{deltalambda}).
The second kind is written with round brackets,
there can be more than one argument, and these arguments follow the function symbol.
In AUT-$\Delta\Lambda$ (as well as in most modern higher order proof
assistants) both kinds of function application have been merged.
\section{Automath proof objects}\label{compile}
The \texttt{aut} checker can \emph{compile} an Automath book to an
AUT-$\Delta\Lambda$ proof object.
We will describe AUT-$\Delta\Lambda$ and then present an example
of such an Automath proof object.
\subsection{$\lambda$-typed versus $\Pi$-typed type theory}\label{diffs}
Automath is fundamentally different from the modern type theories,
which are called \emph{pure type systems} \cite{bar:92}.
In Automath the type of a $\lambda$-expression is itself again a
$\lambda$-expression.
In a pure type system the type of a $\lambda$-expression is a \emph{product type}
or $\Pi$-expression.
The Automath type theories traditionally have been
described in an algorithmic way (by presenting
a type checker), unlike the pure type systems which are generally described
by a deduction system of typing rules.
In \cite{gro:93} the Automath type theories are presented in a more
modern style.
The abstraction rule of a pure type system:
$$
{\Gamma, x{:}A \vdash B:C \quad \Gamma \vdash \Pi x{:}A.C : s \over
\Gamma \vdash \lambda x{:}A.B : \Pi x{:}A.C}
\mbox{\rlap{\enskip $s\in{\cal S}$}}
\eqno{(\emph{abstraction})}
$$
then becomes:
$$
{\Gamma, x{:}A \vdash B:C \over
\Gamma \vdash \lambda x{:}A.B : \lambda x{:}A.C}
\eqno{(\emph{abstraction})}
$$
This clearly is simpler.
The Automath application rule from \cite{gro:93} can be written as:
$$
{\Gamma \vdash F : G \quad \Gamma \vdash a : A \over
\Gamma \vdash Fa : Ga}
\mbox{\enskip \rlap{$G \equiv \lambda x{:}A.B$}}
\eqno{(\emph{application})}
$$
(This rule suggests to add \emph{$\Pi$-application} to pure type systems, with
a reduction rule:
$$(\Pi x{:}A.B)a \to B[x:=a]$$
Such a system is investigated in
\cite{kam:ned:96} and \cite{kam:blo:ned:99}.
In a sense this system is in between Automath and the pure type systems.)
We will briefly discuss the lack of popularity in the type theoretic community
of the $\lambda$-typed
type theories in Section \ref{lessons} below.
\subsection{AUT-$\Delta\Lambda$}\label{deltalambda}
If one streamlines Automath to its simplest form,
one ends up with a system that on page 32 of \cite{ned:geu:vri:94}
is called AUT-$\Delta\Lambda$.
This system is defined in \cite{bru:87:1}, where it is just called $\Delta\Lambda$.
In \cite{gro:93} the system is called $\Lambda\Delta$.
In the AUT-$\Delta\Lambda$ system a text is just one big $\lambda$-term.
For this reason an earlier version of this system was called `Automath
single line' or AUT-SL.
An AUT-$\Delta\Lambda$ term is built from only
four primitives:
\begin{enumerate}
\item
\emph{The type of types.}
In \cite{bru:87:1} this is written as $\tau$.
In the proof objects printed by \texttt{aut}, it is printed as \texttt{*}
if it corresponds to \texttt{TYPE} and \texttt{+} if it corresponds
to \texttt{PROP}.
\item\label{bound}
\emph{Bound variables.}
These are represented by de Bruijn indices.
Both the paper which introduced the de Bruijn indices \cite{bru:72}
and the AUT-$\Delta\Lambda$ paper \cite{bru:87:1} count them from 1,
but the \texttt{aut} checker counts them from 0.
Also, the \texttt{aut} checker represents the number 0 by the empty string.
As an example, the term $\lambda A^* a^A. A$ is written $[\tau]\,[1]\,2$ in \cite{bru:87:1}
and is printed \texttt{[*][]1} by \texttt{aut}.
\item
\emph{$\lambda$-abstraction.}
The term $\lambda x{:}A.B$ is written $[A]\,B$ in \cite{bru:87:1}.
It is printed \texttt{[}$A$\texttt{]}$B$ by \texttt{aut}.
\item
\emph{Function application.}\label{apporder}
The term $fa$ is written $\langle a \rangle\,f$ in \cite{bru:87:1}.
It is printed \texttt{<}$a$\texttt{>}$f$ by \texttt{aut}, unless it
has been derived from the \texttt{:=} in an abbreviation line, in which
case it is printed \texttt{(}$a$\texttt{)}$f$.
This means that
to the Automath input line \texttt{x} \texttt{:=} \texttt{t} \texttt{;} \texttt{A}
corresponds a substring \texttt{(t)[A]} in the AUT-$\Delta\Lambda$ term.
\end{enumerate}
To illustrate the smallness of the number four:
the basic datatype \texttt{exp} of the \texttt{aut} checker has seven constructors,
the basic datatypes \texttt{typ} and \texttt{term} of the Isabelle/Pure logical framework together have nine constructors,
and the basic datatype \texttt{constr} of the Coq
system has sixteen constructors.
\subsection{Example}
The AUT-$\Delta\Lambda$ translation of an \texttt{aut} text
only makes sense if the text is
written in AUT-QE without type inclusion.
This is the language that \texttt{aut} checks with the \texttt{-a}
flag.
Here is an example of a text that already is accepted by \texttt{aut}
without any flags.
It is in the intersection of AUT-68 and AUT-QE:
\begin{verbatim}
+minimal
* Prop := PN ; TYPE
* p := --- ; Prop
p * q := --- ; Prop
q * imp := PN ; Prop
\end{verbatim}
\begin{verbatim}
+intuitionistic
* con := PN ; Prop
p * not := imp(con) ; Prop
-intuitionistic
\end{verbatim}
\begin{verbatim}
p * Proof := PN ; TYPE
q * _q := --- ; [_p,Proof(p)]Proof(q)
_q * imp_intro := PN ; Proof(imp)
q * _p := --- ; Proof(p)
_p * _imp := --- ; Proof(imp)
_imp * imp_elim := PN ; Proof(q)
\end{verbatim}
\begin{verbatim}
+*intuitionistic
+classical
p * _nn := --- ; Proof(not(not))
_nn * notnot_elim := PN ; Proof
-classical
\end{verbatim}
\begin{verbatim}
p * _con := --- ; Proof(con)
_con * con_elim := notnot_elim"-classical"(imp_intro
(not,con,[_not,Proof(not)]_con))
; Proof
-intuitionistic
-minimal
\end{verbatim}
And here is the proof object that \texttt{aut} prints for this text:
\begin{verbatim}
[*][[][1]2][1]([2]<1><>2)[[2]3][[3]*][[4][5][[<1>2]<1>3]<<
1><2>6>3][[5][6][<1>3][<<1><2>7>4]<2>5][[6][<<<>4>4>3]<1>4
]([7][<6>4]<<[<<1>6>5]1><7><<1>6>4><1>2)[[7][<6>4]<1>5]
\end{verbatim}
Written in conventional $\lambda$-notation this is the term:
$$\begin{array}{l}
\lambda P^{*}\,
i^{\lambda p^{P} q^{P}.P}\,
c^{P}.
(\lambda n^{\lambda p^{P}.P}\,
R^{\lambda p^{P}.*}\,
I^{\lambda p^{P} q^{P} \hat{q}^{\lambda \hat{p}^{Rp}.Rq}.R(ipq)}\\
E^{\lambda p^{P} q^{P} \hat{p}^{Rp} \hat{\imath}^{R(ipq)}.Rq}\,
D^{\lambda p^{P} \hat{n}^{R(n(np))}.Rp}.
(\lambda C^{\lambda p^{P} \hat{c}^{Rc}.Rp}.C)\\
(\lambda p^{P} \hat{c}^{Rc}.Dp(I(np)c(\lambda \hat{n}^{R(np)}.\hat{c}))))
(\lambda p^{P}.ipc)
\end{array}$$
Note that in this term the type $P\to P\to P$ of the implication $i$ is
$\lambda p^P q^P.P$ instead of $\Pi p^P q^P.P$.
%And here is the proof object again, but split into lines
%corresponding to the lines of the original text and
%with labels added that correspond to the variables in the $\lambda$-term:
%\begin{flushleft}
%\texttt{[P:*]}\\
%\texttt{[i:[p:][q:1]2]}\\
%\texttt{[c:1]}\\
%\texttt{([p:2]<1><>2)[n:[p:2]3]}\\
%\texttt{[R:[p:3]*]}\\
%\texttt{[I:[p:4][q:5][\^q:[\^p:<1>2]<1>3]<<1><2>6>3]}\\
%\texttt{[E:[p:5][q:6][\^p:<1>3][\^\i:<<1><2>7>4]<2>5]}\\
%\texttt{[D:[p:6][\^n:<<<>4>4>3]<1>4]}\\
%\texttt{([p:7][\^c:<6>4]<<[\^n:<<1>6>5]1><7><<1>6>4><1>2)[C:[p:7][\^c:<6>4]<1>5]}$\hspace{-2cm}$
%\end{flushleft}
\subsection{The proof object of the Grundlagen}
The proof object that \texttt{aut} prints for
an Automath text that uses type inclusion,
is not correct as an AUT-$\Delta\Lambda$ term.
Although there is no system `AUT-$\Delta\Lambda$-QE' in the literature,
\texttt{aut} can still print the proof object.
Here is the proof object for \texttt{grundlagen.aut}:
\begin{verbatim}
([+][+][1]1)[[+][+]+]([+][+][1][<1><2>3]<1>)[[+][+][1][<1>
<2>3]2]([+][])[[+]<><>2]([+][+][+][<1><2>5][<1><2>6][4]<<>
2>1)[[+][+][+][<1><2>5][<1><2>6]<2><4>7][+]([+]<1><>5)[[+]
+]([+]<<>1>1)[[+]+]([+][][<1>3]<1>)[[+][]<1>2][[+][<>2]1](
\end{verbatim}
\vspace{-\medskipamount}\vspace{-\smallskipamount}
\hfill\emph{{\rm 1.8M} of proof term taking {\rm 32722} lines omitted}\hfill
\vspace{-\medskipamount}
\begin{verbatim}
><<3>92>1976>2000]<<1><2>1991><<<><1><2><3><4>6><<1><2>199
6><<3><4>1996>1986><<3><4>1990><1><<<1><2>1996>1994><<<3><
4>1996>1994><3><2965>6711)[[2960][2961][2962][2963][<<<24>
<<>92>1904><<1>92>1976><<<24><<2>92>1904><<3>92>1976>2000]
<1><3>2964]
\end{verbatim}
This $\lambda$-term contains 2917 $\tau$-types,
96528 $\lambda$-abstractions,
406023 function applications, and
499635 bound variables.
\subsection{Checking AUT-QE using Coq?}\label{qe-pts}
The $\lambda$-terms of AUT-QE cannot be checked by a
modern system like Coq, Agda or Lego.
Consider the following correct AUT-QE text:
\begin{verbatim}
* nat := PN ; TYPE
* 0 := PN ; nat
* seq := [n:nat]nat ; [n:nat]TYPE
* nat0 := <0>seq ; TYPE
* id := [n:nat]n ; seq
\end{verbatim}
In this example, the type \texttt{seq} represents $\mathbb{N}\to\mathbb{N}$,
the infinite sequences of natural numbers.
The type \texttt{nat0} is the type of the initial element of such a sequence
(and it is convertible with \texttt{nat}).
The function \texttt{id} is the sequence corresponding to the
identity function: $0,1,2,\ldots$
In Automath the $\lambda$- and $\Pi$-binders have been merged,
but in a pure type system they have to be distinguished.
It is not possible to choose between a $\lambda$- or $\Pi$-binder
for the binder in \texttt{[n:nat]nat} in such a way that the resulting
text will be correct in a modern system.
It has to be a $\lambda$
to make the typing \texttt{[n:nat]nat} : \texttt{[n:nat]TYPE} legal,
and also to make the expression \texttt{<0>seq} correct, but it has to be
a $\Pi$ to make the typing \texttt{[n:nat]n} : \texttt{seq} legal.
%This means that there is no way to choose for each binder in this text
%between a $\lambda$- or $\Pi$-binder,
%in such a way that the typings will be correct in a proper type system.
In the AUT-QE language types are not unique because of the feature
of type inclusion.
The type of \texttt{seq}, \texttt{[n:nat]TYPE}, is
included in the type \texttt{TYPE}.
Therefore \texttt{seq} can both be used in a context that needs type
\texttt{[n:nat]TYPE}, as well as in a context that needs type \texttt{TYPE}.
In a singly sorted (or `functional') proper type system types are unique (up to convertibility),
and there is nothing corresponding to type inclusion.
The problem with the example is not related to type inclusion.
It is also present in AUT-$\Delta\Lambda$,
a system that does not have type inclusion.
The proof object of the example is:
\begin{center}
\texttt{[*][]([1]2)[[1]*](<1>)[*]([3])[1]}
\end{center}
or in conventional $\lambda$-notation:
$$\lambda N^* z^N.(\lambda S^{\lambda n^N.*}. (\lambda M^*. (\lambda i^S.i) (\lambda n^N. n)) (S z)) (\lambda n^N. N)$$
This is a correct AUT-$\Delta\Lambda$ term.
But again, there is no way
to change some of the $\lambda$s in this term to $\Pi$s
in such a way that it becomes correct in a pure type system.
The type of $S$ can not be a sort,
so $S$ should not occur as a type, but it does, as the type of $i$.
In Examples 5.2.4 of \cite{bar:92} a singly sorted pure type system
called $\lambda$AUT-QE is defined,
taken from \cite{jut:90}.
It has the following specification:
\begin{center}
\begin{tabular}{ll}
$\cal{S}$ & $*,\Box,\Delta$\\
$\cal{A}$ & $*:\Box$ \\
$\cal{R}$ & $(*,*,*), (*,\Box,\Box), (\Box,*,\Delta),
(\Box,\Box,\Delta), (*,\Delta,\Delta), (\Box,\Delta,\Delta)$
\end{tabular}
\end{center}
This system encodes the distinction between the two kinds of
function application of AUT-QE,
but it does not solve the problem of the disambiguation of $\lambda$s
into $\lambda$s and $\Pi$s,
and it does not solve the problem of how to deal with Automath's type inclusion
in a pure type system.
It might be possible to generate Coq, Agda or Lego versions
of an AUT-QE text (like the Grundlagen translation), but it is not a mere matter
of syntax.
For this reason, the \texttt{aut} program does not have a feature to
print its $\lambda$-terms in the syntax of one of those systems.
If an approach is developed to generate modern style $\lambda$-terms
from an AUT-QE text, an implementation of such an approach can start from the
proof object that \texttt{aut} prints.
\section{Conclusion}
\subsection{Possible future extensions}
Here are some possible extensions of the \texttt{aut} checker.
They are the features that are currently missing.
We have no specific plans to implement these
in the near future.
\begin{itemize}
\item \emph{Telescopes and segments.}
Automath can be extended with \emph{telescopes}, which are
variables for lists of $\lambda$-binders.
This extension of the Automath language is described in \cite{bru:91}.
A generalization of telescopes is called \emph{segments} \cite{bal:86}.
The \texttt{aut} checker currently does not implement telescopes or segments.
It is not immediately
clear how to implement them in the term graph representation
that is used by \texttt{aut}.
\item AUT-SYNT, AUT-$\Pi$.
There are dialects of the Automath language that have never been
implemented.
In Appendix 9 of \cite{jut:79}, reproduced as (B.5) in \cite{ned:geu:vri:94},
the AUT-SYNT language is described.
In this language parts of terms are synthesized automatically
by the system.
In Chapter VIII of \cite{daa:80}, reproduced as (B.6) in \cite{ned:geu:vri:94},
the AUT-$\Pi$ language is described.
This is an extension of AUT-SYNT that has telescopes and
$\Pi$- and $\Sigma$-types.
The \texttt{aut} system is currently not able to check these languages.
\end{itemize}
\subsection{Lessons for modern systems}\label{lessons}
We do not try to advocate an Automath revival.
Automath is very elegant, but it is too basic for the formalization of large
scale mathematics.
However, our experience with \texttt{aut} pointed out some things that
might be
noted by modern systems:
\begin{itemize}
\item \emph{Proof checkers can be fast.}
\texttt{aut} can check the translation of a full book in under a second.
The modern systems cannot even come close to that.
The reason for this is that the modern systems not only check the proof,
but also do a lot of work for the user constructing the proof.
Obviously they should: the user's time is much more valuable than the
computer's time.
However, it is desirable to be able to recheck proofs with the speed of
\texttt{aut} after they have been processed a first time.
Most modern systems construct all proofs from scratch
every time they recheck a text.
We advocate investigating the notion of \emph{proof caching}.
After a system has constructed a proof it should be kept,
and during a next check it then already will be available and
can be checked fast.
\item \emph{{\rm AUT-$\Delta\Lambda$} is an interesting logical framework.}
The Grundlagen translation uses classical logic, but N.G. de Bruijn
claims that Automath is a \emph{restaurant}.
Just as in a restaurant one can order different kinds of food, one can
use Automath to define different logics.
In modern terminology this means that
he proposes to use Automath as a \emph{logical
framework} \cite{pfe:96}.
Of the modern systems for formalizing mathematics,
the Isabelle system \cite{pau:94,nip:pau:wen:02}
is the primary one that is based on a logical framework.
It consists of the logical framework called Isabelle/Pure, and
on top of this a higher order logic is defined called Isabelle/HOL.
Also first order
logic with ZFC set theory is available as Isabelle/ZF.
AUT-$\Delta\Lambda$ is the ultimate logical framework.
It has not had the attention that it deserves.
The two main reasons for this are:
\begin{itemize}
\item
The type theory of AUT-$\Delta\Lambda$ is $\lambda$-typed,
while the current type theories are $\Pi$-typed.
Because of this, AUT-$\Delta\Lambda$ has no naive set theoretic model
and therefore
is considered to be `just syntax' and to have `no meaning'.
\item
The theory of LF as a logical framework
is well developed, but the corresponding theory of AUT-$\Delta\Lambda$ is not.
In \cite{har:hon:plo:91} it has been proved that the proofs
that one can do with first order logic encoded in LF correspond exactly
to the proofs of first order logic itself.
A similar result for AUT-$\Delta\Lambda$ has never been proved.
\end{itemize}
We claim that it is worthwhile to investigate models of AUT-$\Delta\Lambda$
and to develop the theory for AUT-$\Delta\Lambda$ corresponding to
\cite{har:hon:plo:91}.
\end{itemize}
%\bibliographystyle{klunamed}
%\bibliography{frk}
\begin{thebibliography}{}
\bibitem[\protect\citeauthoryear{Balsters}{1986}]{bal:86}
Balsters, H.: 1986, `{Lambda calculus extended with segments}'.
\newblock Ph.D. thesis, Eindhoven University of Technology.
\bibitem[\protect\citeauthoryear{Barendregt}{1992}]{bar:92}
Barendregt, H.: 1992, `{Lambda calculi with types}'.
\newblock In: S. Abramsky, D. Gabbay, and T. Maibaum (eds.): {\em Handbook of
Logic in Computer Science}, Vol.~II.
\newblock Oxford University Press, pp. 117--309.
\bibitem[\protect\citeauthoryear{de~Bruijn}{1972}]{bru:72}
de~Bruijn, N.: 1972, `Lambda calculus notation with nameless dummies, a tool
for automatic formula manipulation, with application to the Church-Rosser
theorem'.
\newblock {\em Indigationes Math.} {\bf 34}, 381--392.
\newblock (C.2) in \cite{ned:geu:vri:94}.
\bibitem[\protect\citeauthoryear{de~Bruijn}{1987}]{bru:87:1}
de~Bruijn, N.: 1987, `{Generalizing Automath by means of a lambda-typed lambda
calculus}'.
\newblock In: D. Kueker, E. Lopez-Escobar, and C. Smith (eds.): {\em
Mathematical Logic and Theoretical Computer Science}, Vol. 106 of {\em
Lecture Notes in Pure and Appl.~Math.} New York, pp. 71--92, Marcel Dekker.
\newblock (B.7) in \cite{ned:geu:vri:94}.
\bibitem[\protect\citeauthoryear{de~Bruijn}{1991}]{bru:91}
de~Bruijn, N.: 1991, `{Telescopic mappings in typed lambda calculus}'.
\newblock {\em Information and Computation} {\bf 91}, 189--204.
\bibitem[\protect\citeauthoryear{de~Groote}{1993}]{gro:93}
de~Groote, P.: 1993, `Defining $\lambda$-Typed $\lambda$-Calculi by
Axiomatizing the Typing Relation'.
\newblock Technical Report CRIN 93-R-003, Centre de Recherche en Informatique
de Nancy.
\bibitem[\protect\citeauthoryear{Gordon et~al.}{1979}]{gor:mil:wad:79}
Gordon, M., R. Milner, and C. Wadsworth: 1979, {\em Edinburgh LCF: A Mechanised
Logic of Computation}, Vol.~78 of {\em LNCS}.
\newblock Berlin, Heidelberg, New York: Springer Verlag.
\bibitem[\protect\citeauthoryear{Harper et~al.}{1991}]{har:hon:plo:91}
Harper, R., F. Honsell, and G. Plotkin: 1991, `{A Framework for Defining
Logics}'.
\newblock Technical Report ECS-LFCS-91-162, Laboratory for Foundations of
Computer Science, Department of Computer Science, The University of
Edinburgh.
\bibitem[\protect\citeauthoryear{Kamareddine et~al.}{1999}]{kam:blo:ned:99}
Kamareddine, F., R. Bloo, and R. Nederpelt: 1999, `{On $\Pi$-conversion in the
$\lambda$-cube and the combination with abbreviations}'.
\newblock {\em Annals of Pure and Applied Logic} {\bf 97}, 27--45.
\bibitem[\protect\citeauthoryear{Kamareddine and Nederpelt}{1996}]{kam:ned:96}
Kamareddine, F. and R. Nederpelt: 1996, `{Canonical typing and $\Pi$-conversion
in the Barendregt Cube}'.
\newblock {\em J.~Functional Programming} {\bf 6}, 245--267.
\bibitem[\protect\citeauthoryear{Landau}{1965}]{lan:30}
Landau, E.: 1965, {\em Grundlagen der Analysis}.
\newblock New York: Chelsea Publishing Company, fourth edition.
\newblock First edition 1930.
\bibitem[\protect\citeauthoryear{Megill}{1997}]{meg:97}
Megill, N.~D.: 1997, `{Metamath, A Computer Language for Pure Mathematics}'.
\newblock \url{}.
\bibitem[\protect\citeauthoryear{Nederpelt et~al.}{1994}]{ned:geu:vri:94}
Nederpelt, R., J. Geuvers, and R. de~Vrijer: 1994, {\em Selected Papers on
Automath}, Vol. 133 of {\em Studies in Logic and the Foundations of
Mathematics}.
\newblock Amsterdam: Elsevier Science.
\bibitem[\protect\citeauthoryear{Nipkow et~al.}{2002}]{nip:pau:wen:02}
Nipkow, T., L. Paulson, and M. Wenzel: 2002, {\em Isabelle/HOL --- A Proof
Assistant for Higher-Order Logic}, Vol. 2283 of {\em LNCS}.
\newblock Springer.
\bibitem[\protect\citeauthoryear{Paulson}{1994}]{pau:94}
Paulson, L.: 1994, {\em Isabelle: a generic theorem prover}, Vol. 828 of {\em
LNCS}.
\newblock New York: Springer-Verlag.
\bibitem[\protect\citeauthoryear{Pfenning}{1996}]{pfe:96}
Pfenning, F.: 1996, `The Practice of Logical Frameworks'.
\newblock In: H. Kirchner (ed.): {\em Proceedings of the Colloquium on Trees in
Algebra and Programming}. Link{\"o}ping, Sweden, pp. 119--134,
Springer-Verlag LNCS 1059.
\newblock \url{}.
\bibitem[\protect\citeauthoryear{{The Coq Development Team}}{2002}]{coq:02}
{The Coq Development Team}: 2002, `The Coq Proof Assistant Reference Manual'.
\newblock
\url{}.
\bibitem[\protect\citeauthoryear{van Benthem~Jutting}{1976}]{jut:76}
van Benthem~Jutting, L.: 1976, `{A translation of Landau's ``Grundlagen'' in
AUTOMATH}'.
\newblock Technical report, Eindhoven University of Technology.
\bibitem[\protect\citeauthoryear{van Benthem~Jutting}{1979}]{jut:79}
van Benthem~Jutting, L.: 1979, {\em {Checking Landau's ``Grundlagen'' in the
Automath system}}, No.~83 in Mathematical Centre Tracts.
\newblock Amsterdam: Mathematisch Centrum.
\bibitem[\protect\citeauthoryear{van Benthem~Jutting}{1990}]{jut:90}
van Benthem~Jutting, L.: 1990, `{Typing in Pure Type Systems}'.
\newblock Technical report, Dept.~Computer Science, University of Nijmegen,
Nijmegen.
\bibitem[\protect\citeauthoryear{van Daalen}{1973}]{daa:73}
van Daalen, D.: 1973, `{A description of Automath and some aspects of its
language theory}'.
\newblock In: P. Braffort (ed.): {\em {Proceedings of the Symposium APLASM}},
Vol.~1. Orsay.
\newblock (A.3) in \cite{ned:geu:vri:94}.
\bibitem[\protect\citeauthoryear{van Daalen}{1980}]{daa:80}
van Daalen, D.: 1980, `The language theory of Automath'.
\newblock Ph.D. thesis, Eindhoven University of Technology.
\bibitem[\protect\citeauthoryear{Wiedijk}{2000}]{wie:00}
Wiedijk, F.: 2000, `{The De Bruijn Factor}'.
\newblock \url{}.
\bibitem[\protect\citeauthoryear{Wiedijk}{2002}]{wie:02:1}
Wiedijk, F.: 2002, `{The Fifteen Provers of the World}'.
\newblock \url{}.
\bibitem[\protect\citeauthoryear{Zandleven}{1973}]{zan:73}
Zandleven, I.: 1973, `{A verifying program for Automath}'.
\newblock In: P. Braffort (ed.): {\em Proceedings of the Symposium APLASM},
Vol.~I. Orsay.
\newblock (E.1) in \cite{ned:geu:vri:94}.
\end{thebibliography}
\end{document}