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
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}
proofs: tactic based and declarative. We will not investigate the philosophy
aroud the choice that many proof assistant made, \MATITA{} included, and we will not compare the two diffrent approaches. We will describe the common issues of the first one and how \MATITA{} tries to solve them.
-For first we must highlight the fact that proof scripts made using tactis are
-particularly unreadable. This is not a big deal for the user while he iw
+First we must highlight the fact that proof scripts made using tactis are
+particularly unreadable. This is not a big deal for the user while he is
constructing the proof, but is considerably a problem when he tries to reread
-what he did or whe he shows his work to someone else.
+what he did or when he shows his work to someone else.
Another common issue for tactic based proof scripts is their mantenibility.
Huge libraries have been developed, and backward compatibility is a really time
consuming task. This problem is usually ameliorated with tacticals, that
-contibute structuring proofs, but rise one more difficulty for the user that
-want to read a proof, since they are executed in an atomic way, making the
-user loose intermediate steps.
+help in structuring proofs and consequently their maintenance, but have a bad
+counterpart in script readability. Since tacticals are executed atomically,
+the common practice of executing again a script to review all the proof steps
+doesn't work at all. This issue in addition to the really poor feeling that a
+list of tactics gives about the proof makes script rereading particularly hard.
\MATITA{} uses a language of tactics and tacticals, but adopts a peculiar
strategy to make this technique more user friendly without loosing in
\subsubsection{Tacticals overview}
Before describing the peculiarities of \MATITA{} tacticals we briefly introduce what tacticals are and where they can be useful.
-Tacticals first appered in LCF(cita qualcosa) and can be seen as programming constructs, like
-looping, branching, error recovery or sequential composition.
+Tacticals first appered in LCF(cita qualcosa) and can be seen as programming
+constructs, like looping, branching, error recovery or sequential composition.
+For example $tac_1~.~tac_2$ executes the first tactic and applies the second
+only to the first goal opened by $tac_1$. Baranching can be used to specify a
+diffrent tactic to apply to each new goal opened by another tactic, for example
+$tac_1\verb+;[+~tac_{1.1}~\verb+|+~tac_{1.2}~\verb+|+~\cdots~|~tac_{1.n}~\verb+]+$
+applies respectively $tac_{1.i}$ to the $i$-th goal opened by $tac_1$. Looping
+can be used to iterate a tactic until it works: $\verb+repeat+~tac$ applies
+$tac$ to the current goal, and again $tac$ to the eventually resulting goals
+until all goal are closed or the tactic fails.
-\MATITA{} tacticals syntax is reported in table \ref{tab:tacsyn}.
\begin{table}
\caption{\label{tab:tacsyn} Concrete syntax of \MATITA{} tacticals.\strut}
\hrule
\hrule
\end{table}
+\MATITA{} tacticals syntax is reported in table \ref{tab:tacsyn}.
While one whould expect to find structured constructs like
$\verb+do+~n~\NT{tactic}$ the syntax allows pieces of tacticals to be written.
This is essential for base idea behind matita tacticals: step-by-step execution.
\subsubsection{\MATITA{} Tinycals}
-The low-level tacticals implementation of \MATITA{} allows a step-by-step execution of a tactical, that substantially means that a $\NT{block\_kind}$ is not execute as an atomic operation. This has two major benefits for the user, even being a so simple idea:
+The low-level tacticals implementation of \MATITA{} allows a step-by-step execution of a tactical, that substantially means that a $\NT{block\_kind}$ is not executed as an atomic operation. This has two major benefits for the user, even being a so simple idea:
\begin{description}
\item[Proof structuring]
- is much easyer. Consider for example a proof by induction. After applying the
+ is much easyer. Consider for example a proof by induction, and imagine you are using classical tacticals. After applying the
induction principle, with one step tacticals, you have to choose: structure
the proof or not. If you decide for the former you have to branch with
- \verb+[+ and write tactics for all the cases and the close the tactical with
+ \verb+[+ and write tactics for all the cases separated by \verb+|+ and the
+ close the tactical with
\verb+]+. You can replace most of the cases by the identity tactic just to
- concentrate only on the first goal, but you will have to one step back and
+ concentrate only on the first goal, but you will have to go one step back and
one further every time you add something inside the tactical. And if you are
boared of doing so, you will finish in giving up structuring the proof and
- write a plain list of tactics.
+ write a plain list of tactics.\\
+ With step-by-step tacticals you can apply the induction principle, and just
+ open the branching tactical \verb+[+. Then you can interact with the system
+ reaching a proof of the first case, without having to specify the whole
+ branching tactical. When you have proved all the induction cases, you close
+ the branching tactical with \verb+]+ and you are done with a structured proof.
\item[Rereading]
is possible. Going on step by step shows exactly what is going on.
Consider again a proof by induction, that starts applying the induction
- principle and suddenly baranches with a \verb+[+. This clearly subdivided all
+ principle and suddenly baranches with a \verb+[+. This clearly separates all
the induction cases, but if the square brackets content is executed in one
single step you completely loose the possibility of rereading it. Again,
executing step-by-step is the way you whould like to review the
projects / helm.git / blobdiff