From 0934df282c5a661213df1962e678d9b9b95fee50 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 18 Jan 2006 14:09:13 +0000 Subject: [PATCH] library ==> component --- helm/papers/matita/matita2.tex | 96 ++++++++++++++++++---------------- 1 file changed, 51 insertions(+), 45 deletions(-) diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex index 33365877c..7c8e2fa45 100644 --- a/helm/papers/matita/matita2.tex +++ b/helm/papers/matita/matita2.tex @@ -13,6 +13,9 @@ %\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}} @@ -226,7 +229,7 @@ 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. +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 @@ -255,7 +258,7 @@ 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 +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 @@ -271,16 +274,17 @@ allow other developers to quickly understand our code and contribute. \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 @@ -320,18 +324,18 @@ elsewhere. In particular: 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 @@ -350,10 +354,10 @@ content level terms; presentation level terms. 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 @@ -361,39 +365,41 @@ content level terms; presentation level terms. 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. @@ -412,7 +418,7 @@ partially specified term should be \emph{refinable}. A \emph{refiner} is 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. @@ -426,8 +432,8 @@ prove. \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 @@ -478,7 +484,7 @@ standard 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 @@ -490,7 +496,7 @@ 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. +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 @@ -499,7 +505,7 @@ 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 +\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 @@ -526,10 +532,10 @@ 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 +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 @@ -553,7 +559,7 @@ 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 +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 @@ -564,12 +570,12 @@ 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 +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 @@ -579,12 +585,12 @@ browser.\footnote{\TODO{manca la passata verso HTML}} \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}). -- 2.39.2