\documentclass[oribibl]{llncs}
%\documentstyle[a4]{article}
\oddsidemargin 0.25in
\evensidemargin 0.25in
\textwidth 6.25in
\textheight 8.5in
\topmargin -.25in
\begin{document}
\setlength{\tabcolsep}{0.5em}
\def\thefootnote{\fnsymbol{footnote}}
\title{The De Bruijn Factor}
\author{Freek Wiedijk\\
\email{}}
\institute{Department of Computer Science\\
Nijmegen University\\
P.O.~Box 9010\\
6500 GL\ \ Nijmegen\\
The Netherlands}
\date{}
\maketitle
\begin{abstract}
\noindent
We study de Bruijn's `loss factor' between the size of an ordinary mathematical
exposition and its full formal translation inside a computer.
This factor is determined by a combination of the amount of detail present in
the original text and the
expressivity of the system used to do the formalization.
For three specific examples this
factor turns out to be approximately equal to {\em four.}
\end{abstract}
\section{Loss Factor}
In `A survey of the project Automath' de Bruijn wrote (p.~160 in
section A.5 of \cite{ned:geu:vri:94} which is a reprint from \cite{bru:80}):
\begin{quote}
{\em A very important thing that can be concluded from all writing experiments is
the {\em constancy of the loss factor.} The loss factor expresses what we loose in
shortness when translating very meticulous `ordinary' mathematics into
Automath. This factor may be quite big, something like 10 or 20, but it is
constant: it does not increase if we go further in the book. It would not be
too hard to push the constant factor down by efficient abbreviations.}
\end{quote}
Here%
\footnote{The full Automath, Mizar and {\TeX} files that are discussed
here can be found on the World Wide Web at
the address {\tt }.}
we briefly study this loss factor, which we call the {\em de Bruijn factor.}
When writing a `formal proof' (a proof that is entered in a computer
in full detail in such a way that the computer can check the correctness) there
are basically two approaches:
\begin{itemize}
\item One takes an existing, non-formal, mathematical text and translates
it -- more or less faithfully -- into a computer representation.
\item One `programs' the proof directly into the formal system, without first
creating a `natural language' counterpart.
\end{itemize}
The first method has the advantage that the formalization automatically
will be well documented, and also it generally seems to be easier to translate a pre-existing text
than to think about the proof and about the mechanics of the formalization at the same time.
The de Bruijn factor of course only can be objectively measured for a formalization
of the first kind.
The de Bruijn factor of a formalization depends on two aspects.
On the one hand there is the level of detail in the original, which depends on the `character' of
the text that is being translated. There exist a wide range of mathematical styles,
which each have their own level of precision at which the proofs are elaborated. For instance
there are:
\begin{itemize}
\item Books that give a detailed development of a subject for foundational purposes,
like Whitehead and Russell's {\em Principia Mathematica\/} \cite{whi:rus:10}.
\item Ancient mathematics, like Euclid's {\em Elements} \cite{hea:08}.
\item Textbooks for education.
\item Handbooks about specific mathematical subjects.
\item Papers in computer science that have a strong mathematical flavor.
\item Mathematical research papers.
\end{itemize}
The three cases studied in this note are respectively of the first, fifth and
fourth kinds.
On the other hand there is the system that is being used. Some systems have
more automation and more (as de Bruijn called it) `efficient abbreviations'
than others. So the de Bruijn factor measures how efficient a system is.
One might imagine a `benchmark' for proof assistants consisting of a number
of mathematical texts in various styles to be represented. However, the technology currently
seems not to be well-developed enough to already put together such
a benchmark.
\section{Apparent and Intrinsic De Bruijn Factors}
The size in bytes of the files of a formalization is not a very meaningful measure.
It depends on such matters as
the choice of variable names and the use of whitespace: these factors don't seem to
mean much for the contents of the files. For instance if indentation is
done with tab characters that part of the file will be eight times as
small as when it's done with space characters: but the file will look the
same in both cases. As another example, the {\TeX} macro name `\verb|\Leftrightarrow|'
for the `$\Leftrightarrow$'
symbol uses 15 characters, while an encoding like `\verb|<=>|' uses only 3.
To compensate for these effects it seems natural to `squeeze out' trivial
redundancy by compressing the files before calculating the ratios
of their sizes. In fact, use of the tab character can be seen as a crude way of
compressing long runs of spaces.
We will call the ratio of the uncompressed
file sizes the {\em apparent\/} de Bruijn factor, and that of the
compressed file sizes the {\em intrinsic\/} de Bruijn factor.
If one uses the intrinsic de Bruijn factor, it isn't useful any more to remove
the white space from the computer representation of a proof to get a better
ratio, because this kind of optimization only has a minor effect on the size of
the compressed file.
Surprisingly it turns out that generally both the `natural language' and the `computer'
versions of a proof compress similarly well. This means that the apparent
and intrinsic de Bruijn factors turn out to be approximately the same.
\section{Arithmetic in Automath}
The first example for which we will calculate the de Bruijn factor is
Jutting's classic Automath translation (see section D.2 of \cite{ned:geu:vri:94},
a reprint from \cite{jut:79}) of Landau's {\em Grundlagen
der Analysis\/} \cite{lan:30}, a cute little book about the basic
laws of arithmetic up to the complex numbers.
To give an impression of the text and its translation, here is a small fragment
of a proof (of `Satz 27' on p.~37 of \cite{lan:30}) in the {\em Grundlagen\/}:
\ifx\fr\undefined
\font\teneufm=eufm10 \font\seveneufm=eufm7 \font\fiveeufm=eufm5
\csname newfam\endcsname\eufmfam
\textfont\eufmfam=\teneufm \scriptfont\eufmfam=\seveneufm \scriptscriptfont\eufmfam=\fiveeufm
\def\fr{\fam\eufmfam}
\fi
\begin{quote}
{\em 1 geh\"ort zu $\fr M$ nach Satz 24. Nicht jedes $x$ geh\"ort zu $\fr M$;
denn f\"ur jedes $y$ aus $\fr N$ geh\"ort $y + 1$ nicht zu $\fr M$, wegen
$$y + 1 > y.$$}
\end{quote}
together with its rendering in the AUT-QE dialect of the Automath language:
\begin{verse}
\verb|s@[n:nat]|\\
\verb|t1:=[x:p]satz24a(n):lbprop(1,n)|\\
\verb|s@t2:=[x:nat]t1(x):lb(1)|\\
\verb|[l:[x:nat]lb(x)][y:nat][yp:p]|\\
\verb|t3:=satz18(y,1):more(pl(y,1),y)|\\
\verb|t4:=satz10g(pl(y,1),y,t3):not(lessis(pl(y,1),y))|\\
\verb|t5:=th4"l.imp"(p,lessis(pl(y,1),y),yp,t4):not(lbprop(pl(y,1),y))|\\
\verb|t6:=th1"l.all"(nat,[x:nat]lbprop(pl(y,1),x),y,t5):not(lb(pl(y,1)))|\\
\verb|t7:=mp(lb(pl(y,1)),con,l,t6):con|\\
\verb|l@t8:=someapp(nat,p,s,con,[x:nat][y:p]t7(x,y)):con|
\end{verse}
Note the reference to `Satz 24' at the start of both versions of the fragment.
The sizes of both the {\TeX} and Automath versions of this book,
both uncompressed and compressed (using the Unix {\tt gzip} utility), and the corresponding de Bruijn factors
are given in the following table:
\[
\begin{tabular}{rrrrr}
&informal&formal&{\em de Bruijn factor}&\\
\noalign{\smallskip}
\cline{2-5}
\noalign{\smallskip}
uncompressed&189\,K&736\,K&apparent&3.9\\
compressed&42\,K&155\,K&intrinsic&3.7\\
\noalign{\smallskip}
\cline{2-5}
\end{tabular}
\]
Apparently the de Bruijn factor of Automath for this kind of text is slightly
less than {\em four.}
\section{Computer Science in Mizar}
The second example that we will calculate the de Bruijn factor for, is a section
from a paper about `finite topology' (pp.~12--17 of \cite{nak:fuw:imu:91}), really a mathematical development of
the theory of digital filtering of one-bit images. The translation \cite{imu:egu:92}
is in Mizar, which is a more accessible and more high level system than Automath.
As an example, here's a fragment of the proof of `Theorem 2.1' (p.~16 of \cite{nak:fuw:imu:91}):
\begin{quote}
{\em Let $B$ and $C$ be non-void subsets of $A$ such that $B \cap C = \emptyset$ and $B^b \cap C = \emptyset$.
Then, there exists an element $x$ in $B$, and we can construct a set $P_n$ as a procedure
described previously and $P_{n+1} = P_n$.}
\end{quote}
with as Mizar translation:
\begin{verse}
\verb| given B, C being Subset of the carrier of FT such that|\\
\verb| A26:A = B U C and|\\
\verb| A27:B <> |$\emptyset$\verb| and|\\
\verb| A28:C <> |$\emptyset$\verb| and|\\
\verb| A29:B |$\cap$\verb| C = |$\emptyset$\verb| and|\\
\verb| A30:B^b |$\cap$\verb| C = |$\emptyset$\verb|;|\\
\verb| A31: B c= B^b by Th18 ;|\\
\verb| A32: B^b |$\cap$\verb| A = B^b |$\cap$\verb| B U |$\emptyset$\verb| by A26,A30, BOOLE:70|\\
\verb| .= B^b |$\cap$\verb| B by BOOLE:60|\\
\verb| .= B by BOOLE:42, A31 ;|\\
\verb| consider x being Element of B ;|\\
\verb| x |$\in$\verb| A by A26, BOOLE:def 2,A27 ;|\\
\verb| then consider S being FinSequence of bool the carrier of FT such that|\\
\verb| A33:len S > 0 and|\\
\verb| A34:|$\pi$\verb|(S,1) = {x} and|\\
\verb| A35:for i being Nat st i > 0 & i < len S holds |$\pi$\verb|(S,i+1) = |$\pi$\verb|(S,i)^b |$\cap$\verb| A and|\\
\verb| A36:A c= |$\pi$\verb|(S,len S) by A25 ;|
\end{verse}
Note the close syntactical similarity of the requirements on $B$ and $C$ in both versions of the text.
Here are the statistics of this example:
\[
\begin{tabular}{rrrrr}
&informal&formal&{\em de Bruijn factor}&\\
\noalign{\smallskip}
\cline{2-5}
\noalign{\smallskip}
uncompressed&7.7\,K&35.3\,K&apparent&4.6\\
compressed&2.6\,K&8.0\,K&intrinsic&3.1\\
\noalign{\smallskip}
\cline{2-5}
\end{tabular}
\]
So the de Bruijn factor of this text is not much better than that
of the previous one. An explanation might be that the paper that is translated contains much less
detail than the {\em Grundlagen\/} book, so the extra power of Mizar is compensated for by the more loose style
of the informal article. For instance, a number of
statements at the end are not proved, but instead it is just stated that:
\begin{quote}
{\em The following facts are easily derived.}
\end{quote}
\section{Mathematics in Mizar}
The final example for which we calculate the de Bruijn factor, is part of
an ongoing effort at the Mizar project to translate a complete
mathematical book \cite{gie:hof:kei:law:mis:sco:80} into the Mizar language. For the book
a handbook from mathematical logic was chosen, which presents the theory of
`continuous lattices.' The translation of this
book (which currently is halfway finished) consists of a large number of
Mizar articles with names starting with `\verb|YELLOW|' and `\verb|WAYBEL|'.
The
article that we analyze here \cite{byl:rud:97} is the translation of four pages of the book.
Again we give an example of the style of both the original and the translation.
The statement of `Corollary 1.13' (on p.~106 of \cite{gie:hof:kei:law:mis:sco:80}) is:
\begin{quote}
{\em If $L$ is a continuous lattice, then $(L,\sigma(L))$ is a quasicompact
and locally quasicompact sober space. In particular, $(L,\sigma(L))$ is a Baire space.}
\end{quote}
which gets translated into Mizar as:
\begin{verse}
\verb|L is continuous implies L is compact locally-compact sober Baire|
\end{verse}
Then the proof of this `Corollary' starts with the following reasoning:
\let\ua=\uparrow \def\uparrow{\mathord{\ua}}
\def\doubleuparrow{\lower.8pt\hbox{$\ua$}\raise.8pt\llap{$\ua$}}
\begin{quote}
{\em We have to show that a point $x\in L$ has a basis of quasicompact
neighborhoods. By 1.10 the sets $\doubleuparrow y$ with $y\ll x$ form a basis for the
neighborhoods of the point. But as we know, if $x\in U\in\sigma(L)$, then actually we
have a $y\in U$ with $y\ll x$; hence, $\uparrow y\subseteq U$, and so the sets $\uparrow y$ can be used as
neighborhoods.}
\end{quote}
to which corresponds the following fragment of the Mizar proof:
\begin{verse}
\verb| thus A5: L is locally-compact|\\
\verb| proof let x be Point of L, X be Subset of L such that|\\
\verb|A6: x |$\in$\verb| X and|\\
\verb|A7: X is open;|\\
\verb| reconsider x' = x as Element of L by STRUCT_0:def 2;|\\
\verb| set bas = { wayabove q where q is Element of L: q << x' };|\\
\verb|A8: bas is basis of x by A1, WAYBEL11:44;|\\
\verb| consider y being Element of L such that|\\
\verb|A9: y << x' & y |$\in$\verb| X by A1, A6, A7, WAYBEL11:43;|\\
\verb| X is upper by A7, WAYBEL11:def 4; then|\\
\verb|A10: uparrow y c= X by A9, WAYBEL11:42;|\\
\verb| set Y = uparrow y;|\\
\verb| take Y;|\\
\verb| wayabove y |$\in$\verb| bas by A9; then|\\
\verb|A11: wayabove y is open & x |$\in$\verb| wayabove y by A8, YELLOW_8:21;|\\
\verb| wayabove y c= Y by WAYBEL_3:11; then|\\
\verb| wayabove y c= Int Y by A11, TOPS_1:56;|\\
\verb| hence x |$\in$\verb| Int Y by A11;|\\
\verb| thus Y c= X by A10;|
\end{verse}
Because this book is `more mathematical' and hence reasons at a higher level than the previous
two examples, the de Bruijn factor is a bit higher:
\[
\begin{tabular}{rrrrr}
&informal&formal&{\em de Bruijn factor}&\\
\noalign{\smallskip}
\cline{2-5}
\noalign{\smallskip}
uncompressed&11.7\,K&78.4\,K&apparent&6.7\\
compressed&4.0\,K&16.3\,K&intrinsic&4.1\\
\noalign{\smallskip}
\cline{2-5}
\end{tabular}
\]
\vskip 0pt
\section{The De Bruijn Threshold}
It seems plausible that there is a certain value for the de Bruijn factor
such that, when proof checkers become sufficiently powerful that their factor
drops below it, people will start using them for serious
work (like verifying the correctness of their mathematics and communicating
the precise details of their work to others). We suggest to call this value
the {\em de Bruijn threshold.} Like the de Bruijn factor of a system, it
probably depends on the kind of mathematics.
As it probably is not possible to get a formalization to be as short as
its informal version, it is to be hoped that the de Bruijn threshold of
something interesting won't be less than {\em one.}
%\bibliographystyle{plain}
%\bibliography{factor}
\begin{thebibliography}{10}
\bibitem{bru:80}
N.G.~de Bruijn.
\newblock {A survey of the project Automath}.
\newblock In J.P. Seldin and J.R. Hindley, editors, {\em To H.B. Curry: Essays
on Combinatory Logic, Lambda Calculus and Formalism}, pages 579--606.
Academic Press, New York, London, 1980.
\bibitem{byl:rud:97}
C.~Bylinski and P.~Rudnicki.
\newblock {The Scott topology, Part II}.
\newblock {\em Journal of Formalized Mathematics}, 9, 1997.
\newblock MML Identifier: \verb|WAYBEL14|.
\bibitem{gie:hof:kei:law:mis:sco:80}
G.~Gierz, K.H. Hofmann, K.~Keimel, J.D. Lawson, M.~Mislove, and D.S. Scott.
\newblock {\em A Compendium of Continuous Lattices}.
\newblock Springer-Verlag, Berlin, Heidelberg, New York, 1980.
\bibitem{hea:08}
Sir~Th.L. Heath.
\newblock {\em The Thirteen Books of Euclid's Elements}.
\newblock Dover Publications, New York, dover edition, 1956.
\newblock First edition 1908, second edition 1925.
\bibitem{imu:egu:92}
H.~Imura and M.~Eguchi.
\newblock {Finite Topological Spaces}.
\newblock {\em Journal of Formalized Mathematics}, 4, 1992.
\newblock MML Identifier: \verb|FIN_TOPO|.
\bibitem{jut:79}
L.S. van~Benthem Jutting.
\newblock {\em {Checking Landau's ``Grundlagen'' in the Automath system}}.
\newblock Number~83 in Mathematical Centre Tracts. Mathematisch Centrum,
Amsterdam, 1979.
\bibitem{lan:30}
E.~Landau.
\newblock {\em Grundlagen der Analysis}.
\newblock Chelsea Publishing Company, New York, fourth edition, 1965.
\newblock First edition 1930.
\bibitem{nak:fuw:imu:91}
Y.~Nakamura, Y.~Fuwa, and H.~Imura.
\newblock {A Theory of Finite Topology and Image Processing}.
\newblock {\em Journal of the Faculty of Engineering, Shinshu University},
69:11--24, 1991.
\bibitem{ned:geu:vri:94}
R.P. Nederpelt, J.H. Geuvers, and R.C.~de Vrijer.
\newblock {\em Selected Papers on Automath}, volume 133 of {\em Studies in
Logic and the Foundations of Mathematics}.
\newblock Elsevier Science, Amsterdam, etc., 1994.
\bibitem{whi:rus:10}
A.N. Whitehead and B.~Russell.
\newblock {\em Principia Mathematica}.
\newblock Cambridge University Press, Cambridge, paperback edition, 1962.
\newblock First edition 1910, second edition 1927.
\end{thebibliography}
\end{document}