From: Claudio Sacerdoti Coen Date: Fri, 25 Nov 2005 15:22:51 +0000 (+0000) Subject: Confronto con Coq. X-Git-Tag: make_still_working~8098 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d2c251dfd0524ae22a4ef44e8e964d5b0a0f155c;p=helm.git Confronto con Coq. --- diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex index d1cc2e54d..491e92548 100644 --- a/helm/papers/matita/matita2.tex +++ b/helm/papers/matita/matita2.tex @@ -116,12 +116,150 @@ Digital Libraries} \end{opening} +\section{Introduction} +\label{sec:intro} +In this paper we describe the architecture and a few distintive features of the +\emph{\MATITA} proof assistant. \MATITA{} was not conceived out of the blue +one single day; it has been the next natural step in the evolution of one +line of research we started six years ago. Thus, to better understand the +system, we start from its historical roots. + +\subsection{Historical Perspective} +\MATITA{} is under development by the \HELM{} team +\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 +via Web of formal libraries of mathematics. Due to its dimension, the +library of the \COQ{} proof assistant (of the order of 35'000 theorems) +was choosed as a privileged test bench for our work, although experiments +have been also conducted with other systems, and notably with \NUPRL{}. +The work, mostly performed in the framework of the recently concluded +European project IST-33562 \MOWGLI{}~\cite{pechino}, mainly consisted in the +following teps: +\begin{itemize} +\item exporting the information from the internal representation of + \COQ{} to a system and platform independent format. Since XML was at the +time an emerging standard, we naturally adopted this technology, fostering +a content-centric architecture for future system, where the documents +of the library were the the main components around which everything else +has to be build; +\item developing indexing and searching techniques supporting semantic + queries to the library; these efforts gave birth to our \WHELP{} +search engine, described in~\cite{whelp}; +\item developing languages and tools for a high-quality notational +rendering of mathematical information; in particular, we have been +active in the MathML Working group since 1999, and developed inside +\HELM{} a MathML-compliant widget for the GTK graphical environment +which can be integrated in any application. +\end{itemize} + +According to our content-centric commitment, the library exported from +Coq was conceived as being distributed and most of the tools were developed +as Web services. The user could interact with the library and the tools by +means of a Web interface that orchestrates the Web services. + +The Web services and the other tools have been implemented as front-ends +to a set of libraries, collectively called the \HELM{} libraries. +At the end of the \MOWGLI{} project we already disposed of the following +techniques and libraries: +\begin{itemize} +\item XML specifications for the Calculus of Inductive Constructions, +with libraries for parsing and saving mathematical objects in such a format; +\item metadata specifications with libraries for indexing and querying the +XML knowledge base; +\item a proof checker library (i.e. the {\em kernel} of a proof assistant), +implemented to check that we exported form the \COQ{} library all the +logically relevant content; +\item a sophisticated parser (used by the search engine), able to deal +with potentially ambiguous and incomplete information, typical of the +mathematical notation \cite{disambiguation}; +\item a {\em refiner} library, i.e. a type inference system, based on +partially specified terms, used by the disambiguating parser; +\item complex transformation algorithms for proof rendering in natural +language; +\item an innovative rendering widget, supporting high-quality bidimensional +rendering, and semantic selection, i.e. the possibility to select semantically +meaningful rendering expressions, and to past the respective content into +a different text area. +\end{itemize} +Starting from all this, the further step of developing our own +proof assistant was too +small and too tempting to be neglected. Essentially, we ``just'' had to +add an authoring interface, and a set of functionalities for the +overall management of the library, integrating everything into a +single system. \MATITA{} is the result of this effort. + +\subsection{The System} + +At first sight, \MATITA{} looks as (and partly is) a \COQ{} clone. This is +more the effect of the circumstances of its creation described +above than the result of a deliberate design. In particular, we +(essentially) share the same foundational dialect of \COQ{} (the +Calculus of (Co)Inductive Constructions), the same implementative +language (\OCAML{}), and the same (script based) authoring philosophy. +However, the analogy essentially stops here and no code is shared by the +two systems. + +In a sense; we like to think of \MATITA{} as the way \COQ{} would +look like if entirely rewritten from scratch: just to give an +idea, although \MATITA{} currently supports almost all functionalities of +\COQ{}, it links 60'000 lines of \OCAML{} code, against the 166'000 lines linked +by \COQ{} (and we are convinced that, starting from scratch again, +we could furtherly reduce our code in sensible way). + +Moreover, the complexity of the code of \MATITA{} is greatly reduced with +respect to \COQ. For instance, the API of the libraries of \MATITA{} comprise +916 functions, to be compared with the 4'286 functions of \COQ. + +Finally, \MATITA{} has several innovatives features over \COQ{} that derive +from the integration of Mathematical Knowledge Management tools with proof +assistants. Among them, the advanced indexing tools over the library and +the parser for ambiguous mathematical notation. + +The size and complexity improvements over \COQ{} must be understood +historically. \COQ{} is a quite old +system whose development started 15\NOTE{Verificare} years ago. Since then +several developers have took over the code and several new research ideas +that were not considered in the original architecture have been experimented +and integrated in the system. Moreover, there exists a lot of developments +for \COQ{} that require backward compatibility between each pair of releases; +since many central functionalities of a proof assistant are based on heuristics +or arbitrary choices to overcome undecidability (e.g. for higher order +unification), changing these functionalities mantaining backward compatibility +is very difficult. Finally, the code of \COQ{} has been greatly optimized +over the years; optimization reduces maintenability and rises the complexity +of the code. + +In writing \MATITA{} we have not been hindered by backward compatibility and +we have took advantage of the research results and experiences previously +developed by others, comprising the authors of \COQ. Moreover, starting from +scratch, we have designed in advance the architecture and we have splitted +the code in coherent minimally coupled libraries. + +In the future we plan to exploit \MATITA{} as a test bench for new ideas and +extensions. Keeping the single libraries and the whole architecture as +simple as possible is thus crucial to speed up future experiments and to +allow other developers to quickly understand our code and contribute. +For direct experience of the authors, the learning curve to understand and +be able to contribute to \COQ{}'s code is quite steep and requires direct +and frequent interactions with \COQ{} developers. + +\begin{itemize} + \item scelta del sistema fondazionale + \item sistema indipendente (da Coq) + \begin{itemize} + \item possibilit\`a di sperimentare (soluzioni architetturali, logiche, + implementative, \dots) + \item compatibilit\`a con sistemi legacy + \end{itemize} +\end{itemize} + \begin{figure}[t] \begin{center} \includegraphics[width=0.9\textwidth]{librariesCluster.ps} - \caption{\MATITA{} libraries} + \caption{\label{fig:libraries}\MATITA{} libraries} \end{center} - \label{fig:libraries} \end{figure} \section{Overview of the Architecture}