Da capo (matita2.tex).

[helm.git] / helm / papers / matita / matita2.tex

\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{\AUTO}{\textsc{Auto}}
\newcommand{\COQ}{Coq}
\newcommand{\ELIM}{\textsc{Elim}}
\newcommand{\HELM}{Helm}
\newcommand{\HINT}{\textsc{Hint}}
\newcommand{\IN}{\ensuremath{\dN}}
\newcommand{\INSTANCE}{\textsc{Instance}}
\newcommand{\IR}{\ensuremath{\dR}}
\newcommand{\IZ}{\ensuremath{\dZ}}
\newcommand{\LIBXSLT}{LibXSLT}
\newcommand{\LOCATE}{\textsc{Locate}}
\newcommand{\MATCH}{\textsc{Match}}
\newcommand{\MATITA}{Matita}
\newcommand{\METAHEADING}{Symbol & Position \\ \hline\hline}
\newcommand{\MOWGLI}{MoWGLI}
\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{\TEXMACRO}[1]{\texttt{\char92 #1}}
\newcommand{\UWOBO}{UWOBO}
\newcommand{\WHELP}{Whelp}
\newcommand{\DOT}{\ensuremath{\mbox{\textbf{.}}}}
\newcommand{\SEMICOLON}{\ensuremath{\mbox{\textbf{;}}}}
\newcommand{\BRANCH}{\ensuremath{\mbox{\textbf{[}}}}
\newcommand{\SHIFT}{\ensuremath{\mbox{\textbf{\textbar}}}}
\newcommand{\POS}[1]{\ensuremath{#1\mbox{\textbf{:}}}}
\newcommand{\MERGE}{\ensuremath{\mbox{\textbf{]}}}}
\newcommand{\FOCUS}[1]{\ensuremath{\mathtt{focus}~#1}}
\newcommand{\UNFOCUS}{\ensuremath{\mathtt{unfocus}}}
\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{\URI}[1]{\texttt{#1}}

%{\end{SaveVerbatim}\setlength{\fboxrule}{.5mm}\setlength{\fboxsep}{2mm}%
\newenvironment{grafite}{\VerbatimEnvironment
 \begin{SaveVerbatim}{boxtmp}}%
 {\end{SaveVerbatim}\setlength{\fboxsep}{3mm}%
  \begin{center}
   \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}}

\newsavebox{\tmpxyz}
\newcommand{\sequent}[2]{
  \savebox{\tmpxyz}[0.9\linewidth]{
    \begin{minipage}{0.9\linewidth}
      \ensuremath{#1} \\
      \rule{3cm}{0.03cm}\\
      \ensuremath{#2}
    \end{minipage}}\setlength{\fboxsep}{3mm}%
  \begin{center}
   \fcolorbox{black}{gray}{\usebox{\tmpxyz}}
  \end{center}}

\bibliographystyle{plain}

\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}

\runningtitle{The Matita proof assistant}
\runningauthor{Asperti, Sacerdoti Coen, Tassi, Zacchiroli}

% \date{data}

\begin{motto}
``We are nearly bug-free'' -- \emph{CSC, Oct 2005}
\end{motto}

\begin{abstract}
 abstract qui
\end{abstract}

\keywords{Proof Assistant, Mathematical Knowledge Management, XML, Authoring,
Digital Libraries}

\end{opening}

\begin{figure}[t]
 \begin{center}
  \includegraphics[width=0.9\textwidth]{libraries}
  \caption{\MATITA{} 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.

Applications and libraries depend over other libraries forming a
directed acyclic graph (DAG). Each library can be decomposed in
a a set of \emph{modules} also forming a DAG.

Modules and libraries 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.

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:
\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}.
 \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{uwobo}.
 \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}.
 \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}.
\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
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.

To better understand the architecture of \MATITA{} and the role of each
library, we can focus on the rappresentation 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.

\subsection{Fully specified terms}
 \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
   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
   extendible mathematical notation. They are not meant for direct user
   consumption.

   The \texttt{cic} library 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
   \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
   computationally equivalent (i.e. they share the same normal form).

   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,
   providing a mapping from logical names (URIs) to the physical location
   of a notion (an URL). The \texttt{urimanager} library 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. 

   The Proof Checker is the Web service that provides an HTTP interface
   to the \texttt{cic\_proof\_checking} library.

   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
   interface to a (possibly remote) MySql database system used to store the
   metadata. The \texttt{metadata} library 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
   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
   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.

\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
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
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.

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
in the \texttt{cic\_unification} library. 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
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
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.

As fully specified terms, partially specified terms are not well suited
for user consumption since their syntax is not extendible and it is not
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{Terms at the presentation level}

\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}).

\texttt{urimanager}

\texttt{getter}

\texttt{cic}

\acknowledgements
We would like to thank all the students that during the past
five years collaborated in the \HELM{} project and contributed to 
the development of Matita, and in particular
A.Griggio, F.Guidi, P. Di Lena, L.Padovani, I.Schena, M.Selmi, 
V.Tamburrelli.

\theendnotes

\bibliography{matita}


\end{document}