\end{opening}
\tableofcontents
+\listoffigures
\section{Introduction}
\label{sec:intro}
\cite{mkm-helm} at the University of Bologna, under the direction of
Prof.~Asperti. \\
The paper describes the overall architecture of
-the system, focusing on its most distintive and innovative
+the system, focusing on its most distinctive and innovative
features.
\subsection{Historical Perspective}
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~\cite{CoqManual} proof assistant (of the order of 35'000 theorems)
-was choosed as a privileged test bench for our work, although experiments
+was chosen as a privileged test bench for our work, although experiments
have been also conducted with other systems, and notably
-with \NUPRL{}\cite{nuprl-book}.
+with \NUPRL~\cite{nuprl-book}.
The work, mostly performed in the framework of the recently concluded
European project IST-33562 \MOWGLI{}~\cite{pechino}, mainly consisted in the
following steps:
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\footnote{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
\subsection{The system}
\MATITA{} is a proof assistant (also called interactive theorem prover).
-It is based on the Calculus of (Co)Inductive Constructions (CIC) that
-is a dependently typed lambda-calculus \`a la Church enriched with primitive
-inductive and co-indutive data types. Via the Curry-Howard isomorphism, the
-calculus can be seen as a very rich higher order logic and proofs can be
-simply represented and stored as lambda-terms. Coq and Lego are other systems
-that adopt (variations of) CIC as their foundation.
+It is based on the Calculus of (Co)Inductive Constructions
+(CIC)~\cite{Werner} that is a dependently typed lambda-calculus \`a la
+Church enriched with primitive inductive and co-inductive data types.
+Via the Curry-Howard isomorphism, the calculus can be seen as a very
+rich higher order logic and proofs can be simply represented and
+stored as lambda-terms. \COQ{} and Lego are other systems that adopt
+(variations of) CIC as their foundation.
The proof language of \MATITA{} is procedural, in the tradition of the LCF
theorem prover. Coq, NuPRL, PVS, Isabelle are all examples of others systems
primary mean of communication of proofs (once rendered to natural language
for human audiences).
-The user interfaces now adopted by all the proof assistants that adopt a
+The user interfaces now adopted by all the proof assistants based on a
procedural proof language have been inspired by the CtCoq pioneering
-system~\cite{ctcoq}. One succesfull incarnation of the ideas introduced
+system~\cite{ctcoq1}. One successful incarnation of the ideas introduced
by CtCoq is the Proof General generic interface~\cite{proofgeneral},
that has set a sort of
standard way to interact with the system. Several procedural proof assistants
have either adopted or cloned Proof General as their main user interface.
-\MATITA{} has also cloned the Proof General interface,
+The authoring interface of \MATITA{} is a clone of the Proof General interface.
\begin{itemize}
- \item scelta del sistema fondazionale
+ \item scelta del sistema fondazional.
\item sistema indipendente (da \COQ)
\item compatibilit\`a con sistemi legacy
\end{itemize}
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
+Calculus of (Co)Inductive Constructions), the same implementation
language (\OCAML{}), and the same (script based) authoring philosophy.
However, the analogy essentially stops here and no code is shared by the
two systems.
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).
+we could reduce our code even further in sensible way).
Moreover, the complexity of the code of \MATITA{} is greatly reduced with
respect to \COQ. For instance, the API of the components of \MATITA{} comprise
989 functions, to be compared with the 4'286 functions of \COQ.
-Finally, \MATITA{} has several innovatives features over \COQ{} that derive
+FINQUI SPELL CHECKATO
+
+Finally, \MATITA{} has several innovative 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.
\begin{figure}[!ht]
\begin{center}
\includegraphics[width=0.9\textwidth,height=0.8\textheight]{libraries-clusters}
- \caption{\MATITA{} components}
+ \caption[\MATITA{} components and related applications]{\MATITA{}
+ components and related applications, with thousands of line of
+ codes (klocs)}
\label{fig:libraries}
\end{center}
\end{figure}
Fig.~\ref{fig:libraries} shows the architecture of the \emph{\components}
(circle nodes) and \emph{applications} (squared nodes) developed in the HELM
-project.
+project. Each node is annotated with the number of lines of source code
+(comprising comments).
Applications and \components{} depend over other \components{} forming a
directed acyclic graph (DAG). Each \component{} can be decomposed in
For those \components{} whose functionalities are also provided by the
aforementioned Web services, it is also possible to link stub code that
forwards the request to a remote Web service. For instance, the Getter
-is just a wrapper to the \GETTER \component{} that allows the
+is just a wrapper to the \GETTER{} \component{} that allows the
\component{} to be used as a Web service. \MATITA{} can directly link the code
-of the \GETTER \component, or it can use a stub library with the same
+of the \GETTER{} \component, or it can use a stub library with the same
API that forwards every request to the Getter.
To better understand the architecture of \MATITA{} and the role of each
content level terms; presentation level terms.
\subsection{Fully specified terms}
-\label{fully-spec}
+\label{sec:fullyspec}
+
\emph{Fully specified terms} are CIC terms where no information is
missing or left implicit. A fully specified term should be well-typed.
The mathematical notions (axioms, definitions, theorems) that are stored
Terms may reference other mathematical notions in the library.
One commitment of our project is that the library should be physically
- distributed. The \GETTER \component{} manages the distribution,
+ distributed. The \GETTER{} \component{} manages the distribution,
providing a mapping from logical names (URIs) to the physical location
of a notion (an URL). The \texttt{urimanager} \component{} provides the URI
data type and several utility functions over URIs. The
in Sect.~\ref{sec:libmanagement}.
\subsection{Partially specified terms}
+\label{sec:partspec}
+
\emph{Partially specified terms} are CIC terms where subterms can be omitted.
Omitted subterms can bear no information at all or they may be associated to
a sequent. The formers are called \emph{implicit terms} and they occur only
interpretations. An interpretation is correct if the partially specified term
obtained using the interpretation is refinable.
-In the last section we have described the semantics of a command as a
+In Sect.~\ref{sec:partspec} the last section we described the semantics of a
+command as a
function from status to status. We also suggested that the formulae in a
command are encoded as partially specified terms. However, consider the
command ``\texttt{replace} $x$ \texttt{with} $y^2$''. Until the occurrence
context of the occurrence $x$ it must replace.
The elegant solution we have implemented consists in representing terms
-in a command as function from a context to a partially refined term. The
+in a command as functions from a context to a partially refined term. The
function is obtained by partially applying our disambiguation function to
the content term to be disambiguated. Our solution should be compared with
-the one adopted in the Coq system (where ambiguity is only relative to
-DeBrujin indexes). In Coq variables can be bound either by name or by
-position. This makes more complex every operation over terms (i.e. according
-to our architecture every module that depends on \texttt{cic}). Moreover,
-this solution cannot cope with other forms of ambiguity (as the meaning
-of the $~^2$ exponent in the previous example that depends on the context).
+the one adopted in the Coq system, where ambiguity is only relative to De Brujin
+indexes. In Coq variables can be bound either by name or by position. A term
+occurring in a command has all its variables bound by name to avoid the need of
+a context during disambiguation. Moreover, this makes more complex every
+operation over terms (i.e. according to our architecture every module that
+depends on \texttt{cic}) since the code must deal consistently with both kinds
+of binding. Also, this solution cannot cope with other forms of ambiguity (as
+the context dependent meaning of the exponent in the previous example).
\subsection{Presentation level terms}
against the \texttt{grafite\_parser} \components{}
since they provide an interface to the user. In both cases the formulae
written by the user are parsed using the \texttt{content\_pres} \component{} and
-then disambiguated using the \texttt{cic\_disambiguation} \component.
-However, only \MATITA{} is linked against the \texttt{grafite\_engine} and
-\texttt{tactics} components since \WHELP{} can only execute those ASTs that
-correspond to queries (implemented in the \texttt{whelp} component).
+then disambiguated using the \texttt{cic\_disambiguation} \component. However,
+only \MATITA{} is linked against the \texttt{grafite\_engine} and
+\texttt{tactics} components (summing up to a total of 11'200 lines of code)
+since \WHELP{} can only execute those ASTs that correspond to queries
+(implemented in the \texttt{whelp} component).
The \UWOBO{} Web service wraps the \texttt{content\_pres} \component,
providing a rendering service for the documents in the distributed library.
\section{The interface to the library}
+\label{sec:library}
A proof assistant provides both an interface to interact with its library and
an \emph{authoring} interface to develop new proofs and theories. According
acyclic dependencies among them. This way the library forms a global (and
distributed) hypertext. Several useful operations can be implemented on the
library only, regardless of the scripts. Examples of such operations
-implemented in \MATITA{} are: searching and browing (see Sect.~\ref{sec:indexing});
+implemented in \MATITA{} are: searching and browsing (see Sect.~\ref{sec:indexing});
disambiguation of content level terms (see Sect.~\ref{sec:disambiguation});
automatic proof searching (see Sect.~\ref{sec:automation}).
-A requisite for the previous operations is that the library must
+The key requisite for the previous operations is that the library must
be fully accessible and in a logically consistent state. To preserve
consistency, a concept cannot be altered or removed unless the part of the
library that depends on it is modified accordingly. To allow incremental
database.
For non collaborative development, full versioning can be avoided, but
-invalidation is still required. Since nobody else is relying on your
-development, you are free to change and invalidate part of the library
+invalidation is still required. Since nobody else is relying on the
+user development, the user is free to change and invalidate part of the library
without branching. Invalidation is still necessary to avoid using a
concept that is no longer valid.
So far, in \MATITA{} we address only this non collaborative scenario
group notions together. They also constitute a less fine grained clustering
of notions for invalidation.
-In the following sections we present in more details the functionalities
-of \MATITA{} related to library management and exploitation.
-
-
+In the rest of this section we present in more details the functionalities of
+\MATITA{} related to library management and exploitation.
+Sect.~\ref{sec:authoring} is devoted to the description of the peculiarities of
+the \MATITA{} authoring interface.
\subsection{Indexing and searching}
\label{sec:indexing}
The \texttt{include} statement adds the requirement that the part of the library
defining the notion of natural numbers should be defined before
-processing the what follows. Note indeed that the algorithm presented
+processing what follows. 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.
the alias for \OP{<} 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 (\emph{mono aliases} pass), in case of failure the next pass try again
-the disambiguation forgetting the aliases and using the whole library to
+For this reason we chose to attempt \emph{multiple disambiguation passes}. A
+first pass attempts to disambiguate using the last available disambiguation
+aliases (\emph{mono aliases} pass); in case of failure the next pass tries
+disambiguation again forgetting the aliases and using the whole library to
retrieve interpretation for ambiguous expressions (\emph{library aliases} pass).
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
\subsubsection{Implicit coercions}
-Let's now consider a (rather hypothetical) theorem about derivation:
+Let's now consider a theorem about derivation:
\begin{grafite}
theorem power_deriv:
and suppose there exists a \texttt{R \TEXMACRO{to} nat \TEXMACRO{to} R}
interpretation for \OP{\^}, and a real number interpretation for \OP{*}.
-Mathematichians would write the term that way since it is well known that the
+Mathematichans would write the term that way since it is well known that the
natural number \texttt{n} could be ``injected'' in \IR{} and considered a real
number for the purpose of real multiplication. The refiner of \MATITA{} supports
\emph{implicit coercions} for this reason: given as input the above content
\subsubsection{Disambiguation passes}
According to the criteria described above in \MATITA{} we choose to perform the
-sequence of disambiguation passes depicted in Tab.~\ref{tab:disambpasses}. In
-our experience that choice implements a good trade off among disambiguation time
-and admitted ambiguity in terms input by users.
+sequence of disambiguation passes depicted in Tab.~\ref{tab:disambpasses}. In
+our experience that choice gives reasonable performance and minimize the need of
+user interaction during the disambiguation.
\begin{table}[ht]
\caption{Sequence of disambiguation passes used in \MATITA.\strut}
-\subsection{Compilation and cleaning}
+\subsection{Generation and Invalidation}
\label{sec:libmanagement}
-%
-%goals: consentire sviluppo di una librearia mantenendo integrita' referenziale e usando le teconologie nostre (quindi con metadati, XML, libreria visibile)
-%\subsubsection{Composition}
-%scripts.ma, .moo, XML, metadata
-%\subsubsection{Compilation}
-%analogie con compilazione classica dso.\\
-%granularita' differenti per uso interattivo e non
-%\paragraph{Batch}
-%- granularita' .ma/buri \\
-%-- motivazioni\\
-%- come si calcolano le dipendenze\\
-%- quando la si usa\\
-%- metodi (cc e clean)\\
-%- garanzie
-%\paragraph{Interactive}
-%- granularita' fine\\
-%-- motivazioni
-%\label{sec:libmanagement}
-%consistenza: integrita' referenziale
-%Goals: mantenere consistente la rappresentazione della libreria su
-%memoria persistente consentendo di compilare e pulire le compilation
-%unit (.ma).\\
-%Vincoli: dipendenze oggetti-oggetti e metadati-oggetti\\
-%Due livelli di gestione libreria, uno e' solo in fase interattiva dove la compilazione e' passo passo: \\
-%--- granularita' oggetto per matita interactive\\
-%--- granularita' baseuri (compilation unit) per la libreria\\
-%In entrmbi i casi ora:\\
-%--- matitaSync: add, remove, timetravel(facility-macro tra 2 stati)[obj]\\
-%--- matitaCleanLib: clean\_baseuri (che poi usa matitaSync a sua volta)[comp1]\\
-%Vincoli di add: typecheck ( ==$>$ tutto quello che usa sta in lib)\\
-%Vincoli di remove: \\
-%--- la remove di mSync non li controlla (ma sa cosa cancellare per ogni uri)\\
-%--- la clean\_baseuri calcola le dipendenze con i metadati (o anche i moo direi) e li rispetta\\
-%Undo di matita garantisce la consistenza a patto che l'history che tiene sia ok\\
-%Undo della lib (mClean) garantisce la consistenza (usando moo o Db).\\
-
The aim of this section is to describe the way \MATITA{}
preserves the consistency and the availability of the library
-using the \WHELP{} technology, in response to the user addition or
+using the \WHELP{} technology, in response to the user alteration or
removal of mathematical objects.
-As already sketched in \ref{fully-spec} the output of the
-compilation of a script is split among two storage media, a
+As already sketched in Sec.~\ref{sec:fullyspec} what we generate
+from a script is split among two storage media, a
classical filesystem and a relational database. The former is used to
store the XML encoding of the objects defined in the script, the
disambiguation aliases and the interpretation and notational convention defined,
\subsubsection{Batch vs Interactive}
-\MATITA{} includes an interactive graphical interface and a batch
-compiler (\MATITAC). Only the former is intended to be used directly by the
+\MATITA{} includes an interactive authoring interface and a batch
+``compiler'' (\MATITAC). Only the former is intended to be used directly by the
user, the latter is automatically invoked when a
part of the user development is required (for example issuing an
\texttt{include} command) but not yet compiled.
\end{center}
\end{figure}
-\MATITA{} has a script based user interface (UI) for proof authoring,
-based on the paradigm already exploited by other widespread user
-interfaces for theorem provers like the Proof
-General~\cite{proofgeneral} generic interface. We choosed not to
-build \MATITA{} UI over Proof General for two reasons. First because
-we had the need to integrate our rendering technologies --- mainly
-\GTKMATHVIEW{} --- based on XML markup languages whereas at the time
+The authoring interface of \MATITA{} is very similar to Proof General.
+We chose not to
+build the \MATITA{} UI over Proof General for two reasons. First of all we
+wanted to integrate our XML-based rendering technologies, mainly
+\GTKMATHVIEW{}.
+--- based on XML markup languages whereas at the time
of writing Proof General supports only text based
rendering.\footnote{This may change with the future release of Proof
General based on Eclipse, but is not yet the case.} The second reason
\end{description}
\section{Standard library}
+\label{sec:stdlib}
\MATITA{} is \COQ{} compatible, in the sense that every theorem of \COQ{}
can be read, checked and referenced in further developments.
projects / helm.git / commitdiff