\newcommand{\ASSIGNEDTO}[1]{\textbf{Assigned to:} #1}
\newcommand{\NOTE}[1]{\marginpar{\scriptsize #1}}
+\newcommand{\NT}[1]{\langle\mathit{#1}\rangle}
\title{The Matita proof assistant}
\author{Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi
\institute{Department of Computer Science, University of Bologna\\
Mura Anteo Zamboni, 7 --- 40127 Bologna, ITALY\\
\email{$\{$asperti,sacerdot,tassi,zacchiro$\}$@cs.unibo.it}}
+\bibliographystyle{plain}
\begin{document}
\maketitle
\section{Introduction}
\label{sec:intro}
{\em Matita} is the proof assistant under development by the \HELM{} team
-\cite{annals} at the University of Bologna, under the direction of
+\cite{mkm-helm} at the University of Bologna, under the direction of
Prof.~Asperti.
The origin of the system goes back to 1999. At the time we were mostly
interested to develop tools and techniques to enhance the accessibility
\HELM{} a MathML-compliant widget for the GTK graphical environment
which can be integrated in any application.
\end{itemize}
-The exportation issue, extensively discussed in \cite{exportation},
+The exportation issue, extensively discussed in \cite{exportation-module},
has several major implications worth to be discussed.
The first
\label{sec:disambiguation}
\ASSIGNEDTO{zack}
-%The disambiguation phase builds CIC terms from ASTs of user inputs (also called
-%\emph{ambiguous terms}). Ambiguous terms may carry three different \emph{sources
-%of ambiguity}: unbound identifiers, literal numbers, and literal symbols.
-%\emph{Unbound identifiers} are sources of ambiguity since the same name
-%could have been used to represent different objects. For example, three
-%different theorems of the \COQ{} library share the name $\mathit{plus\_assoc}$
-%(locating them is an exercise for the interested reader. Hint: use \WHELP's
-%\LOCATE{} query).
-%
-%\emph{Numbers} are ambiguous since several different encodings of them could be
-%provided in logical systems. In the \COQ{} standard library for example we found
-%naturals (in their unary encoding), positives (binary encoding), integers
-%(signed positives), and reals. Finally, \emph{symbols} (instances of the
-%\emph{binop} and \emph{unop} syntactic categories of Table~\ref{tab:syntax}) are
-%ambiguous as well: infix \texttt{+} for example is overloaded to represent
-%addition over the four different kinds of numbers available in the \COQ{}
-%standard library. Note that given a term with more than one sources of
-%ambiguity, not all possible disambiguation choices are valid: for example, given
-%the input \texttt{1+1} we must choose an interpretation of \texttt{+} which is
-%typable in CIC according to the chosen interpretation for \texttt{1}; choosing
-%as \texttt{+} the addition over natural numbers and as \texttt{1} the real
-%number $1$ will lead to a type error.
-%
-%A \emph{disambiguation algorithm} takes as input an ambiguous term and return a
-%fully determined CIC term. The \emph{naive disambiguation algorithm} takes as
-%input an ambiguous term $t$ and proceeds as follows:
-%
-%\begin{enumerate}
-%
-% \item Create disambiguation domains $\{D_i | i\in\mathit{Dom}(t)\}$, where
-% $\mathit{Dom}(t)$ is the set of ambiguity sources of $t$. Each $D_i$ is a set
-% of CIC terms.
-%
-% \item Let $\Phi = \{\phi_i | {i\in\mathit{Dom}(t)},\phi_i\in D_i\}$
-%% such that $\forall i\in\mathit{Dom}(t),\exists\phi_j\in\Phi,i=j$
-% be an interpretation for $t$. Given $t$ and an interpretation $\Phi$, a CIC
-% term is fully determined. Iterate over all possible interpretations of $t$ and
-% type-check them, keep only typable interpretations (i.e. interpretations that
-% determine typable terms).
-%
-% \item Let $n$ be the number of interpretations who survived step 2. If $n=0$
-% signal a type error. If $n=1$ we have found exactly one CIC term
-% corresponding to $t$, returns it as output of the disambiguation phase.
-% If $n>1$ let the user choose one of the $n$ interpretations and returns the
-% corresponding term.
-%
-%\end{enumerate}
-%
-%The above algorithm is highly inefficient since the number of possible
-%interpretations $\Phi$ grows exponentially with the number of ambiguity sources.
-%The actual algorithm used in \WHELP{} is far more efficient being, in the
-%average case, linear in the number of ambiguity sources.
-%
-%The efficient algorithm can be applied if the logic can be extended with
-%metavariables and a refiner can be implemented. This is the case for CIC and
-%several other logics.
-%\emph{Metavariables}~\cite{munoz} are typed, non linear placeholders that can
-%occur in terms; $?_i$ usually denotes the $i$-th metavariable, while $?$ denotes
-%a freshly created metavariable. A \emph{refiner}~\cite{mcbride} is a
-%function whose input is a term with placeholders and whose output is either a
-%new term obtained instantiating some placeholder or $\epsilon$, meaning that no
-%well typed instantiation could be found for the placeholders occurring in
-%the term (type error).
-%
-%The efficient algorithm starts with an interpretation $\Phi_0 = \{\phi_i |
-%\phi_i = ?, i\in\mathit{Dom}(t)\}$,
-%which associates a fresh metavariable to each
-%source of ambiguity. Then it iterates refining the current CIC term (i.e. the
-%term obtained interpreting $t$ with $\Phi_i$). If the refinement succeeds the
-%next interpretation $\Phi_{i+1}$ will be created \emph{making a choice}, that is
-%replacing a placeholder with one of the possible choice from the corresponding
-%disambiguation domain. The placeholder to be replaced is chosen following a
-%preorder visit of the ambiguous term. If the refinement fails the current set of
-%choices cannot lead to a well-typed term and backtracking is attempted.
-%Once an unambiguous correct interpretation is found (i.e. $\Phi_i$ does no
-%longer contain any placeholder), backtracking is attempted
-%anyway to find the other correct interpretations.
-%
-%The intuition which explain why this algorithm is more efficient is that as soon
-%as a term containing placeholders is not typable, no further instantiation of
-%its placeholders could lead to a typable term. For example, during the
-%disambiguation of user input \texttt{\TEXMACRO{forall} x. x*0 = 0}, an
-%interpretation $\Phi_i$ is encountered which associates $?$ to the instance
-%of \texttt{0} on the right, the real number $0$ to the instance of \texttt{0} on
-%the left, and the multiplication over natural numbers (\texttt{mult} for short)
-%to \texttt{*}. The refiner will fail, since \texttt{mult} require a natural
-%argument, and no further instantiation of the placeholder will be tried.
-%
-%If, at the end of the disambiguation, more than one possible interpretations are
-%possible, the user will be asked to choose the intended one (see
-%Fig.~\ref{fig:disambiguation}).
-%
-%\begin{figure}[htb]
-%% \centerline{\includegraphics[width=0.9\textwidth]{disambiguation-1}}
-% \caption{\label{fig:disambiguation} Disambiguation: interpretation choice}
-%\end{figure}
-%
-%Details of the disambiguation algorithm of \WHELP{} can
-%be found in~\cite{disambiguation}, where an equivalent algorithm
-%that avoids backtracking is also presented.
+\begin{table}
+ \caption{\label{tab:termsyn} Concrete syntax of CIC terms: built-in notation\strut}
+\hrule
+\[
+\begin{array}{@{}rcll@{}}
+ \NT{term} & ::= & & \mbox{\bf terms} \\
+ & & x & \mbox{(identifier)} \\
+ & | & n & \mbox{(number)} \\
+ & | & s & \mbox{(symbol)} \\
+ & | & \mathrm{URI} & \mbox{(URI)} \\
+ & | & \verb+?+ & \mbox{(implicit)} \\
+ & | & \verb+?+n~[\verb+[+~\{\NT{subst}\}~\verb+]+] & \mbox{(meta)} \\
+ & | & \verb+let+~\NT{ptname}~\verb+\def+~\NT{term}~\verb+in+~\NT{term} \\
+ & | & \verb+let+~\NT{kind}~\NT{defs}~\verb+in+~\NT{term} \\
+ & | & \NT{binder}~\{\NT{ptnames}\}^{+}~\verb+.+~\NT{term} \\
+ & | & \NT{term}~\NT{term} & \mbox{(application)} \\
+ & | & \verb+Prop+ \mid \verb+Set+ \mid \verb+Type+ \mid \verb+CProp+ & \mbox{(sort)} \\
+ & | & \verb+match+~\NT{term}~ & \mbox{(pattern matching)} \\
+ & & ~ ~ [\verb+[+~\verb+in+~x~\verb+]+]
+ ~ [\verb+[+~\verb+return+~\NT{term}~\verb+]+] \\
+ & & ~ ~ \verb+with [+~[\NT{rule}~\{\verb+|+~\NT{rule}\}]~\verb+]+ & \\
+ & | & \verb+(+~\NT{term}~\verb+:+~\NT{term}~\verb+)+ & \mbox{(cast)} \\
+ & | & \verb+(+~\NT{term}~\verb+)+ \\
+ \NT{defs} & ::= & & \mbox{\bf mutual definitions} \\
+ & & \NT{fun}~\{\verb+and+~\NT{fun}\} \\
+ \NT{fun} & ::= & & \mbox{\bf functions} \\
+ & & \NT{arg}~\{\NT{ptnames}\}^{+}~[\verb+on+~x]~\verb+\def+~\NT{term} \\
+ \NT{binder} & ::= & & \mbox{\bf binders} \\
+ & & \verb+\forall+ \mid \verb+\lambda+ \\
+ \NT{arg} & ::= & & \mbox{\bf single argument} \\
+ & & \verb+_+ \mid x \\
+ \NT{ptname} & ::= & & \mbox{\bf possibly typed name} \\
+ & & \NT{arg} \\
+ & | & \verb+(+~\NT{arg}~\verb+:+~\NT{term}~\verb+)+ \\
+ \NT{ptnames} & ::= & & \mbox{\bf bound variables} \\
+ & & \NT{arg} \\
+ & | & \verb+(+~\NT{arg}~\{\verb+,+~\NT{arg}\}~[\verb+:+~\NT{term}]~\verb+)+ \\
+ \NT{kind} & ::= & & \mbox{\bf induction kind} \\
+ & & \verb+rec+ \mid \verb+corec+ \\
+ \NT{rule} & ::= & & \mbox{\bf rules} \\
+ & & x~\{\NT{ptname}\}~\verb+\Rightarrow+~\NT{term}
+\end{array}
+\]
+\hrule
+\end{table}
+
+\subsubsection{Term input}
+
+The primary form of user interaction employed by \MATITA{} is textual script
+editing: the user can modifies it and evaluate step by step its composing
+\emph{statements}. Examples of statements are inductive type definitions,
+theorem declarations, LCF-style tacticals, and macros (e.g. \texttt{Check} can
+be used to ask the system to refine a given term and pretty print the result).
+Since many statements refer to terms of the underlying calculus, \MATITA{} needs
+a concrete syntax able to encode terms of the Calculus of Inductive
+Constructions.
+
+Two of the requirements in the design of such a syntax are apparently in
+contrast:
+\begin{enumerate}
+ \item the syntax should be as close as possible to common mathematical practice
+ and implement widespread mathematical notions;
+ \item each term described by the syntax should be non-ambiguous meaning that it
+ should exists a function which associates to each term of the syntax a CIC
+ term.
+\end{enumerate}
+
+These two requirements are addressed in \MATITA{} by the mean of two mechanisms
+which work together: \emph{term disambiguation} and \emph{extensible notation}.
+Their interaction is visible in the architecture of the \MATITA{} input phase,
+depicted in Fig.~\ref{fig:inputphase}. The architecture is articulated as a
+pipline of three levels: the concrete syntax level (level 0) is the one the user
+has to deal with when inserting CIC terms; the abstract syntax level (level 2)
+is an internal representation which intuitively encodes mathematical formulae at
+the content level~\cite{adams}~\cite{mkm-structure}; the formal mathematics
+level (level 3) is the CIC encoding of terms.
+
+Requirement (1) is addressed by a built-in concrete syntax for terms, described
+in Tab.~\ref{tab:termsyn}, and the extensible notation mechanisms which offers a
+way for extending available mathematical notations. Extensible notation, which
+is also in charge of providing a parsing function mapping concrete syntax terms
+to content level terms, is described in Sect.~\ref{sec:notation}. Requirement
+(2) is addressed by the conjunct action of that parsing function and
+disambiguation which provides a function from content level terms to CIC terms.
+
+\subsubsection{Sources of ambiguity}
+
+The translation from content level terms to CIC terms is not straightforward
+because some nodes of the content encoding admit more that one CIC encoding,
+invalidating requirement (2).
+
+\begin{example}
+
+ Consider the term \texttt{\TEXMACRO{forall} x. x + ln 1 = x}, the type of a
+ lemma the user may want to prove. Assuming that both \texttt{+} and \texttt{=}
+ are parsed as infix operators, all the following questions are legitimate and
+ must be answered before obtaining a CIC term from its content level encoding
+ (Fig.~\ref{fig:inputphase}(b)):
+
+ \begin{enumerate}
+
+ \item Since \texttt{ln} is an unbound identifier, which CIC constants does it
+ represent? Many different theorems in the library may share its (rather
+ short) name \dots
+
+ \item Which kind of number (\IN, \IR, \dots) the \texttt{1} literal stand for?
+ Which encoding is used in CIC to represent it? E.g., assuming $1\in\IN$, is
+ it an unary or a binary encoding?
+
+ \item Which kind of equality the ``='' node represents? Is it Leibniz's
+ polymorhpic equality? Is it a decidable equality over \IN, \IR, \dots?
+
+ \end{enumerate}
+
+\end{example}
+
+In \MATITA, three \emph{sources of ambiguity} are admitted for content level
+terms: unbound identifiers, literal numbers, and literal symbols.
+
+\emph{Unbound identifiers} (question 1) are sources of ambiguity since the same
+name could have been used in the proof assistant library to represent different
+objects. \emph{Numbers} (question 2) are ambiguous since several different
+encodings of them could be provided in the calculus. Finally, \emph{symbols}
+(question 3) are ambiguous as well, since they may be used in an overloaded
+fashion to represent the application of different objects.
+
+\textbf{FINQUI, il resto \`e copy and paste dal Whelp paper \dots}
+
+Note that given a content level term with more than one sources of ambiguity,
+not all possible disambiguation choices are valid: for example, given the input
+\texttt{1+1} we must choose an interpretation of \texttt{+} which is typable in
+CIC according to the chosen interpretation for \texttt{1}; choosing as
+\texttt{+} the addition over natural numbers and as \texttt{1} the real number
+$1$ will lead to a type error.
+
+A \emph{disambiguation algorithm} takes as input an ambiguous term and return a
+fully determined CIC term. The \emph{naive disambiguation algorithm} takes as
+input an ambiguous term $t$ and proceeds as follows:
+
+\begin{enumerate}
+
+ \item Create disambiguation domains $\{D_i | i\in\mathit{Dom}(t)\}$, where
+ $\mathit{Dom}(t)$ is the set of ambiguity sources of $t$. Each $D_i$ is a set
+ of CIC terms.
+
+ \item Let $\Phi = \{\phi_i | {i\in\mathit{Dom}(t)},\phi_i\in D_i\}$
+% such that $\forall i\in\mathit{Dom}(t),\exists\phi_j\in\Phi,i=j$
+ be an interpretation for $t$. Given $t$ and an interpretation $\Phi$, a CIC
+ term is fully determined. Iterate over all possible interpretations of $t$ and
+ type-check them, keep only typable interpretations (i.e. interpretations that
+ determine typable terms).
+
+ \item Let $n$ be the number of interpretations who survived step 2. If $n=0$
+ signal a type error. If $n=1$ we have found exactly one CIC term
+ corresponding to $t$, returns it as output of the disambiguation phase.
+ If $n>1$ let the user choose one of the $n$ interpretations and returns the
+ corresponding term.
+
+\end{enumerate}
+
+The above algorithm is highly inefficient since the number of possible
+interpretations $\Phi$ grows exponentially with the number of ambiguity sources.
+The actual algorithm used in \WHELP{} is far more efficient being, in the
+average case, linear in the number of ambiguity sources.
+
+The efficient algorithm can be applied if the logic can be extended with
+metavariables and a refiner can be implemented. This is the case for CIC and
+several other logics.
+\emph{Metavariables}~\cite{munoz} are typed, non linear placeholders that can
+occur in terms; $?_i$ usually denotes the $i$-th metavariable, while $?$ denotes
+a freshly created metavariable. A \emph{refiner}~\cite{McBride} is a
+function whose input is a term with placeholders and whose output is either a
+new term obtained instantiating some placeholder or $\epsilon$, meaning that no
+well typed instantiation could be found for the placeholders occurring in
+the term (type error).
+
+The efficient algorithm starts with an interpretation $\Phi_0 = \{\phi_i |
+\phi_i = ?, i\in\mathit{Dom}(t)\}$,
+which associates a fresh metavariable to each
+source of ambiguity. Then it iterates refining the current CIC term (i.e. the
+term obtained interpreting $t$ with $\Phi_i$). If the refinement succeeds the
+next interpretation $\Phi_{i+1}$ will be created \emph{making a choice}, that is
+replacing a placeholder with one of the possible choice from the corresponding
+disambiguation domain. The placeholder to be replaced is chosen following a
+preorder visit of the ambiguous term. If the refinement fails the current set of
+choices cannot lead to a well-typed term and backtracking is attempted.
+Once an unambiguous correct interpretation is found (i.e. $\Phi_i$ does no
+longer contain any placeholder), backtracking is attempted
+anyway to find the other correct interpretations.
+
+The intuition which explain why this algorithm is more efficient is that as soon
+as a term containing placeholders is not typable, no further instantiation of
+its placeholders could lead to a typable term. For example, during the
+disambiguation of user input \texttt{\TEXMACRO{forall} x. x*0 = 0}, an
+interpretation $\Phi_i$ is encountered which associates $?$ to the instance
+of \texttt{0} on the right, the real number $0$ to the instance of \texttt{0} on
+the left, and the multiplication over natural numbers (\texttt{mult} for short)
+to \texttt{*}. The refiner will fail, since \texttt{mult} require a natural
+argument, and no further instantiation of the placeholder will be tried.
+
+If, at the end of the disambiguation, more than one possible interpretations are
+possible, the user will be asked to choose the intended one (see
+Fig.~\ref{fig:disambiguation}).
+
+\begin{figure}[htb]
+% \centerline{\includegraphics[width=0.9\textwidth]{disambiguation-1}}
+ \caption{\label{fig:disambiguation} Disambiguation: interpretation choice}
+\end{figure}
+
+Details of the disambiguation algorithm of \WHELP{} can
+be found in~\cite{disambiguation}, where an equivalent algorithm
+that avoids backtracking is also presented.
\subsection{notazione}
+\label{sec:notation}
\ASSIGNEDTO{zack}
\subsection{libreria tutta visibile}
A.Griggio, F.Guidi, P. Di Lena, L.Padovani, I.Schena, M.Selmi,
V.Tamburrelli.
-
-\begin{thebibliography}{}
-
- \bibitem{ida}A.Asperti, H.Geuvers, I.Loeb, L.E.Mamane, C.Sacerdoti Coen.
- An Interactive Algebra Course with Formalised Proofs and Definitions.
- Post-Proceedings of the Fourth International Conference on
- Mathemtical Knowledge Management. Bremen, Germany, July 2005. LNCS,
- to appear.
-
- \bibitem{annals} A.~Asperti, F.~Guidi, L.~Padovani, C.~Sacerdoti Coen,
- I.~Schena. \emph{Mathematical Knowledge Management in HELM}. Annals of
- Mathematics and Artificial Intelligence, 38(1): 27--46; May 2003.
-
- \bibitem{whelp} A.~Asperti, F.~Guidi, C.~Sacerdoti Coen,
- E.Tassi, S.Zacchiroli. \emph{A content based mathematical search
- engine: whelp}. Post-proceedings of the Types 2004 International
- Conference, Jouy-en-Josas, France, December 2004. LNCS (to appear).
-
- \bibitem{metadata2} A. Asperti, M. Selmi. \emph{Efficient Retrieval of
- Mathematical Statements}. In Proceeding of the Third International Conference
- on Mathematical Knowledge Management, MKM 2004. Bialowieza, Poland. LNCS 3119.
- \bibitem{pechino} A.Asperti, B.Wegner. \emph{An Approach to
- Machine-Understandable Representation of the Mathematical Information in
- Digital Documents}. In: Fengshai Bai and Bernd Wegner (eds.): Electronic
- Information and Communication in Mathematics, LNCS vol. 2730,
- pp. 14--23, 2003
-
- \bibitem{coq} The Coq proof-assistant, \url{http://coq.inria.fr}
-
- \bibitem{metadata1} F. Guidi, C. Sacerdoti Coen. \emph{Querying Distributed
- Digital Libraries of Mathematics}. In Proceedings of Calculemus 2003, 11th
- Symposium on the Integration of Symbolic Computation and Mechanized
- Reasoning. Aracne Editrice.
-
- \bibitem{exportation} C. Sacerdoti Coen. \emph{From Proof-Assistans to
- Distributed Libraries of Mathematics: Tips and Pitfalls}.
- In Proc. Mathematical Knowledge Management 2003, Lecture Notes in Computer
- Science, Vol. 2594, pp. 30--44, Springer-Verlag.
-
- \bibitem{disambiguation} C. Sacerdoti Coen, S. Zacchiroli. \emph{Efficient
- Ambiguous Parsing of Mathematical Formulae}. In Proceedings of the Third
- International Conference on Mathematical Knowledge Management, MKM 2004.
- LNCS,3119.
-
-\end{thebibliography}
+\bibliography{matita}
\end{document}
projects / helm.git / blobdiff