\documentclass[runningheads]{llncs}
\usepackage{amssymb,url}
\raggedbottom

\begin{document}

\title{A proposed syntax for binders in Mizar}
\author{Freek Wiedijk}
\institute{University of Nijmegen}
\maketitle

\begin{abstract}
Binders like `$\lim$' (for limits), `$\sum$' (for summation) and `$\int$' (for integration)
are an essential part of the language of mathematics.
They are the `higher order' elements of mathematical expressions.

At the TYPES meeting of 2003 in Turin,
Andrzej Trybulec told me that the reason that Mizar did not have
binders was that nobody had proposed a good syntax for them yet.
To take this reason away, we will present a syntax for binders in Mizar.
\end{abstract}

\section{Introduction}

\subsection{Problem}

One of the main difficulties when trying to `sell' the mathematical
language of the Mizar system \cite{muz:93,wie:99:1} to real mathematicians is its lack of binders.
Consider for instance the formula\footnote{
In this example $\int$ is an indefinite integral that is not very subtle
(it can be taken to be an abbreviation of $\int_0^x$),
because there is no constant of integration.
A more intelligent formal version of indefinite integration is certainly possible.}:
$$\int x^n \,dx = {x^{n + 1}\over n + 1}$$
In the current Mizar language this has to be rendered like:
\begin{verse}\tt
for f st for x holds f.x = x to\char`\_power n holds \\
\ (integral f).x = (x to\char`\_power (n + 1))/(n + 1)
\end{verse}
instead of as the more concise and readable:
\begin{verse}\tt
(integral x of x to\char`\_power n).x = (x to\char`\_power (n + 1))/(n + 1)$\hspace{-1em}$
\end{verse}
Clearly adding binders to the Mizar language will improve it.
Therefore we will propose a notation for binders,
in the hope that some day it will be implemented.

At the TYPES meeting of 2003 I showed a rough version of this proposal to
Andrzej Trybulec and Czeslaw Bylinski.
This note is a worked out version of the same concept.

\subsection{Approach}

We will look for a notation that fits the current style of the Mizar language.
For instance keywords will be preferred over symbols.
Therefore a notation like:
\begin{center}
\verb|\x. x^2 + 1|
\end{center}
(the way $\lambda$-terms are written in the HOL Light system \cite{har:00}) will not be considered to be as `Mizar like' as:
\begin{center}
\verb|lambda x of x^2 + 1|
\end{center}
Another goal will be that the binders will behave similarly
to the first order Mizar operators (`functors')
with respect to overloading and implicit arguments.

\subsection{Related Work}

Most proof assistants for mathematics are based on a higher order logic.
This means that they have $\lambda$-abstraction as a fundamental building block,
and therefore binders are natural for them.
In this respect Mizar is uncommon.

In higher order systems binders often are represented by a functional applied
to a $\lambda$-term.
A binder ${\cal B}$ will thus be represented like:
$${\cal B}(\lambda x.\,f(x))$$
instead of it having `first class' status:
$${\cal B} x.\,f(x)$$
Sometimes the fact that binders are functionals applied to
$\lambda$-terms is hidden with syntactic sugar.
For instance in HOL Light, after one says
\verb|parse_as_binder| \verb|"integral"| %;;
the term:
\begin{center}
\verb|(integral) (\x. x^2 + 1)|
\end{center}
will be pretty-printed by the system as:
\begin{center}
\verb|integral x. x^2 + 1|
\end{center}
and it also can (and generally will) be entered into the system like this.
However, internally it still has the structure of the first term.

An example of a binder that
in a type theoretical system
is not defined with the aid of the $\lambda$-binder
is the product type ${\rm \Pi} x.\, A(x)$.

In our proposed Mizar notation \emph{all} binders will be first class objects.
The \texttt{lambda} binder that we will show in Section \ref{section:lambda}
will have no special status among the other examples.

\subsection{Contribution}

This note shows how binders can be added to the Mizar system in a natural way.

\subsection{Outline}

In Section \ref{section:syntax} we will present our proposed syntax for Mizar binders in an abstract way.
In Sections \ref{section:sums}, \ref{section:lambda} and \ref{section:other} we will illustrate our proposal through examples.
Finally in Section \ref{section:conclusion} we will discuss.

\section{Syntax}\label{section:syntax}

The syntax that we propose for Mizar binders is\footnote{
We underline all binders
to make the structure of these examples clearer,
but these underlinings do not represent anything special in the {\small ASCII}
of the Mizar file.
Look at Section \ref{section:other} for examples written
in a plain typewriter font.
}:
\def\keyword#1{\textsf{\textbf{#1}}}
\begin{center}
\emph{\underbar{binder}} \emph{x} [ \keyword{where} \emph{x} \keyword{is} \emph{type} ] \keyword{at} \emph{args} \keyword{of} \emph{body}
\end{center}
The way a binder will be defined is:
\begin{verse}
\keyword{definition}
 \keyword{let} \emph{args}; 
 [ \keyword{assume} \emph{conditions}; ] \\
\ \keyword{binder} $\{$ \emph{f}($\mbox{\emph{type}}_1$) $\to$ $\mbox{\emph{type}}_2$ $\}$ \\
\ \ \emph{\underbar{binder}} \emph{x} [ \keyword{where} \emph{x} \keyword{is} $\mbox{\emph{type}}_1$ ] \keyword{at} \emph{args} \keyword{of} $f(x)$ $\to$ $\mbox{\emph{type}}_3$ \\
\ \quad \keyword{means} {\dots}; \\
\ \dots \\
\keyword{end}
\end{verse}
(In such a definition the `\keyword{where} \keyword{is}' clause is always redundant,
because $\mbox{\emph{type}}_1$ is also present in the typing of the $f$.
However we allow it for orthogonality.)

To be able to introduce binder symbols, we also will need a new category in the vocabularies.
We propose to use the letter `\texttt{B}' for this.

Note that the binder notation uses the keywords
\keyword{at}, \keyword{of} and \keyword{binder},
together with the keywords
\keyword{where} and \keyword{is}
that are also used in the Fr\"{a}nkel operator (the Mizar notation for
set comprehension).


\section{Finite sums}\label{section:sums}

As an example of what our proposed notation looks like in practice,
take the following equation:
$$\sum_{i = 1}^n i = {n (n + 1)\over 2}$$
It becomes:
\begin{center}
\textsf{\underbar{sum} i \textbf{at} 1,n \textbf{of} i = n$*$(n + 1)/2;}
\end{center}

\medskip\noindent
To be able to write this formula, we need a vocabulary
that contains the following lines\footnote{
The symbol \textsf{sum$'$} is the operator
that in the MML is defined in {\small\texttt{RVSUM}}\texttt{\char`\_1:def} \texttt{10}.
It is the functor that sums a finite sequence of complex numbers.
The symbol \underbar{\textsf{sum}} is the binder that we define from it.
}:
\begin{verse}
\texttt{O}$\,$\textsf{sum$'$} \\
\texttt{B}$\,$\underbar{\textsf{sum}}
\end{verse}
Here is a way that the binder \underbar{\textsf{sum}} might then be defined:
\begin{verse}\sf
\textbf{reserve} i,n,a,b \textbf{for} natural number;
\end{verse}
\begin{verse}\sf
\textbf{definition} 
 \textbf{let} n; \\
\ \textbf{binder} $\{$ f(natural number) $\to$ complex number $\}$ \\
\ \ \underbar{sum} i \textbf{at} n \textbf{of} f(i) $\to$ complex number \\
\ \textbf{means} \\
\ \ \textbf{ex} f' \textbf{being} FinSequence \textbf{of} {\small COMPLEX} \textbf{st} len f' = n \char`\& \\
\ \ \ (\textbf{for} i \textbf{st} i $<$ n \textbf{holds} f'.(i + 1) = f(i)) \char`\&\ \textbf{it} = sum$'$ f'; \\
\ \textbf{existence} \dots; \\
\ \textbf{uniqueness} \dots; \\
\textbf{end};
\end{verse}
\begin{verse}\sf
\textbf{definition} 
 \textbf{let} a,b; \\
\ \textbf{binder} $\{$ f(natural number) $\to$ complex number $\}$ \\
\ \ \underbar{sum} i \textbf{at} a,b \textbf{of} f(i) $\to$ complex number \\
\ \textbf{equals} \\
\ \ (\underbar{sum} i \textbf{at} b + 1 \textbf{of} f(i)) $-$ (\underbar{sum} i \textbf{at} a \textbf{of} f(i)); \\
\ \textbf{coherence} \dots; \\
\textbf{end};
\end{verse}
Note that `\underbar{\textsf{sum}} \textsf{i} \keyword{at} \textsf{n}' means $\sum_{i < n}$,
while `\underbar{\textsf{sum}} \textsf{i} \keyword{at} \textsf{a,b}' means $\sum_{i = a}^b$.


\section{$\lambda$-abstraction}\label{section:lambda}

The most elementary binder is $\lambda$-abstraction
(although it is not the most important one:
$\lim$, $\sum$ and $\int$ are more important for real mathematics).
As an example $\lambda$-abstraction is also interesting because it shows how implicit arguments behave with binders.

The $\lambda$-term:
$$\lambda x.\, x^2 + 1$$
is written:
\begin{center}
\textsf{\underbar{lambda} x \textbf{of} x\^{}2 + 1}
\end{center}
%Of course it denotes the function $f$ with $f(x) = x^2 + 1$.
%
Here is a possible definition of the \underbar{\textsf{lambda}} binder:
\begin{verse}\sf
\textbf{reserve} A,B \textbf{for} non empty set; \\
\textbf{reserve} x \textbf{for} Element \textbf{of} A;
\end{verse}
\begin{verse}\sf
\textbf{definition} 
 \textbf{let} A,B; \\
\ \textbf{binder} $\{$ f(Element \textbf{of} A) $\to$ Element \textbf{of} B $\}$ \\
\ \ \underbar{lambda} x \textbf{of} f(x) $\to$ Function \textbf{of} A,B \\
\ \textbf{means} \\
\ \ \textbf{for} x \textbf{holds} \textbf{it}.x = f(x) \\
\ \textbf{existence} \dots; \\
\ \textbf{uniqueness} \dots; \\
\textbf{end};
\end{verse}
Note that the arguments \textsf{A} and \textsf{B} to the \underline{\textsf{lambda}} binder are inferred rather than being
given explicitly in the term.

The $\beta$-reduction rule now becomes a scheme\footnote{
The double \keyword{of} in `{\dots} \keyword{of} \textsf{A()} \keyword{of} \textsf{f(x)}' might be a bit confusing.
The first \keyword{of} is part of the type, the second \keyword{of} is part of the binder.
}:
\begin{verse}\sf
\textbf{scheme} beta $\{$ A() $\to$ non empty set, B() $\to$ non empty set, \\
\ \quad f(Element \textbf{of} A()) $\to$ Element \textbf{of} B(), a() $\to$ Element \textbf{of} A() $\}$: \\
\ (\underbar{lambda} x \textbf{where} x \textbf{is} Element \textbf{of} A() \textbf{of} f(x)).a() = f(a()) \\
\dots;
\end{verse}
The `definitional scheme' (the equivalent of a definitional theorem for a binder) of the
the definition of \underbar{\textsf{lambda}} is:
\begin{verse}\sf
\textbf{scheme} lambda\_def $\{$ A() $\to$ non empty set, B() $\to$ non empty set, \\
\ \quad f(Element \textbf{of} A()) $\to$ Element \textbf{of} B() $\}$ : \\
\ \textbf{for} x \textbf{being} Element \textbf{of} A() \textbf{holds} \\
\ \ (\underbar{lambda} x \textbf{where} x \textbf{is} Element \textbf{of} A() \textbf{of} f(x)).x = f(x);
\end{verse}
which of course is already very close to this \textsf{beta} scheme.


\section{Examples}\label{section:other}

We now list some more formulas with their proposed Mizar translation.
The first two are repeats from the previous two sections.
Instead of displaying the Mizar fragments in a nice
pretty printed format like before, we will show them here in a plain typewriter font.

$$\sum_{i=1}^n i = {n(n + 1)\over 2}$$
\begin{verse}\tt
sum i at 1,n of i = n*(n + 1)/2
\end{verse}

$$\lambda x.\,x^2 + 1$$
\begin{verse}\tt
lambda x of x\char`\^2 + 1
\end{verse}

$$f\mbox{ is continuous} \iff \lim_{x\to a} f(x) = f(a)\quad\mbox{for all $a$}$$
\begin{verse}\tt
f is continuous iff for a holds lim x at a of f.x = f.a
\end{verse}

$$\sum_{p\;\rm{prime}}\, {1\over p^2} < {1\over 2}$$
\begin{verse}\tt
sum p at \char`\{\ p : p is prime \char`\}\ of 1/p\char`\^2 < 1/2
\end{verse}

$$\int\!\!\!\int_{x^2 + y^2 \le 1} \sqrt{1 - x^2 + y^2} \;dx\,dy = {2\over 3}\pi$$
\begin{verse}\tt
integral z where z is Element of [:REAL,REAL:] at \\
\quad \char`\{\ [x,y] : x\char`\^2 + y\char`\^2 <= 1 \char`\}\ of sqrt(1 - (z`1)\char`\^2 + (z`2)\char`\^2) \\
= 2/3*pi
\end{verse}

\medskip\noindent
The last two examples are interesting because the expressions
\verb|{| \verb|p| \verb|:| \verb|p| \verb|is| \verb|prime| \verb|}| and
\verb|{| \verb|[x,y]| \verb|:| \verb|x^2| \verb|+| \verb|y^2| \verb|<=| \verb|1| \verb|}| have type \verb|set|.
Therefore these variants of \verb|sum| and \verb|integral| need
a `permissive definition' (they need an assumption) to make sense.\footnote{
Really in the definition of \texttt{integral} one would also like the set \texttt{D} to be \texttt{measurable} and the
function \texttt{f} to be \texttt{integrable}.
}
\begin{verse}
\verb|definition let D be set;| \\
\verb| |\underbar{\texttt{assume D is Subset of NAT}}\verb|;| \\
\verb| binder { f(natural number)->complex number }| \\
\verb|  sum i at D of f(i) means |\dots \\
\verb| |\dots \\
\verb|end|
\end{verse}
and:
\begin{verse}
\verb|definition let D be set;| \\
\verb| |\underbar{\texttt{assume D is Subset of [:REAL,REAL:]}}\verb|;| \\
\verb| binder { f(Element of [:REAL,REAL:])->complex number }| \\
\verb|  integral z at D of f(z) means |\dots \\
\verb| |\dots \\
\verb|end|
\end{verse}


\section{Conclusion}\label{section:conclusion}

\subsection{Discussion}

Binders are higher order objects.
Therefore reasoning about binders in Mizar will consist of the application
of schemes.
It is not clear whether this will be practical.

The style of defining binders that we propose is a mixture of the
style of ordinary (first order) definitions and the style of (higher order) schemes.
This is apparent when comparing the definition of \underline{\textsf{lambda}}
in Section \ref{section:lambda} with its definitional scheme \textsf{lambda\_def}.
%
In the definition itself (which has a mixed style) the sets \textsf{A} and \textsf{B} are introduced in
a first order style `\textsf{\textbf{let} A,B \textbf{be} non empty set}', while in its definitional
scheme (which has a purely higher order style) they are introduced in the higher order style `\textsf{$\{\,$A()$\,\to\,$non empty set, B()$\,\to\,$non empty set$\,\}$}'.
%
It is not clear whether this mixture of first order and higher order
style in the definition of binders will cause trouble
in the implementation.

\subsection{Future work}

Implement binders in the Mizar system.

\paragraph{Acknowledgments.}
Thanks to Andrzej Trybulec and Czeslaw Bylinski for discussing this
proposal with me.

\bibliographystyle{plain}
\bibliography{frk}

\end{document}