%\parpic(0cm,0cm)(#2,#3)[l]{\includegraphics[width=#1]{whelp-bw}}
%}
+\newcommand{\component}{component}
+\newcommand{\components}{components}
+
\newcommand{\AUTO}{\textsc{Auto}}
\newcommand{\COQ}{Coq}
\newcommand{\ELIM}{\textsc{Elim}}
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.
+989 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
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
+simple as possible is thus crucial to foster 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
\end{figure}
\section{Overview of the Architecture}
-Fig.~\ref{fig:libraries} shows the architecture of the \emph{libraries} (circle nodes)
-and \emph{applications} (squared nodes) developed in the HELM project.
+Fig.~\ref{fig:libraries} shows the architecture of the \emph{\components}
+(circle nodes) and \emph{applications} (squared nodes) developed in the HELM
+project.
-Applications and libraries depend over other libraries forming a
-directed acyclic graph (DAG). Each library can be decomposed in
+Applications and \components{} depend over other \components{} forming a
+directed acyclic graph (DAG). Each \component{} can be decomposed in
a a set of \emph{modules} also forming a DAG.
-Modules and libraries provide coherent sets of functionalities
+Modules and \components{} provide coherent sets of functionalities
at different scales. Applications that require only a few functionalities
-depend on a restricted set of libraries.
+depend on a restricted set of \components{}.
Only the proof assistant \MATITA{} and the \WHELP{} search engine are
applications meant to be used directly by the user. All the other applications
The dependency analyzer has been described in~\cite{zack-master}.
\end{itemize}
-The dependency of a library or application over another library can
-be satisfied by linking the library in the same executable.
-For those libraries whose functionalities are also provided by the
+The dependency of a \component{} or application over another \component{} can
+be satisfied by linking the \component{} in the same executable.
+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 \texttt{getter} library that allows the library
-to be used as a Web service. \MATITA{} can directly link the code of the
-\texttt{getter} library, or it can use a stub library with the same API
-that forwards every request to the Getter.
+is just a wrapper to the \texttt{getter} \component{} that allows the
+\component{} to be used as a Web service. \MATITA{} can directly link the code
+of the \texttt{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
-library, we can focus on the representation of the mathematical information.
+\component, 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
extendible mathematical notation. They are not meant for direct user
consumption.
- The \texttt{cic} library defines the data type that represents CIC terms
+ The \texttt{cic} \component{} defines the data type that represents CIC terms
and provides a parser for terms stored in an XML format.
- The most important library that deals with fully specified terms is
+ The most important \component{} that deals with fully specified terms is
\texttt{cic\_proof\_checking}. It implements the procedure that verifies
if a fully specified term is well-typed. It also implements the
\emph{conversion} judgement that verifies if two given terms are
Terms may reference other mathematical notions in the library.
One commitment of our project is that the library should be physically
- distributed. The \texttt{getter} library manages the distribution,
+ distributed. The \texttt{getter} \component{} manages the distribution,
providing a mapping from logical names (URIs) to the physical location
- of a notion (an URL). The \texttt{urimanager} library provides the URI
+ of a notion (an URL). The \texttt{urimanager} \component{} provides the URI
data type and several utility functions over URIs. The
- \texttt{cic\_proof\_checking} library calls the \texttt{getter} library
- every time it needs to retrieve the definition of a mathematical notion
- referenced by a term that is being type-checked.
+ \texttt{cic\_proof\_checking} \component{} calls the \texttt{getter}
+ \component{} 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 interface
- to the \texttt{cic\_proof\_checking} library.
+ to the \texttt{cic\_proof\_checking} \component.
We use metadata and a sort of crawler to index the mathematical notions
in the distributed library. We are interested in retrieving a notion
by matching, instantiation or generalization of a user or system provided
mathematical expression. Thus we need to collect metadata over the fully
specified terms and to store the metadata in some kind of (relational)
- database for later usage. The \texttt{hmysql} library provides a simplified
+ database for later usage. The \texttt{hmysql} \component{} provides
+ a simplified
interface to a (possibly remote) MySql database system used to store the
- metadata. The \texttt{metadata} library defines the data type of the metadata
+ metadata. The \texttt{metadata} \component{} defines the data type of the
+ metadata
we are collecting and the functions that extracts the metadata from the
mathematical notions (the main functionality of the crawler).
- The \texttt{whelp} library implements a search engine that performs
+ The \texttt{whelp} \component{} implements a search engine that performs
approximated queries by matching/instantiation/generalization. The queries
operate only on the metadata and do not involve any actual matching
(that will be described later on and that is implemented in the
- \texttt{cic\_unification} library). Not performing any actual matching
+ \texttt{cic\_unification} \component). Not performing any actual matching
the query only returns a complete and hopefully small set of matching
candidates. The process that has issued the query is responsible of
actually retrieving from the distributed library the candidates to prune
out false matches if interested in doing so.
The Whelp search engine is the Web service that provides an interface to
- the \texttt{whelp} library.
+ the \texttt{whelp} \component.
\subsection{Partially specified terms}
\emph{Partially specified terms} are CIC terms where subterms can be omitted.
a type-inference procedure that can instantiate implicit terms and
metavariables and that can introduce \emph{implicit coercions} to make a
partially specified term be well-typed. The refiner of \MATITA{} is implemented
-in the \texttt{cic\_unification} library. As the type checker is based on
+in the \texttt{cic\_unification} \component. As the type checker is based on
the conversion check, the refiner is based on \emph{unification} that is
a procedure that makes two partially specified term convertible by instantiating
as few as possible metavariables that occur in them.
\emph{Tactics} are the procedures that the user can apply to progress in the
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. \TODO{citare paramodulation
+\texttt{tactics} \component. It is heavily based on the refinement and unification
+procedures of the \texttt{cic\_unification} \component. \TODO{citare paramodulation
da qualche part o toglierla dal grafo}
As fully specified terms, partially specified terms are not well suited
for the representation of content level expressions in an XML extensible format.
The translation to content level is implemented in the
-\texttt{acic\_content} library. Its input are \emph{annotated partially
+\texttt{acic\_content} \component. 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
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.
+The \texttt{cic\_acic} \component 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 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
+\texttt{disambiguation} \component{} 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
many equivalent specifications exist and we have adopted our own, called
BoxML.
-The \texttt{content\_pres} library contains the implementation of the
+The \texttt{content\_pres} \component{} 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
+the \component. However, in the \texttt{hgdome} \component{} 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
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
+parsing tool 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
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
+against the \texttt{cic\_disambiguation} and \texttt{content\_pres} \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} library and
-then disambiguated using the \texttt{cic\_disambiguation} library.
+written by the user are parsed using the \texttt{content\_pres} \component{} and
+then disambiguated using the \texttt{cic\_disambiguation} \component.
-The \UWOBO{} Web service wraps the \texttt{content\_pres} library,
+The \UWOBO{} Web service wraps the \texttt{content\_pres} \component,
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
\hrule
-At the bottom of the DAG we have a few libraries (\texttt{extlib},
+At the bottom of the DAG we have a few \components{} (\texttt{extlib},
\texttt{xml} and the \texttt{registry}) that provide a core of
-useful functions used everywhere else. In particular, the \texttt{xml} library
+useful functions used everywhere else. In particular, the \texttt{xml} \component{}
to easily represent, parse and pretty-print XML files is a central component
since in HELM every piece of information is stored in \ldots. [FINIRE]
-The other basic libraries provide often needed operations over generic
+The other basic \components{} provide often needed operations over generic
data structures (\texttt{extlib}) and central storage for configuration options
(the \texttt{registry}).
projects / helm.git / blobdiff