X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fpapers%2Fmatita%2Fmatita2.tex;h=f2e411d4a6b097227b4a315698d3993d97caa0fb;hb=6db12650bceb071d9b5ea8f882613a98bd6df79b;hp=5e5bb5bef6e84b1e1c8f8d36ec945e76a01c2071;hpb=f271439ffbe4b5a689061bd4744c9b9294f734e1;p=helm.git diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex index 5e5bb5bef..f2e411d4a 100644 --- a/helm/papers/matita/matita2.tex +++ b/helm/papers/matita/matita2.tex @@ -1,4 +1,4 @@ -\documentclass{kluwer} +\documentclass[]{kluwer} \usepackage{color} \usepackage{graphicx} % \usepackage{amssymb,amsmath} @@ -13,9 +13,13 @@ %\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}} +\newcommand{\GDOME}{Gdome} \newcommand{\HELM}{Helm} \newcommand{\HINT}{\textsc{Hint}} \newcommand{\IN}{\ensuremath{\dN}} @@ -52,6 +56,7 @@ \definecolor{gray}{gray}{0.85} % 1 -> white; 0 -> black \newcommand{\NT}[1]{\langle\mathit{#1}\rangle} \newcommand{\URI}[1]{\texttt{#1}} +\newcommand{\OP}[1]{``\texttt{#1}''} %{\end{SaveVerbatim}\setlength{\fboxrule}{.5mm}\setlength{\fboxsep}{2mm}% \newenvironment{grafite}{\VerbatimEnvironment @@ -70,6 +75,9 @@ \newcommand{\NOTE}[1]{\ednote{#1}{foo}} \newcommand{\TODO}[1]{\textbf{TODO: #1}} +\newcounter{pass} +\newcommand{\PASS}{\stepcounter{pass}\arabic{pass}} + \newsavebox{\tmpxyz} \newcommand{\sequent}[2]{ \savebox{\tmpxyz}[0.9\linewidth]{ @@ -115,37 +123,181 @@ Digital Libraries} \end{opening} + +\section{Introduction} +\label{sec:intro} +\MATITA{} is the Proof Assistant under development by the \HELM{} team +\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 +features. + +\subsection{Historical Perspective} +The origins of \MATITA{} go 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~\cite{CoqManual} 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{}\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: +\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\cite{content-centric} 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\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 +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 software libraries, collectively called the \HELM{} libraries. +At the end of the \MOWGLI{} project we already disposed of the following +tools and software libraries: +\begin{itemize} +\item XML specifications for the Calculus of Inductive Constructions, +with libraries for parsing and saving mathematical objects in such a format +\cite{exportation-module}; +\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 \cite{remathematization}; +\item an innovative, MathML-compliant rendering widget for the GTK +graphical environment\cite{padovani}, 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, developing our own proof assistant was not +too far away: 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 +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 +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 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 +%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} + \label{fig:libraries} \end{center} - \label{fig:libraries} \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. +\section{Architecture} +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. \MATITA, our most complex -application, depends on every library. +depend on a restricted set of \components{}. -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 @@ -161,37 +313,37 @@ HELM and MoWGLI projects and already described elsewhere. In particular: 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 -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 -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 @@ -203,10 +355,10 @@ at the content level; terms at the presentation level. 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 @@ -214,40 +366,51 @@ at the content level; terms at the presentation level. 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 HTTP interface - to the \texttt{cic\_proof\_checking} library. + The Proof Checker is the Web service that provides an interface + 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. + + According to our vision, the library is developed collaboratively so that + changing or removing a notion can invalidate other notions in the library. + Moreover, changing or removing a notion requires a corresponding change + in the metadata database. The \texttt{library} \component{} is responsible + of preserving the coherence of the library and the database. For instance, + when a notion is removed, all the notions that depend on it and their + metadata are removed from the library. This aspect will be better detailed + in Sect.~\ref{decompilazione}. + \subsection{Partially specified terms} \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 @@ -265,12 +428,12 @@ 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. -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 @@ -279,8 +442,16 @@ 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. +\texttt{tactics} \component. It is heavily based on the refinement and +unification procedures of the \texttt{cic\_unification} \component. + +The \texttt{grafite} \component{} defines the abstract syntax tree (AST) for the +commands of the \MATITA{} proof assistant. Most of the commands are tactics. +Other commands are used to give definitions and axioms or to state theorems +and lemmas. The \texttt{grafite\_engine} \component{} is the core of \MATITA{}. +It implements the semantics of each command in the grafite AST as a function +from status to status. It implements also an undo function to go back to +previous statuses. \TODO{parlare di disambiguazione lazy \& co?} As fully specified terms, partially specified terms are not well suited for user consumption since their syntax is not extendible and it is not @@ -288,7 +459,9 @@ possible to adopt the usual mathematical notation. However they are already 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 @@ -296,7 +469,7 @@ ambiguity that the mathematical language provides. 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. @@ -314,7 +487,7 @@ practice to stick to the usual imprecise mathematical ontology. In the Mathematical Knowledge Management community this imprecise language is called the \emph{content level} representation of expressions. -In \MATITA{} we provide two translations from partially specified 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 specified terms since a fully specified term is a special case of partially specified term where no metavariable or implicit term occurs. @@ -323,12 +496,13 @@ 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 proof steps that can easily be rendered in natural language. The latters -are translated to MathML Content formulae. MathML Content is a W3C standard +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\_content} library. Its input are \emph{annotated partially -specified terms}. Annotated partially specified terms are maximally unshared +\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 proofs and terms that represent expressions. Part of it is also stored at the @@ -339,22 +513,24 @@ 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{} unshares and annotates terms. It is used +by the \texttt{library} \component{} since fully specified terms are stored +in the library in their annotated form. We do not provide yet a reverse translation from content level proofs to -partially specified terms. But in \texttt{disambiguation} we do provide +partially specified terms. But in \texttt{cic\_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 +\texttt{cic\_disambiguation} \component{} implements 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 refined term +interpretations. An interpretation is correct if the partially specified term obtained using the interpretation is refinable. -\subsection{Terms at the presentation level} +\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 @@ -368,31 +544,35 @@ 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 that is an XML dialect standardized by the W3C. To visually +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 +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 -utility functions to build a GDOM MathML+BoxML tree from our presentation -level terms. GDOM MathML+BoxML trees can be rendered by the GtkMathView -widget developed by Luca Padovani \cite{gtkmathview}. The widget is +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 +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 -refined terms they correspond to. Highlight of formulae in the widget is +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 level term. Once the rendering of a lower level term is +correspond to a lower level term, that is a content term or a partially or +fully specified 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 enriched term), +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). @@ -400,56 +580,407 @@ 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 -precedence level of every operator is he using. In prctice this limitation +precedence level of every operator he is using. In practice 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). +Both the direct and reverse translation from presentation to content level +terms are parameterized over the user provided mathematical notation. +The \texttt{lexicon} \component{} is responsible of managing the lexicon, +that is the set of active notations. It defines an abstract syntax tree +of commands to declare and activate new notations and it implements the +semantics of these commands. It also implements undoing of the semantic +actions. Among the commands there are hints to the +disambiguation algorithm that are used to control and speed up disambiguation. +These mechanisms will be further discussed in Sect.~\ref{disambiguazione}. + +Finally, the \texttt{grafite\_parser} \component{} implements a parser for +the concrete syntax of the commands of \MATITA. The parser process a stream +of characters and returns a stream of abstract syntax trees (the ones +defined by the \texttt{grafite} component and whose semantics is given +by \texttt{grafite\_engine}). When the parser meets a command that changes +the lexicon, it invokes the \texttt{lexicon} \component{} to immediately +process the command. When the parser needs to parse a term at the presentation +level, it invokes the already described parser for terms contained in +\texttt{content\_pres}. + 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{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} 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. +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). -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 it to the presentation level passing through the content level. Finally -it returns the result document to be rendered by the user's browser. +it returns the result document to be rendered by the user's +browser.\footnote{\TODO{manca la passata verso HTML}} -\hrule -At the bottom of the DAG we have a few libraries (\texttt{extlib}, -\texttt{xml} and the \texttt{registry}) that provide a core of -useful functions used everywhere else. In particular, the \texttt{xml} library -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 -data structures (\texttt{extlib}) and central storage for configuration options -(the \texttt{registry}). +The \components{} not yet described (\texttt{extlib}, \texttt{xml}, +\texttt{logger}, \texttt{registry} and \texttt{utf8\_macros}) are +minor \components{} that provide a core of useful functions and basic +services missing from the standard library of the programming language. +In particular, the \texttt{xml} \component{} is used +to easily represent, parse and pretty-print XML files. + +\section{Using \MATITA (boh \ldots cambiare titolo)} + +\begin{figure}[t] + \begin{center} +% \includegraphics[width=0.9\textwidth]{a.eps} + \caption{\MATITA{} screenshot} + \label{fig:screenshot} + \end{center} +\end{figure} + +\MATITA{} has a script based user interface. As can be seen in Fig.~... it is +split in two main windows: on the left a textual widget is used to edit the +script, on the right the list of open goal is shown using a MathML rendering +widget. A distinguished part of the script (shaded in the screenshot) represent +the commands already executed and can't be edited without undoing them. The +remaining part can be freely edited and commands from that part can be executed +moving down the execution point. An additional window --- the ``cicBrowser'' --- +can be used to browse the library, including the proof being developed, and +enable content based search on it. In the cicBrowser proofs are rendered in +natural language, automatically generated from the low-level $\lambda$-terms +using techniques inspired by \cite{natural,YANNTHESIS}. + +In the \MATITA{} philosophy the script is not relevant \emph{per se}, but is +only seen as a convenient way to create mathematical objects. The universe of +all these objects makes up the \HELM{} library, which is always completely +visible to the user. The mathematical library is thus conceived as a global +hypertext, where objects may freely reference each other. It is a duty of +the system to guide the user through the relevant parts of the library. + +This methodological assumption has many important consequences +which will be discussed in the next section. + +%on one side +%it requires functionalities for the overall management of the library, +%%%%%comprising efficient indexing techniques to retrieve and filter the +%information; +%on the other it introduces overloading in the use of +%identifiers and mathematical notation, requiring sophisticated disambiguation +%techniques for interpreting the user inputs. +%In the next two sections we shall separately discuss the two previous +%points. + +%In order to maximize accessibility mathematical objects are encoded in XML. (As%discussed in the introduction,) the modular architecture of \MATITA{} is +%organized in components which work on data in this format. For instance the +%rendering engine, which transform $\lambda$-terms encoded as XML document to +%MathML Presentation documents, can be used apart from \MATITA{} to print ... +%FINIRE + +A final section is devoted to some innovative aspects +of the authoring system, such as a step by step tactical execution, +content selection and copy-paste. + +\section{Library Management} + +\subsection{Indexing and searching} + +\subsection{Developments} + +\subsection{Automation} + +\subsection{Matita's naming convention} +A minor but not entirely negligible aspect of Matita is that of +adopting a (semi)-rigid naming convention for identifiers, derived by +our studies about metadata for statements. +The convention is only applied to identifiers for theorems +(not definitions), and relates the name of a proof to its statement. +The basic rules are the following: +\begin{itemize} +\item each identifier is composed by an ordered list of (short) +names occurring in a left to right traversal of the statement; +\item all identifiers should (but this is not strictly compulsory) +separated by an underscore, +\item identifiers in two different hypothesis, or in an hypothesis +and in the conlcusion must be separated by the string ``\verb+_to_+''; +\item the identifier may be followed by a numerical suffix, or a +single or duoble apostrophe. + +\end{itemize} +Take for instance the theorem +\[\forall n:nat. n = plus \; n\; O\] +Possible legal names are: \verb+plus_n_O+, \verb+plus_O+, +\verb+eq_n_plus_n_O+ and so on. +Similarly, consider the theorem +\[\forall n,m:nat. n