X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fpapers%2Fmatita%2Fmatita2.tex;h=88f664c2dcbf911e5acffd7fa2d8841a184f4077;hb=57d038849d866853795522e360723a881c2d4831;hp=9a9870fcc12846948cc3324d4179d651a555d57d;hpb=be5869cd0bbe16c8a67827723c97d2d4fce4c0bc;p=helm.git diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex index 9a9870fcc..88f664c2d 100644 --- a/helm/papers/matita/matita2.tex +++ b/helm/papers/matita/matita2.tex @@ -1,26 +1,22 @@ -\documentclass[draft]{kluwer} +\documentclass[]{kluwer} \usepackage{color} \usepackage{graphicx} -% \usepackage{amssymb,amsmath} \usepackage{hyperref} -% \usepackage{picins} \usepackage{color} \usepackage{fancyvrb} \usepackage[show]{ed} -\definecolor{gray}{gray}{0.85} -%\newcommand{\logo}[3]{ -%\parpic(0cm,0cm)(#2,#3)[l]{\includegraphics[width=#1]{whelp-bw}} -%} - \newcommand{\component}{component} \newcommand{\components}{components} \newcommand{\AUTO}{\textsc{Auto}} +\newcommand{\BOXML}{BoxML} \newcommand{\COQ}{Coq} \newcommand{\COQIDE}{CoqIde} \newcommand{\ELIM}{\textsc{Elim}} \newcommand{\GDOME}{Gdome} +\newcommand{\GTK}{GTK+} +\newcommand{\GTKMATHVIEW}{\textsc{GtkMathView}} \newcommand{\HELM}{Helm} \newcommand{\HINT}{\textsc{Hint}} \newcommand{\IN}{\ensuremath{\dN}} @@ -28,23 +24,27 @@ \newcommand{\IR}{\ensuremath{\dR}} \newcommand{\IZ}{\ensuremath{\dZ}} \newcommand{\LIBXSLT}{LibXSLT} +\newcommand{\LEGO}{Lego} \newcommand{\LOCATE}{\textsc{Locate}} \newcommand{\MATCH}{\textsc{Match}} +\newcommand{\MATHML}{MathML} \newcommand{\MATITA}{Matita} \newcommand{\MATITAC}{\texttt{matitac}} \newcommand{\MATITADEP}{\texttt{matitadep}} -\newcommand{\METAHEADING}{Symbol & Position \\ \hline\hline} \newcommand{\MOWGLI}{MoWGLI} +\newcommand{\MOWGLIIST}{IST-2001-33562} \newcommand{\NAT}{\ensuremath{\mathit{nat}}} \newcommand{\NATIND}{\mathit{nat\_ind}} \newcommand{\NUPRL}{NuPRL} \newcommand{\OCAML}{OCaml} \newcommand{\PROP}{\mathit{Prop}} \newcommand{\REF}[3]{\ensuremath{\mathit{Ref}_{#1}(#2,#3)}} +\newcommand{\REWRITEHINT}{\textsc{RewriteHint}} \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{;}}}} \newcommand{\BRANCH}{\ensuremath{\mbox{\textbf{[}}}} @@ -56,12 +56,15 @@ \newcommand{\SKIP}{\MATHTT{skip}} \newcommand{\TACTIC}[1]{\ensuremath{\mathtt{tactic}~#1}} -\definecolor{gray}{gray}{0.85} % 1 -> white; 0 -> black -\newcommand{\NT}[1]{\langle\mathit{#1}\rangle} +\newcommand{\NT}[1]{\ensuremath{\langle\mathit{#1}\rangle}} \newcommand{\URI}[1]{\texttt{#1}} \newcommand{\OP}[1]{``\texttt{#1}''} +\newcommand{\FILE}[1]{\texttt{#1}} +\newcommand{\TAC}[1]{\texttt{#1}} +\newcommand{\TODO}[1]{\textbf{TODO: #1}} + +\definecolor{gray}{gray}{0.85} % 1 -> white; 0 -> black -%{\end{SaveVerbatim}\setlength{\fboxrule}{.5mm}\setlength{\fboxsep}{2mm}% \newenvironment{grafite}{\VerbatimEnvironment \begin{SaveVerbatim}{boxtmp}}% {\end{SaveVerbatim}\setlength{\fboxsep}{3mm}% @@ -69,15 +72,6 @@ \fcolorbox{black}{gray}{\BUseVerbatim[boxwidth=0.9\linewidth]{boxtmp}} \end{center}} -\newcounter{example} -\newenvironment{example}{\stepcounter{example}\vspace{0.5em}\noindent\emph{Example} \arabic{example}.} - {} -\newcommand{\ASSIGNEDTO}[1]{\textbf{Assigned to:} #1} -\newcommand{\FILE}[1]{\texttt{#1}} -% \newcommand{\NOTE}[1]{\ifodd \arabic{page} \else \hspace{-2cm}\fi\ednote{#1}} -\newcommand{\NOTE}[1]{\ednote{#1}{foo}} -\newcommand{\TODO}[1]{\textbf{TODO: #1}} - \newcounter{pass} \newcommand{\PASS}{\stepcounter{pass}\arabic{pass}} @@ -93,126 +87,163 @@ \fcolorbox{black}{gray}{\usebox{\tmpxyz}} \end{center}} -\bibliographystyle{plain} +\bibliographystyle{klunum} \begin{document} \begin{opening} - \title{The \MATITA{} Proof Assistant} -\author{Andrea \surname{Asperti} \email{asperti@cs.unibo.it}} -\author{Claudio \surname{Sacerdoti Coen} \email{sacerdot@cs.unibo.it}} -\author{Enrico \surname{Tassi} \email{tassi@cs.unibo.it}} -\author{Stefano \surname{Zacchiroli} \email{zacchiro@cs.unibo.it}} -\institute{Department of Computer Science, University of Bologna\\ - Mura Anteo Zamboni, 7 --- 40127 Bologna, ITALY} + \author{Andrea \surname{Asperti} \email{asperti@cs.unibo.it}} + \author{Claudio \surname{Sacerdoti Coen} \email{sacerdot@cs.unibo.it}} + \author{Enrico \surname{Tassi} \email{tassi@cs.unibo.it}} + \author{Stefano \surname{Zacchiroli} \email{zacchiro@cs.unibo.it}} -\runningtitle{The \MATITA{} proof assistant} -\runningauthor{Asperti, Sacerdoti Coen, Tassi, Zacchiroli} - -% \date{data} + \institute{Department of Computer Science, University of Bologna\\ + Mura Anteo Zamboni, 7 --- 40127 Bologna, ITALY} -\begin{motto} -``We are nearly bug-free'' -- \emph{CSC, Oct 2005} -\end{motto} + \runningtitle{The \MATITA{} proof assistant} + \runningauthor{Asperti, Sacerdoti Coen, Tassi, Zacchiroli} -\begin{abstract} - abstract qui -\end{abstract} + \begin{motto} + ``We are nearly bug-free'' -- \emph{CSC, Oct 2005} + \end{motto} -\keywords{Proof Assistant, Mathematical Knowledge Management, XML, Authoring, -Digital Libraries} + \begin{abstract} + \TODO{scrivere abstract} + \end{abstract} + \keywords{Proof Assistant, Mathematical Knowledge Management, XML, Authoring, + Digital Libraries} \end{opening} +% toc & co: to be removed in the final paper version \tableofcontents +\listoffigures +\listoftables \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 + +\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. This paper describes the overall architecture of +the system, focusing on its most distinctive and innovative features. -\subsection{Historical Perspective} +\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 +interested in developing tools and techniques to enhance the accessibility +via Web of libraries of formalized mathematics. Due to its dimension, the +library of the \COQ~\cite{CoqManual} proof assistant (of the order of +35'000 theorems) +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 +European project \MOWGLIIST{} \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} +\begin{enumerate} + + \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 that 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 built; + + \item developing indexing and searching techniques supporting semantic + queries to the library; + + \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.} + +\end{enumerate} 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 +as Web services. The user can 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. +Web services and other tools have been implemented as front-ends +to a set of software components, collectively called the \HELM{} components. At the end of the \MOWGLI{} project we already disposed of the following -tools and software libraries: +tools and software components: \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. + + \item XML specifications for the Calculus of Inductive Constructions, + with components for parsing and saving mathematical objects in such a + format~\cite{exportation-module}; + + \item metadata specifications with components for indexing and querying the + XML knowledge base; + + \item a proof checker (i.e. the \emph{kernel} of a proof assistant), + implemented to check that we exported from the \COQ{} library all the + logically relevant content; + + \item a sophisticated term parser (used by the search engine), able to deal + with potentially ambiguous and incomplete information, typical of the + mathematical notation~\cite{disambiguation}; + + \item a \emph{refiner} component, 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~\cite{padovani} + for the \GTK{} graphical environment,\footnote{\url{http://www.gtk.org/}} + supporting high-quality bidimensional + rendering, and semantic selection, i.e. the possibility to select semantically + meaningful rendering expressions, and to paste 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{The system} + +\MATITA{} is a proof assistant (also called interactive theorem prover). +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~\cite{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~\cite{lcf}. \COQ, \NUPRL, PVS, Isabelle are all examples of +others systems +whose proof language is procedural. Traditionally, in a procedural system +the user interacts only with the \emph{script}, while proof terms are internal +records kept by the system. On the contrary, in \MATITA{} proof terms are +praised as declarative versions of the proof. Playing that role, they are the +primary mean of communication of proofs (once rendered to natural language +for human audiences). + +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{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. +The authoring interface of \MATITA{} is a clone of the Proof General interface. +On the contrary, the interface to interact with the library is rather +innovative and directly inspired by the Web interfaces to our Web servers. + +\MATITA{} is backward compatible with the XML library of proof objects exported +from \COQ{}, but, in order to test the actual usability of the system, we are +also developing a new library of basic results from scratch. \subsection{Relationship with \COQ{}} @@ -220,49 +251,50 @@ 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. +Calculus of (Co)Inductive Constructions), the same implementation +language (\OCAML\footnote{\url{http://caml.inria.fr/}}), +and the same (procedural, script based) authoring philosophy. +However, the analogy essentially stops here and no code is shared +between the two systems. -In a sense; we like to think of \MATITA{} as the way \COQ{} would +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). +we could reduce our code even further in a 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 +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 +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. 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 +historically. \COQ{}\cite{CoqArt} is a quite old +system whose development started 20 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 +unification), changing these functionalities maintaining backward compatibility is very difficult. Finally, the code of \COQ{} has been greatly optimized -over the years; optimization reduces maintenability and rises the complexity +over the years; optimization reduces maintainability 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. +scratch, we have designed in advance the architecture and we have split +the code in coherent minimally coupled components. 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 +extensions. Keeping the single components 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. @@ -270,91 +302,101 @@ allow other developers to quickly understand our code and contribute. %be able to contribute to \COQ{}'s code is quite steep and requires direct %and frequent interactions with \COQ{} developers. -\begin{figure}[t] +\section{Architecture} +\label{architettura} + +\begin{figure}[!ht] \begin{center} - \includegraphics[width=0.9\textwidth]{librariesCluster.ps} - \caption{\MATITA{} libraries} + \includegraphics[width=0.9\textwidth,height=0.8\textheight]{pics/libraries-clusters} + \caption[\MATITA{} components and related applications]{\MATITA{} + components and related applications, with thousands of line of + codes (klocs)\strut} \label{fig:libraries} \end{center} \end{figure} -\section{Architecture} -\label{architettura} Fig.~\ref{fig:libraries} shows the architecture of the \emph{\components} -(circle nodes) and \emph{applications} (squared nodes) developed in the HELM -project. +(circle nodes) and \emph{applications} (squared nodes) developed in the +\HELM{} project. Each node is annotated with the number of lines of +source code (comprising comments). -Applications and \components{} depend over other \components{} forming a +Applications and \components{} depend on other \components{} forming a directed acyclic graph (DAG). Each \component{} can be decomposed in -a a set of \emph{modules} also forming a DAG. +a set of \emph{modules} also forming a DAG. Modules and \components{} provide coherent sets of functionalities at different scales. Applications that require only a few functionalities -depend on a restricted set of \components{}. +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 -are Web services developed in the HELM and MoWGLI projects and already described -elsewhere. In particular: +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{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 - for a theorem that generalize or instantiate a given formula, or that - can be immediately applied to prove a given goal. The output of Whelp is - an XML document that lists the URIs of a complete set of candidates that - are likely to satisfy the given query. The set is complete in the sense - that no notion that actually satisfies the query is thrown away. However, - the query is only approssimated in the sense that false matches can be - returned. Whelp has been described in~\cite{whelp}. - \item \emph{Uwobo} is a Web service that, given the URI of a mathematical - notion in the distributed library, renders it according to the user provided - 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{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{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{zack-master}. + + \item The \emph{\GETTER}~\cite{zack-master} 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. + + \item \emph{\WHELP}~\cite{whelp} is a search engine to index and + locate mathematical concepts (axioms, theorems, definitions) in the + logical library managed by the Getter. Typical examples of + \WHELP{} queries are those that search for a theorem that generalize or + instantiate a given formula, or that can be immediately applied to + prove a given goal. The output of Whelp is an XML document that lists + the URIs of a complete set of candidates that are likely to satisfy + the given query. The set is complete in the sense that no concept that + actually satisfies the query is thrown away. However, the query is + only approximated in the sense that false matches can be returned. + + \item \emph{\UWOBO}~\cite{zack-master} is a Web service that, given the + URI of a mathematical concept in the distributed library, renders it + according to the user provided two dimensional mathematical notation. + \UWOBO{} may also inline the rendering of mathematical concepts into + arbitrary documents before returning them. The Getter is used by + \UWOBO{} to retrieve the document to be rendered. + + \item The \emph{Proof Checker}~\cite{zack-master} is a Web service + that, given the URI of a concept in the distributed library, checks its + correctness. Since the concept is likely to depend in an acyclic way + on other concepts, the proof checker is also responsible of building + in a top-down way the DAG of all dependencies, checking in turn every + concept for correctness. + + \item The \emph{Dependency Analyzer}~\cite{zack-master} is a Web + service that can produce a textual or graphical representation of the + dependencies of a concept. + \end{itemize} 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 \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 -API that forwards every request to the Getter. +forwards the request to a remote Web service. For instance, the +\GETTER{} application is just a wrapper to the \GETTER{} \component{} +that allows it 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 API that forwards every request to the Web service. To better understand the architecture of \MATITA{} and the role of each -\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 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. +\component, we can focus on the representation of the mathematical +information. In CIC terms are used to represent mathematical formulae, +types and proofs. \MATITA{} is able to handle terms at 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} -\label{fully-spec} +\label{sec:fullyintro} + \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 + The mathematical concepts (axioms, definitions, theorems) that are stored in our mathematical library are fully specified and well-typed terms. Fully specified terms are extremely verbose (to make type-checking decidable). Their syntax is fixed and does not resemble the usual @@ -362,7 +404,7 @@ content level terms; presentation level terms. consumption. The \texttt{cic} \component{} defines the data type that represents CIC terms - and provides a parser for terms stored in an XML format. + and provides a parser for terms stored in XML format. The most important \component{} that deals with fully specified terms is \texttt{cic\_proof\_checking}. It implements the procedure that verifies @@ -370,74 +412,78 @@ content level terms; presentation level terms. \emph{conversion} judgement that verifies if two given terms are computationally equivalent (i.e. they share the same normal form). - Terms may reference other mathematical notions in the library. + Terms may reference other mathematical concepts 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 + of a concept (an URL). The \texttt{urimanager} \component{} provides the URI data type and several utility functions over URIs. The - \texttt{cic\_proof\_checking} \component{} calls the \GETTER + \texttt{cic\_proof\_checking} \component{} calls the \GETTER{} \component{} every time it needs to retrieve the definition of a mathematical - notion referenced by a term that is being type-checked. + concept referenced by a term that is being type-checked. - The Proof Checker is the Web service that provides an interface + The Proof Checker application 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 + We use metadata and a sort of crawler to index the mathematical concepts + in the distributed library. We are interested in retrieving a concept by matching, instantiation or generalization of a user or system provided - mathematical expression. Thus we need to collect metadata over the fully + mathematical formula. 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} \component{} provides a simplified - interface to a (possibly remote) MySql database system used to store the - metadata. The \texttt{metadata} \component{} defines the data type of the - metadata + interface to a (possibly remote) MySQL\footnote{\url{http://www.mysql.com/}} + database system used to store the 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). + mathematical concepts (the main functionality of the crawler). 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} \component). Not performing any actual matching - the query only returns a complete and hopefully small set of matching + (see the \texttt{cic\_unification} \component in + Sect.~\ref{sec:partiallyintro}). Not performing any actual matching + a 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 \WHELP{} application is the Web service that provides an interface to 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 + changing or removing a concept can invalidate other concepts in the library. + Moreover, changing or removing a concept 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 + when a concept is removed, all the concepts that depend on it and their metadata are removed from the library. This aspect will be better detailed in Sect.~\ref{sec:libmanagement}. \subsection{Partially specified terms} +\label{sec:partiallyintro} + \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 linearly. The latters may occur multiple times and are called -\emph{metavariables}. An \emph{explicit substitution} is applied to each -occurrence of a metavariable. A metavariable stand for a term whose type is +\emph{metavariables}~\cite{geuvers-jojgov,munoz}. +An \emph{explicit substitution} is applied to each +occurrence of a metavariable. A metavariable stands for a term whose type is given by the conclusion of the sequent. The term must be closed in the context that is given by the ordered list of hypotheses of the sequent. The explicit substitution instantiates every hypothesis with an actual -value for the term bound by the hypothesis. +value for the variable bound by the hypothesis. Partially specified terms are not required to be well-typed. However a 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 +metavariables and that can introduce +\emph{implicit coercions}~\cite{barthe95implicit} to make a +partially specified term well-typed. The refiner of \MATITA{} is implemented 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. +the conversion check, the refiner is based on \emph{unification}~\cite{strecker} +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 used in CIC to represent proofs, correct incomplete proofs are represented by refinable partially specified terms. The metavariables @@ -454,10 +500,10 @@ 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{}. +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?} +previous statuses. As fully specified terms, partially specified terms are not well suited for user consumption since their syntax is not extendible and it is not @@ -468,8 +514,8 @@ information that can be inferred by the refiner. \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 +The language used to communicate proofs and especially formulae with the +user does not only needs to be extendible and accommodate the usual mathematical notation. It must also reflect the comfortable degree of imprecision and ambiguity that the mathematical language provides. @@ -486,36 +532,38 @@ properties of addition over the binary representation are very different from those of addition over the unary representation. And addition over two natural numbers is definitely different from addition over two real numbers. -Formal mathematics cannot hide these differences and obliges the user to be +Formalized mathematics cannot hide these differences and obliges the user to be very precise on the types he is using and their representation. However, to communicate formulae with the user and with external tools, it seems good 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. +the \emph{content level}~\cite{adams} representation of formulae. -In \MATITA{} we provide two translations: from partially specified terms +In \MATITA{} we provide 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. 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~\cite{mathml} is a W3C -standard -for the representation of content level expressions in an XML extensible format. +formulae. The firsts are translated to a content level representation of +proof steps that can in turn easily be rendered in natural language +using techniques inspired by~\cite{natural,YANNTHESIS}. The representation +adopted has greatly influenced the OMDoc~\cite{omdoc} proof format that is now +isomorphic to it. Terms that represent formulae are translated to \MATHML{} +Content formulae. \MATHML{} Content~\cite{mathml} is a W3C standard +for the representation of content level formulae in an extensible XML format. The translation to content level is implemented in the \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 +proofs and terms that represent formulae. Part of it is also stored at the content level since it is required to generate the natural language rendering 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. +and not a DAG). The reason is that to different occurrences of a subterm +we need to associate different typing information. 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. @@ -525,21 +573,46 @@ 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{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 reverse translation for formulae. The mapping from +content level formulae 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 +every ambiguous formula one partially specified term. The \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'' +disambiguation algorithm presented in~\cite{disambiguation} that is +responsible of building in an efficient way the set of all correct interpretations. An interpretation is correct if the partially specified term obtained using the interpretation is refinable. +In Sect.~\ref{sec:partiallyintro} we described the semantics of +a command as a +function from status to status. We also hinted 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 +of $x$ to be replaced is located, its context is unknown. Since $y^2$ must +replace $x$ in that context, its encoding as a term cannot be computed +until $x$ is located. In other words, $y^2$ must be disambiguated in the +context of the occurrence $x$ it must replace. + +The elegant solution we have implemented consists in representing terms +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 level term to be disambiguated. Our solution should be compared with +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. 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. Moreover, 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} +\label{sec:presentationintro} Content level terms are a sort of abstract syntax trees for mathematical -expressions and proofs. The concrete syntax given to these abstract trees +formulae 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 @@ -549,23 +622,24 @@ 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 +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. +\BOXML. 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 \component. However, in the \texttt{hgdome} \component{} we provide a few -utility functions to build a \GDOME~\cite{gdome2} MathML+BoxML tree from our +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 +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 the implementation of \emph{semantic selection}. Semantic selection is a technique that consists in enriching the presentation @@ -577,7 +651,7 @@ 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 +\emph{semantic copy \& 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). @@ -620,10 +694,11 @@ The \MATITA{} proof assistant and the \WHELP{} search engine are both linked 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. @@ -631,286 +706,161 @@ 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}} - +browser. 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] +%In particular, the \texttt{xml} \component{} is used to easily represent, +%parse and pretty-print XML files. + +\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 +to its historical origins, \MATITA{} strives to provide innovative +functionalities for the interaction with the library. It is more traditional +in its script based authoring interface. In the remaining part of the paper we +focus on the user view of \MATITA. + +The library of \MATITA{} comprises mathematical concepts (theorems, +axioms, definitions) and notation. The concepts are authored sequentially +using scripts that are (ordered) sequences of procedural commands. +Once they are produced we store them independently in the library. +The only relation implicitly kept between the concepts are the logical, +acyclic dependencies among them. This way the library forms a global (and +distributed) hypertext. + +\begin{figure}[!ht] \begin{center} -% \includegraphics[width=0.9\textwidth]{a.eps} - \caption{\MATITA{} screenshot} - \label{fig:screenshot} + \includegraphics[width=0.45\textwidth]{pics/cicbrowser-screenshot-browsing} + \hspace{0.05\textwidth} + \includegraphics[width=0.45\textwidth]{pics/cicbrowser-screenshot-query} + \caption{Browsing and searching the library\strut} + \label{fig:cicbrowser1} \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{Compilation and cleaning} -\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 -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 -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, -while the latter is used to store all the metadata needed by -\WHELP{}. - -While the consistency of the data store in the two media has -nothing to do with the nature of -the content of the library and is thus uninteresting (but really -tedious to implement and keep bug-free), there is a deeper -notion of mathematical consistency we need to provide. Each object -must reference only defined object (i.e. each proof must use only -already proved theorems). - -We will focus on how \MATITA{} ensures the interesting kind -of consistency during the formalization of a mathematical theory, -giving the user the freedom of adding, removing, modifying objects -without loosing the feeling of an always visible and browsable -library. - -\subsubsection{Compilation} - -The typechecker component guarantees that if an object is well typed -it depends only on well typed objects available in the library, -that is exactly what we need to be sure that the logic consistency of -the library is preserved. We have only to find the right order of -compilation of the scripts that compose the user development. +\begin{figure}[!ht] + \begin{center} + \includegraphics[width=0.70\textwidth]{pics/cicbrowser-screenshot-con} + \caption[Natural language rendering]{Natural language rendering of a theorem + from the library\strut} + \label{fig:cicbrowser2} + \end{center} +\end{figure} -For this purpose we provide a tool called \MATITADEP{} -that takes in input the list of files that compose the development and -outputs their dependencies in a format suitable for the GNU \texttt{make} tool. -The user is not asked to run \MATITADEP{} by hand, but -simply to tell \MATITA{} the root directory of his development (where all -script files can be found) and \MATITA{} will handle all the compilation -related tasks, including dependencies calculation. -To compute dependencies it is enough to look at the script files for -inclusions of other parts of the development or for explicit -references to other objects (i.e. with explicit aliases, see -\ref{sec:disambaliases}). - -The output of the compilation is immediately available to the user -trough the \WHELP{} technology, since all metadata are stored in a -user-specific area of the database where the search engine has read -access, and all the automated tactics that operates on the whole -library, like \AUTO, have full visibility of the newly defined objects. - -Compilation is rather simple, and the only tricky case is when we want -to compile again the same script, maybe after the removal of a -theorem. Here the policy is simple: clean the output before recompiling. -As we will see in the next section cleaning will ensure that -there will be no theorems in the development that depends on the -removed items. - -\subsubsection{Cleaning} - -With the term ``cleaning'' we mean the process of removing all the -results of an object compilation. In order to keep the consistency of -the library, cleaning an object requires the (recursive) cleaning -of all the objects that depend on it (\emph{reverse dependencies}). - -The calculation of the reverse dependencies can be computed in two -ways, using the relational database or using a simpler set of metadata -that \MATITA{} saves in the filesystem as a result of compilation. The -former technique is the same used by the \emph{Dependency Analyzer} -described in \cite{zack-master} and really depends on a relational +Several useful operations can be implemented on the library only, +regardless of the scripts. For instance, searching and browsing is +implemented by the ``cicBrowser'' window available from the \MATITA{} +GUI. Using it, the hierarchical structure of the library can be +explored (on the left of Fig.~\ref{fig:cicbrowser1}), the natural +language rendering of proofs can be inspected +(Fig.~\ref{fig:cicbrowser2}), and content based searches on the +library can be performed (on the right of Fig.~\ref{fig:cicbrowser1}). +Content based searches are described in +Sect.~\ref{sec:indexing}. Other examples of library operations are +disambiguation of content level terms (see +Sect.~\ref{sec:disambiguation}) and automatic proof searching (see +Sect.~\ref{sec:automation}). + +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 +changes and cooperative development, consistent revisions are necessary. +For instance, to modify a definition, the user could fork a new version +of the library where the definition is updated and all the concepts that +used to rely on it are absent. The user is then responsible to restore +the removed part in the new branch, merging the branch when the library is +fully restored. + +To implement the proposed versioning system on top of a standard one +it is necessary to implement \emph{invalidation} first. Invalidation +is the operation that locates and removes from the library all the concepts +that depend on a given one. As described in Sect.~\ref{sec:libmanagement} removing +a concept from the library also involves deleting its metadata from the database. -The latter is a fall-back in case the database is not -available.\footnote{Due to the complex deployment of a large piece of -software like a database, it is a common practice for the \HELM{} team -to use a shared remote database, that may be unavailable if the user -workstation lacks network connectivity.} This facility has to be -intended only as a fall-back, since the queries of the \WHELP{} -technology depend require a working database. - -Cleaning guarantees that if an object is removed there are no dandling -references to it, and that the part of the library still compiled is -consistent. Since cleaning involves the removal of all the results of -the compilation, metadata included, the library browsable trough the -\WHELP{} technology is always kept up to date. - -\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 -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. - -While they share the same engine for compilation and cleaning, they -provide different granularity. The batch compiler is only able to -compile a whole script and similarly to clean only a whole script -(together with all the other scripts that rely on an object defined in -it). The interactive interface is able to execute single steps of -compilation, that may include the definition of an object, and -similarly to undo single steps. Note that in the latter case there is -no risk of introducing dangling references since the \MATITA{} user -interface inhibit undoing a step which is not the last executed. - -\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