\newcommand{\AUTO}{\textsc{Auto}}
\newcommand{\COQ}{Coq}
\newcommand{\ELIM}{\textsc{Elim}}
+\newcommand{\GDOME}{Gdome}
\newcommand{\HELM}{Helm}
\newcommand{\HINT}{\textsc{Hint}}
\newcommand{\IN}{\ensuremath{\dN}}
\newcommand{\REF}[3]{\ensuremath{\mathit{Ref}_{#1}(#2,#3)}}
\newcommand{\TEXMACRO}[1]{\texttt{\char92 #1}}
\newcommand{\UWOBO}{UWOBO}
+\newcommand{\GETTER}{Getter}
\newcommand{\WHELP}{Whelp}
\newcommand{\DOT}{\ensuremath{\mbox{\textbf{.}}}}
\newcommand{\SEMICOLON}{\ensuremath{\mbox{\textbf{;}}}}
\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}
+DESCRIZIONE DEL SISTEMA DAL PUNTO DI VISTA ``UTENTE''
+
+\begin{itemize}
+ \item scelta del sistema fondazionale
+ \item sistema indipendente (da Coq)
+ \item compatibilit\`a con sistemi legacy
+\end{itemize}
+
+\subsection{Relationship with \COQ{}}
+
+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{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}
Modules and libraries provide coherent sets of functionalities
at different scales. Applications that require only a few functionalities
-depend on a restricted set of libraries. \MATITA, our most complex
-application, depends on every library.
+depend on a restricted set of libraries.
-Only the proof assistant \MATITA{} is an application meant to be used directly
-by the user. All the other applications are Web services developed in the
-HELM and MoWGLI projects and already described elsewhere. In particular:
+Only the proof assistant \MATITA{} and the \WHELP{} search engine are
+applications meant to be used directly by the user. All the other applications
+are Web services developed in the HELM and MoWGLI projects and already described
+elsewhere. In particular:
\begin{itemize}
\item The \emph{Getter} is a Web service to retrieve an (XML) document
from a physical location (URL) given its logical name (URI). The Getter is
responsible of updating a table that maps URIs to URLs. Thanks to the Getter
it is possible to work on a logically monolithic library that is physically
distributed on the network. More information on the Getter can be found
- in~\cite{getter}.
+ in~\cite{zack-master}.
\item \emph{Whelp} is a search engine to index and locate mathematical
notions (axioms, theorems, definitions) in the logical library managed
by the Getter. Typical examples of a query to Whelp are queries that search
two dimensional mathematical notation. Uwobo may also embed the rendering
of mathematical notions into arbitrary documents before returning them.
The Getter is used by Uwobo to retrieve the document to be rendered.
- Uwobo has been described in~\cite{uwobo}.
+ Uwobo has been described in~\cite{zack-master}.
\item The \emph{Proof Checker} is a Web service that, given the URI of
notion in the distributed library, checks its correctness. Since the notion
is likely to depend in an acyclic way over other notions, the proof checker
is also responsible of building in a top-down way the DAG of all
dependencies, checking in turn every notion for correctness.
- The proof checker has been described in~\cite{proofchecker}.
+ The proof checker has been described in~\cite{zack-master}.
\item The \emph{Dependency Analyzer} is a Web service that can produce
a textual or graphical representation of the dependecies of an object.
- The dependency analyzer has been described in~\cite{dependencyanalyzer}.
+ The dependency analyzer has been described in~\cite{zack-master}.
\end{itemize}
The dependency of a library or application over another library can
that forwards every request to the Getter.
To better understand the architecture of \MATITA{} and the role of each
-library, we can focus on the rappresentation of the mathematical information.
+library, we can focus on the representation of the mathematical information.
\MATITA{} is based on (a variant of) the Calculus of (Co)Inductive
Constructions (CIC). In CIC terms are used to represent mathematical
expressions, types and proofs. \MATITA{} is able to handle terms at
-four different levels of refinement. On each level it is possible to provide a
-different set of functionalities. The four different levels are:
-fully specified terms; partially specified terms; terms
-at the content level; terms at the presentation level.
+four different levels of specification. On each level it is possible to provide
+a different set of functionalities. The four different levels are:
+fully specified terms; partially specified terms;
+content level terms; presentation level terms.
\subsection{Fully specified terms}
\emph{Fully specified terms} are CIC terms where no information is
every time it needs to retrieve the definition of a mathematical notion
referenced by a term that is being type-checked.
- The Proof Checker is the Web service that provides an HTTP interface
+ The Proof Checker is the Web service that provides an interface
to the \texttt{cic\_proof\_checking} library.
We use metadata and a sort of crawler to index the mathematical notions
a procedure that makes two partially specified term convertible by instantiating
as few as possible metavariables that occur in them.
-Since terms are use in CIC to represent proofs, so far correct incomplete
+Since terms are used in CIC to represent proofs, correct incomplete
proofs are represented by refinable partially specified terms. The metavariables
that occur in the proof correspond to the conjectures still to be proved.
The sequent associated to the metavariable is the conjecture the user needs to
proof. A tactic proves a conjecture possibly creating new (and hopefully
simpler) conjectures. The implementation of tactics is given in the
\texttt{tactics} library. It is heavily based on the refinement and unification
-procedures of the \texttt{cic\_unification} library.
+procedures of the \texttt{cic\_unification} library. \TODO{citare paramodulation
+da qualche part o toglierla dal grafo}
As fully specified terms, partially specified terms are not well suited
for user consumption since their syntax is not extendible and it is not
an improvement over fully specified terms since they allow to omit redundant
information that can be inferred by the refiner.
-\subsection{Terms at the content level}
+\subsection{Content level terms}
+\label{sec:contentintro}
+
The language used to communicate proofs and expecially expressions with the
user does not only needs to be extendible and accomodate the usual mathematical
notation. It must also reflect the comfortable degree of imprecision and
For instance, it is common practice in mathematics to speak of a generic
equality that can be used to compare any two terms. However, it is well known
-that several equalities can be identified as soon as we care for decidability
+that several equalities can be distinguished as soon as we care for decidability
or for their computational properties. For instance equality over real
numbers is well known to be undecidable, whereas it is decidable over
rational numbers.
Mathematical Knowledge Management community this imprecise language is called
the \emph{content level} representation of expressions.
-In \MATITA{} we provide two translations from partially refined terms
+In \MATITA{} we provide two translations: from partially specified terms
to content level terms and the other way around. The first translation can also
-be applied to fully refined terms since a fully refined term is a special case
-of partially refined term where no metavariable or implicit term occurs.
+be applied to fully specified terms since a fully specified term is a special
+case of partially specified term where no metavariable or implicit term occurs.
-The translation from partially refined terms to content level terms must
+The translation from partially specified terms to content level terms must
discriminate between terms used to represent proofs and terms used to represent
expressions. The firsts are translated to a content level representation of
-proofs steps that can easily be rendered in natural language. The latters
-are translated to MathML Content formulae. MathML Content is a W3C standard
+proof steps that can easily be rendered in natural language. The latters
+are translated to MathML Content formulae. MathML Content~\cite{mathml} is a W3C
+standard
for the representation of content level expressions in an XML extensible format.
The translation to content level is implemented in the
-\texttt{acic\_to\_content} library. Its input are \emph{annotated partially
-refined terms}. Annotated partially refined terms are maximally unshared
-partially refined terms enriched with additional typing information for each
+\texttt{acic\_content} library. Its input are \emph{annotated partially
+specified terms}, that are maximally unshared
+partially specified terms enriched with additional typing information for each
subterm. This information is used to discriminate between terms that represent
proofs and terms that represent expressions. Part of it is also stored at the
content level since it is required to generate the natural language rendering
-of proofs. The \emph{cic\_to\_acic} library annotates partially refined terms.
-
-The translation from content level terms to partially refined terms is
-also performed in \ldots ???
-
-\subsection{Terms at the presentation level}
+of proofs. The terms need to be maximally unshared (i.e. they must be a tree
+and not a DAG). The reason is that to the occurrences of a subterm in
+two different positions we need to associate different typing informations.
+This association is made easier when the term is represented as a tree since
+it is possible to label each node with an unique identifier and associate
+the typing information using a map on the identifiers.
+The \texttt{cic\_acic} library annotates partially specified terms.
+
+We do not provide yet a reverse translation from content level proofs to
+partially specified terms. But in \texttt{disambiguation} we do provide
+the reverse translation for expressions. The mapping from
+content level expressions to partially specified terms is not unique due to
+the ambiguity of the content level. As a consequence the translation
+is guided by an \emph{interpretation}, that is a function that chooses for
+every ambiguous expression one partially specified term. The
+\texttt{disambiguation} library contains the implementation of the
+disambiguation algorithm we presented in~\cite{disambiguation} that is
+responsible of building in an efficicent way the set of all ``correct''
+interpretations. An interpretation is correct if the partially specified term
+obtained using the interpretation is refinable.
+
+\subsection{Presentation level terms}
+
+Content level terms are a sort of abstract syntax trees for mathematical
+expressions and proofs. The concrete syntax given to these abstract trees
+is called \emph{presentation level}.
+
+The main important difference between the content level language and the
+presentation level language is that only the former is extendible. Indeed,
+the presentation level language is a finite language that comprises all
+the usual mathematical symbols. Mathematicians invent new notions every
+single day, but they stick to a set of symbols that is more or less fixed.
+
+The fact that the presentation language is finite allows the definition of
+standard languages. In particular, for formulae we have adopt MathML
+Presentation~\cite{mathml} that is an XML dialect standardized by the W3C. To
+visually
+represent proofs it is enough to embed formulae in plain text enriched with
+formatting boxes. Since the language of formatting boxes is very simple,
+many equivalent specifications exist and we have adopted our own, called
+BoxML.
+
+The \texttt{content\_pres} library contains the implementation of the
+translation from content level terms to presentation level terms. The
+rendering of presentation level terms is left to the application that uses
+the library. However, in the \texttt{hgdome} library we provide a few
+utility functions to build a \GDOME~\cite{gdome2} MathML+BoxML tree from our
+presentation
+level terms. \GDOME{} MathML+BoxML trees can be rendered by the GtkMathView
+widget developed by Luca Padovani \cite{padovani}. The widget is
+particularly interesting since it allows to implement \emph{semantic
+selection}.
+
+Semantic selection is a technique that consists in enriching the presentation
+level terms with pointers to the content level terms and to the partially
+specified terms they correspond to. Highlight of formulae in the widget is
+constrained to selection of meaningful expressions, i.e. expressions that
+correspond to a lower\footnote{\TODO{non abbiamo parlato di ``ordine''}} level term. Once the rendering of a lower level term is
+selected it is possible for the application to retrieve the pointer to the
+lower level term. An example of applications of semantic selection is
+\emph{semantic cut\&paste}: the user can select an expression and paste it
+elsewhere preserving its semantics (i.e. the partially specified term),
+possibly performing some semantic transformation over it (e.g. renaming
+variables that would be captured or lambda-lifting free variables).
+
+The reverse translation from presentation level terms to content level terms
+is implemented by a parser that is also found in \texttt{content\_pres}.
+Differently from the translation from content level terms to partially
+refined terms, this translation is not ambiguous. The reason is that the
+parsing library we have adopted (CamlP4) is not able to parse ambiguous
+grammars. Thus we require the mapping from presentation level terms
+(concrete syntax) to content level terms (abstract syntax) to be unique.
+This means that the user must fix once and for all the associativity and
+precedence level of every operator he is using. In prctice this limitation
+does not seem too strong. The reason is that the target of the
+translation is an ambiguous language and the user is free to associate
+to every content level term several different interpretations (as a
+partially specified term).
+
+The \MATITA{} proof assistant and the \WHELP{} search engine are both linked
+against the \texttt{cic\_disambiguation} and \texttt{content\_pres} libraries
+since they provide an interface to the user. In both cases the formulae
+written by the user are parsed using the \texttt{content\_pres} library and
+then disambiguated using the \texttt{cic\_disambiguation} library.
+
+The \UWOBO{} Web service wraps the \texttt{content\_pres} library,
+providing a rendering service for the documents in the distributed library.
+To render a document given its URI, \UWOBO{} retrieves it using the
+\GETTER{} obtaining a document with fully specified terms. Then it translates
+it to the presentation level passing through the content level. Finally
+it returns the result document to be rendered by the user's
+browser.\footnote{\TODO{manca la passata verso HTML}}
\hrule
goal) gives you the feeling of what is going on.
\end{description}
+\section{Content level terms}
+
+\subsection{Disambiguation}
+
+Software applications that involve input of mathematical content should strive
+to require the user as less drift from informal mathematics as possible. We
+believe this to be a fundamental aspect of such applications user interfaces.
+Being that drift in general very large when inputing
+proofs~\cite{debrujinfactor}, in \MATITA{} we achieved good results for
+mathematical formulae which can be input using a \TeX-like encoding (the
+concrete syntax corresponding to presentation level terms) and are then
+translated (in multiple steps) to partially specified terms as sketched in
+Sect.~\ref{sec:contentintro}.
+
+The key component of the translation is the generic disambiguation algorithm
+implemented in the \texttt{disambiguation} library of Fig.~\ref{fig:libraries}
+and presented in~\cite{disambiguation}. In this section we present how to use
+such an algorithm in the context of the development of a library of formalized
+mathematics. We proceed by examples took from the \MATITA{} standard library.
+
+\subsubsection{Disambiguation aliases}
+
+Let's start with the definition of the ``strictly greater then'' notion over
+(Peano) natural numbers.
+
+\begin{grafite}
+include "nat/nat.ma".
+..
+definition gt: nat \to nat \to Prop \def
+ \lambda n, m. m < n.
+\end{grafite}
+
+The \texttt{include} statement adds the requirement that the part of the library
+defining the notion of (Peano) natural numbers should be defined before
+processing the following definition. Note indeed that the algorithm presented
+in~\cite{disambiguation} does not describe where interpretations for ambiguous
+expressions come from, since it is application-specific. As a first
+approximation, we will assume that in \MATITA{} they come from the library (i.e.
+all interpretations available in the library are used) and the \texttt{include}
+statements are used to ensure the availability of required library slices (see
+Sect.~\ref{sec:libmanagement}).
+
+While processing the \texttt{gt} definition, \MATITA{} has to disambiguate two
+terms: its type and its body. Being available in the required library only one
+interpretation both for the unbound identifier \texttt{nat} and for the
+\texttt{<} operator, and being the resulting partially specified term refinable,
+both type and body are easily disambiguated.
+
+Now suppose we have defined integers as signed Peano numbers, and that we want
+to prove a theorem about an order relationship already defined on them (which of
+course overload the \texttt{<} operator):
+
+\begin{grafite}
+include "Z/z.ma".
+..
+theorem Zlt_compat:
+ \forall x, y, z. x < y \to y < z \to x < z.
+\end{grafite}
+
+Since integers are defined on top of Peano numbers, the part of the library
+concerning the latters is available when disambiguating \texttt{Zlt\_compat}'s
+type. Thus, according to the disambiguation algorithm, two different partially
+specified terms could be associated to it. At first, this might not be seen as a
+problem, since the user is asked and can choose interactively which of the two
+she had in mind. However in the long run it has the drawbacks of inhibiting
+batch compilation of the library (a technique used in \MATITA{} for behind the
+scene compilation when needed, e.g. when an \texttt{include} is issued) and
+yields to poor user interaction (imagine how tedious would be to be asked for a
+choice each time you re-evaluate \texttt{Zlt\_compat}!).
+
+For this reason we added to \MATITA{} the concept of \emph{disambiguation
+aliases}. Disambiguation aliases are one-to-many mappings from ambiguous
+expressions to partially specified terms, which are part of the runtime status
+of \MATITA. They can be provided by users with the \texttt{alias} statement, but
+are usually automatically added when evaluating \texttt{include} statements
+(\emph{implicit aliases}). Moreover, \MATITA{} does it best to ensure that
+terms which require interactive choice are saved in batch compilable format.
+Thus, after evaluating the above theorem the script will be changed to the
+following snippet (assuming that the interpretation of \texttt{<} over integers
+has been choosed):
+
+\begin{grafite}
+alias symbol "lt" (instance 0) = "integer 'less than'".
+theorem Zlt_compat:
+ \forall x, y, z. x < y \to y < z \to x < z.
+\end{grafite}
+
+But how are disambiguation aliases used? Since they come from the parts of the
+library explicitely included we may be tempted of using them as the only
+available interpretations. This would speed up the disambiguation, but may fail.
+Consider for example:
+
+\begin{grafite}
+theorem lt_mono: \forall x, y, k. x < y \to x < y + k.
+\end{grafite}
+
+and suppose that the \texttt{+} operator is defined only on Peano numbers. If
+the alias for \texttt{<} points to the integer version of the operator, no
+refinable partially specified term matching the term could be found.
+
+For this reason we choosed to attempt \emph{multiple disambiguation passes}. A
+first pass attempt to disambiguate using the last available disambiguation
+aliases, in case of failure the next pass try again the disambiguation
+forgetting the aliases and using the whole library to retrieve interpretation
+for ambiguous expressions. Since the latter pass may lead to too many choices we
+intertwined an additional pass among the two which use as interpretations all
+the aliases coming for included parts of the library (this is the reason why
+aliases are \emph{one-to-many} mappings instead of one-to-one). This choice
+turned out to be a well-balanced trade-off among performances (earlier passes
+fail quickly) and degree of ambiguity supported for presentation level terms.
+
+\subsubsection{Operator instances}
\acknowledgements
We would like to thank all the students that during the past
five years collaborated in the \HELM{} project and contributed to
the development of Matita, and in particular
-A.Griggio, F.Guidi, P. Di Lena, L.Padovani, I.Schena, M.Selmi,
-V.Tamburrelli.
+A.~Griggio, F.~Guidi, P.~Di~Lena, L.~Padovani, I.~Schena, M.~Selmi,
+and V.~Tamburrelli.
\theendnotes
\bibliography{matita}
-
\end{document}
projects / helm.git / blobdiff