More on accessibility.

diff --git a/helm/papers/matita/matita.tex b/helm/papers/matita/matita.tex
index b17ead7366de31c999a311be9d870ebb1a844ed5..d9a7a525f572972bb90800a547c1d25635a2a146 100644 (file)
--- a/helm/papers/matita/matita.tex
+++ b/helm/papers/matita/matita.tex
@@ -356,8 +356,17 @@ up way and the system must check that no inconsistency arises.
 
 The practice of limiting the scope on the library to the logical environment
 is contrary to our commitment of being able to fully exploit as much as possible
-of the library at any given time. To reconcile the two worlds, we have
-designed \MATITA \ldots \NOTE{Da completare se lo riteniamo un punto interessante.}
+of the library at any given time. To reconcile consistency and visibility
+we have departed from the traditional implementation of an environment
+allowing environments to be built on demand in a top-down way. The new
+implementation is based on a modified meta-theory that changes the way
+convertibility, type checking, unification and refinement judgements.
+The modified meta-theory is fully described in \cite{libraryenvironments}.
+Here we just remark how a strong commitment on the way the user interacts
+with the library has lead to modifications to the logical core of the proof
+assistant. This is evidence that breakthroughs in the user interfaces
+and in the way the user interacts with the tools and with the library could
+be achieved only by means of strong architectural changes.
 
 \subsubsection{Accessibility}
 A large library that is completely in scope needs effective indexing and
@@ -372,6 +381,46 @@ when automatic tactics exploit the library during the proof search. In this
 scenario the tactics must retrieve a set of candidates for backward or
 forward reasoning in a few milliseconds.
 
+The choice of several proof assistants is to use ad-hoc data structures,
+such as context trees, to index all the terms currently in scope. These
+data structures are expecially designed to quickly retrieve terms up
+to matching, instantiation and generalization. All these data structures
+try to maximize sharing of identical subterms so that matching can be
+reduced to a visit of the tree (or dag) that holds all the maximally shared
+terms together.
+
+Since the terms to be retrieved (or at least their initial prefix)
+are stored (actually ``melted'') in the data structure, these data structures
+must collect all the terms in a single location. In other words, adopting
+such data structures means centralizing the library.
+
+In the \MOWGLI{} project we have tried to follow an alternative approach
+that consists in keeping the library fully distributed and indexing it
+by means of spiders that collect metadata and store them in a database.
+The challenge is to be able to collect only a smaller as possible number
+of metadata that provide enough information to approximate the matching
+operation. A matching operation is then performed in two steps. The first
+step is a query to the remote search engine that stores the metadata in
+order to detect a (hopefully small) complete set of candidates that could
+match. Completeness means that no term that matches should be excluded from
+the set of candiates. The second step consists in retrieving from the
+distributed library all the candidates and attempt the actual matching.
+
+In the last we years we have progressively improved this technique.
+Our achievements can be found in \cite{query1,query2,query3}.
+
+The technique and tools already developed have been integrated in \MATITA{},
+that is able to contact a remote \WHELP{} search engine \cite{whelp} or that
+can be directly linked to the code of the \WHELP. In either case the database
+used to store the metadata can be local or remote.
+
+Our current challenge consists in the exploitation of \WHELP{} inside of
+\MATITA. In particular we are developing a set of tactics, for instance
+based on paramodulation \cite{paramodulation}, that perform queries to \WHELP{}
+to restrict the scope on the library to a set of interesting candidates,
+greatly reducing the search space. Moreover, queries to \WHELP{} are performed
+during parsing of user provided terms to disambiguate them.
+
 In Sect.~\ref{sec:metadata} we describe the technique adopted in \MATITA.
 
 \subsubsection{Library management}