\end{figure}
}
-\usepackage[show]{ed}
-\usepackage{draftstamp}
+%\usepackage[show]{ed}
+%\usepackage{draftstamp}
+\newcommand{\musing}{\texttt{musing}}
+\newcommand{\musings}{\texttt{musings}}
\newcommand{\ws}{Web-Service}
\newcommand{\wss}{Web-Services}
\newcommand{\hbugs}{H-Bugs}
\title{Brokers and Web-Services for Automatic Deduction: a Case Study}
-\author{Claudio Sacerdoti Coen \and Stefano Zacchiroli}
+\author{
+ Claudio Sacerdoti Coen\thanks{Partially supported by `MoWGLI: Math on the Web, Get it by Logic and Interfaces', EU IST-2001-33562} \and
+ Stefano Zacchiroli\thanks{Partially supported by `MyThS: Models and Types for Security in Mobile Distributed Systems', EU FET-GC IST-2001-32617}}
\institute{
Department of Computer Science\\
University of Bologna\\
- Via di Mura Anteo Zamboni 7, 40127 Bologna, ITALY\\
+ Mura Anteo Zamboni 7, 40127 Bologna, ITALY\\
\email{sacerdot@cs.unibo.it}
\and
Department of Computer Science\\
\begin{abstract}
We present a planning broker and several Web-Services for automatic deduction.
- Each Web-Service implements one of the tactics usually available in an
- interactive proof-assistant. When the broker is submitted a "proof status" (an
- unfinished proof tree and a focus on an open goal) it dispatches the proof to
- the Web-Services, collects the successfull results, and send them back to the
- client as "hints" as soon as they are available.
+ Each Web-Service implements one of the tactics usually available in
+ interactive proof-assistants. When the broker is submitted a ``proof status''
+ (an incomplete proof tree and a focus on an open goal) it dispatches the proof
+ to the Web-Services, collects the successful results, and send them back to
+ the client as ``hints'' as soon as they are available.
In our experience this architecture turns out to be helpful both for
experienced users (who can take benefit of distributing heavy computations)
The \ws{} approach at software development seems to be a working solution for
getting rid of a wide range of incompatibilities between communicating
software applications. W3C's efforts in standardizing related technologies
- grant longevity and implementations availability for frameworks based on \wss{}\
- for information exchange. As a direct conseguence, the number of such
+ grant longevity and implementations availability for frameworks based on
+ \wss{} for information exchange. As a direct consequence, the number of such
frameworks is increasing and the World Wide Web is moving from a disorganized
repository of human-understandable HTML documents to a disorganized repository
of applications working on machine-understandable XML documents both for input
and output.
The big challenge for the next future is to provide stable and reliable
- services over this disorganized, unreliable and ever-evolving architecture.
- The standard solution \ednote{zack: buhm! :-P} is providing a further level of
- stable services (called \emph{brokers}) that behave as common gateway/address
- for client applications to access a wide variety of services and abstract over
- them.
-
- Since the \emph{Declaration of Linz}, the MONET Consortium \cite{MONET},
- following the guidelines \ednote{guidelines non e' molto appropriato, dato che
- il concetto di broker non e' definito da W3C e co} of the \wss{}/brokers
- approach, is working on the development of a framework aimed at providing a
- set of software tools for the advertisement and discovering of mathematical
- web services.
+ services over this disorganized, unreliable, and ever-evolving architecture.
+ The standard solution is to provide a further level of stable services (called
+ \emph{brokers}) that behave as common gateways/addresses for client
+ applications to access a wide variety of services and abstract over them.
+
+ Since the \emph{Declaration of Linz}, the MONET
+ Consortium\footnote{\url{http://monet.nag.co.uk/cocoon/monet/index.html}}
+ is working on the development of a framework, based on the
+ \wss{}/brokers approach, aimed at providing a set of software tools for the
+ advertisement and the discovery of mathematical \wss{}.
%CSC This framework turns out to be strongly based on both \wss{} and brokers.
- Several groups have already developed \wss{} providing both computational and
- reasoning capabilities \cite{???,???,???}\ednote{trovare dei puntatori carini
- dalle conferenze calculemus}: the first ones are implemented on top of
- Computer Algebra Systems; the last ones provide interfaces to well-known
- theorem provers. Proof-planners, proof-assistants, CAS themselves and
- domain-specific problem solvers are natural candidates to be client of these
+ Several groups have already developed software bus and
+ services\footnote{The most part of these systems predate the development of
+ \wss. Those systems whose development is still active are slowly being
+ reimplemented as \wss.} providing both computational and reasoning
+ capabilities \cite{ws1,ws2,ws3,ws4}: the first ones are implemented on top of
+ Computer Algebra Systems; the second ones provide interfaces to well-known
+ theorem provers.
+ Proof-planners, proof-assistants, CASs and
+ domain-specific problem solvers are natural candidates to be clients of these
services. Nevertheless, so far the number of examples in the literature has
- been extremely low and the concrete benefits are still to be assessed.
+ been insufficient to fully assess the concrete benefits of the framework.
In this paper we present an architecture, namely \hbugs{}, implementing a
\emph{suggestion engine} for the proof assistant developed on behalf of the
- \helm{} project. We provide several \wss{} (called \emph{tutors}) able to
+ \helm{}\footnote{Hypertextual Electronic Library of Mathematics,
+ \url{http://helm.cs.unibo.it}} project
+ \cite{helm}. We provide several \wss{} (called \emph{tutors}) able to
suggest possible ways to proceed in a proof. The tutors are orchestrated
- by a broker (a \ws{} itself) that is able to distribute a proof
+ by a broker (a \ws{} itself) that is able to dispatch a proof
status from a client (the proof-assistant) to the tutors;
- each tutor try to make progress in the proof and, in case
- of success, notify the client that shows an \emph{hint} to the user.
- Both the broker and the tutors are instances of the homonymous entities of
- the MONET framework.
-
- A precursor of \hbugs{} is the \OmegaAnts{} project \cite{???},
- which provided similar functionalities to the
- \Omegapp{} proof-planner \cite{Omega}. The main architectural difference
+ each tutor tries to make progress in the proof and, in case
+ of success, notifies the client that shows an \emph{hint} to the user.
+ The broker is an instance of the homonymous entity of the MONET framework.
+ The tutors are MONET services. Another \ws{} (which is not described in this
+ paper and which is called Getter \cite{zack}) is used to locate and download
+ mathematical entities; the Getter plays the role of the Mathematical Object
+ Manager of the MONET framework.
+
+ A precursor of \hbugs{} is the \OmegaAnts{} project
+ \cite{omegaants1,omegaants2}, which provided similar functionalities to the
+ \Omegapp{} proof-planner \cite{omega}. The main architectural difference
between \hbugs{} and \OmegaAnts{} is that the latter is based on a
black-board architecture and it is not implemented using \wss{} and
- brokers. Other differences will be detailed in Sect. \ref{conclusions}.
+ brokers.
In Sect. \ref{architecture} we present the architecture of \hbugs{}.
+ A usage session is shown in Sect. \ref{usage}.
Further implementation details are given in Sect. \ref{implementation}.
Sect. \ref{tutors} is an overview of the tutors that have been implemented.
- As usual, the paper ends with the conclusions and future works.
+ As usual, the final section of this paper is devoted to conclusions and future works.
-\oldpart
-{CSC: Non so se/dove mettere queste parti.
- Zack: per ora facciamo senza e vediamo se/quanto spazio abbiamo, la prima parte
- non e' molto utile, ma la seconda sugli usi tipici di proof assistant
- come ws client si}
-{
- Despite of that the proof assistant case seems to be well suited to
- investigate the usage of many different mathematical \wss{}. Indeed: most proof
- assistants are still based on non-client/server architectures, are
- application-centric instead of document-centric, offer a scarce level of
- automation leaving entirely to the user the choice of which macro (usually
- called \emph{tactic}) to use in order to make progress in a proof.
-
- The average proof assistant can be, for example, a client of a \ws{}\
- interfacing a specific or generic purpose theorem prover, or a client of a
- \ws{} interfacing a CAS to simplify expressions in a particular mathematical
- domain.
-}
-
-\section{Architecture}
+\section{An \hbugs{} Bird's Eye View}
\label{architecture}
\myincludegraphics{arch}{t}{8cm}{\hbugs{} architecture}{\hbugs{} architecture}
The \hbugs{} architecture (depicted in Fig. \ref{arch}) is based on three
different kinds of actors: \emph{clients}, \emph{brokers}, and \emph{tutors}.
- Each actor present one or more \ws{} interface to its neighbours \hbugs{}
+ Each actor presents one or more \ws{} interfaces to its neighbors \hbugs{}
actors.
- In this section we will detail the role and requiremente of each kind of
- actors and discuss about the correspondencies between them and the MONET
+ In this section we detail the role and requirements of each kind of
+ actors and we discuss about the correspondences between them and the MONET
entities described in \cite{MONET-Overview}.
+ Due to lack of space, we cannot compare our framework to similar proposals, as
+ the older and more advanced \Omegapp{} system. The study of the
+ correspondences with MONET is well motivated by the fact that the MONET
+ framework is still under development and that our implementation is one of the
+ first experiments in \ws based distributed reasoning. On the other hand, a
+ comparison with \Omegapp{} would be less interesting since the functionalities we
+ provide so far are just a subset of the \OmegaAnts{} ones.
\paragraph{Clients}
An \hbugs{} client is a software component able to produce \emph{proof
status} and to consume \emph{hints}.
- \ednote{"status" ha il plurale?}
A proof status is a representation of an incomplete proof and is supposed to
be informative enough to be used by an interactive proof assistant. No
- additional requirement exists on the proof status, but there should be an
- agreement on its format between clients and tutors. An hint is a
- representation of a step that can be performed in order to proceed in an
- incomplete proof. Usually it represents a tactic available on some proof
- assistant along with instantiation of its parameters for tactics which
- require them.
-
- Clients act both as \ws{} provider and requester (using W3C's terminology
- \cite{ws-glossary}). They act as providers for the broker (to receive hints)
- ans as requesters again for the broker (to submit new status). Clients
- additionally use broker service to know which tutors are available and to
- subscribe to one or more of them.
-
- Usually, when the role of client is taken by an interactive proof assistant,
+ additional requirements exist on the proof status, but there should be an
+ agreement on its format between clients and tutors. A hint is an
+ encoding of a step that can be performed in order to proceed in an
+ incomplete proof. Usually it represents a reference to a tactic available
+ on some proof assistant along with an instantiation for its formal
+ parameters. Hints can also be more structured: a hint can be
+ as complex as a whole proof-plan.
+
+ Using W3C's terminology \cite{ws-glossary}, clients act both as \ws{}
+ providers and requesters, see Fig. \ref{interfaces}.
+ They act as providers receiving hints from the broker; they act as
+ requesters submitting new status to the tutors.
+ Clients additionally use broker services to know which tutors are available
+ and to subscribe to one or more of them.
+
+ Usually, when the client role is taken by an interactive proof assistant,
new status are sent to the broker as soon as the proof change (e.g. when the
- user applies a tactic or when a new proof is started) and hints are shown to
- the user be the means of some effect in the user interface (e.g. popping a
+ user applies a tactic or when a new proof is started); hints are shown to
+ the user by the means of some effects in the user interface (e.g. popping a
dialog box or enlightening a tactic button).
- \hbugs{} clients act as MONET clients and ask broker to provide access to a
- set of services (the tutors). \hbugs{} has no actors corresponding to MONET's
- Broker Locating Service (since the client is supposed to know the URI of at
- least one broker) and Mathematical Object Manager (since proof status are
- built on the fly and not stored).
+ \hbugs{} clients act as MONET clients and ask brokers to provide access to a
+ set of services (the tutors). \hbugs{} has no actors corresponding to
+ MONET's Broker Locating Service (since the client is supposed to know the
+ URI of at least one broker). The \hbugs{} clients and tutors contact the
+ Getter (a MONET Mathematical Object Manager) to locate and retrieve
+ mathematical items from the \helm{} library.
+ The proof status that are exchanged
+ by the \hbugs{} actors, instead, are built on the fly and are neither
+ stored nor given an unique identifier (URI) to be managed by the
+ Getter.
\paragraph{Brokers}
- \hbugs{} brokers are the key actors of the \hbugs{} architecture since they
- act as intermediaries between clients and tutors. They act both as \ws{}
- provider and requester \emph{both} for clients and tutors.
+ \myincludegraphics{interfaces}{t!}{10cm}{\hbugs{} \wss{} interfaces}
+ {\hbugs{} \wss{} interfaces}
+
+ Brokers are the key actors of the \hbugs{} architecture since they
+ act as intermediaries between clients and tutors. They behave as \wss{}
+ providers and requesters for \emph{both} clients and tutors, see Fig.
+ \ref{interfaces}.
- With respect to client, a broker act as \ws{} provider receiving status and
- forwarding them to one or more tutors. They act as \ws{} requester sending
- hints to client as soon as they are available from tutors.
+ With respect to the client, a broker acts as a \ws{} provider, receiving the
+ proof status and forwarding it to one or more tutors.
+ It also acts as a \ws{} requester sending
+ hints to the client as soon as they are available from the tutors.
- With respect to tutors, the \ws{} provider role is accomplished by receiving
- hints as soon as they are produced; the \ws{} requester one is accomplished
- by requesting computations (\emph{musings} in \hbugs{} terminology) on status
- received by clients and stopping out of date ongoing musings.
+ With respect to the tutors, the \ws{} provider role is accomplished by
+ receiving hints as soon as they are produced; as a requester, it is
+ accomplished by asking for computations (\emph{musings} in \hbugs{}
+ terminology) on status received by clients and by stopping already late but
+ still ongoing \musings{}.
- Additionally brokers keep track of available tutors and subscription of each
- client.
+ Additionally brokers keep track of available tutors and clients
+ subscriptions.
\hbugs{} brokers act as MONET brokers implementing the following components:
Client Manager, Service Registry Manager (keeping track of available
- tutors), Planning Manager (chosing the available tutors among the ones to
- which the client is subscribed), Execution Manager. \ednote{non e' chiaro se
- in monet le risposte siano sincrone o meno, se cosi' fosse dobbiamo
- specificare che nel nostro caso non lo sono}
+ tutors), Planning Manager (choosing the available tutors among the ones to
+ which the client is subscribed), Execution Manager. The Service Manager
+ component is not required since the session handler, that identifies
+ a session between a service and a broker, is provided to the service by
+ the broker instead of being received from the service when the session is
+ initialized. In particular, a session is identified by an unique identifier
+ for the client (its URL) and an unique identifier for the broker (its
+ URL).
+
+ Notice that \hbugs{} brokers have no knowledge of the domain area of
+ proof-assistants, nor they are able to interpret the messages that they
+ are forwarding. They are indeed only in charge of maintaining the
+ abstraction of several reasoning blackboards --- one for each client ---
+ of capacity one: a blackboard is created when the client submits a problem;
+ it is then ``shared'' by the client and all the tutors until the client
+ submits the next problem. For instance, replacing the client with a CAS and
+ all the tutors with agents implementing different resolution methods for
+ differential equations would not require any change in the broker. Notice
+ that all the tutors must expose the same interface to the broker.
+
+ The MONET architecture specification does not state explicitly whether the
+ service and broker answers can be asynchronous. Nevertheless, the
+ described information flow implicitly suggests a synchronous implementation.
+ On the contrary, in \hbugs{} every request is asynchronous: the connection
+ used by an actor to issue a query is immediately closed; when a service
+ produces an answer, it gives it back to the issuer by calling the
+ appropriate actor's method.
\paragraph{Tutors}
- Tutors are software component able to consume proof status producing hints.
- \hbugs{} doesn't specify by which means hints should be produced, tutors can
- use any means necessary (heuristics, external theorem prover or CAS, ...).
- The only requirement is that exists an agreement on the formats of proof
- status and hints.
-
- tutors act both as \ws{} providers and requesters for broker. As providers,
- they wait for commands requesting to start a new musing on a given proof
- status or to stop an old, out of date, musing. As requesters, they signal to
- the broker the end of a musing along with its outcome (an hint in case of
- success or a notification of failure).
+ Tutors are software components able to consume proof status producing hints.
+ \hbugs{} does not specify by which means hints should be produced: tutors
+ can use any means necessary (heuristics, external theorem prover or CAS,
+ etc.). The only requirement is that there exists an agreement on the formats
+ of proof status and hints.
+
+ Tutors act both as \ws{} providers and requesters for the broker, see Fig.
+ \ref{interfaces}. As
+ providers, they wait for commands requesting to start a new \musing{} on
+ a given proof status or to stop an old, out of date, \musing{}. As
+ requesters, they signal to the broker the end of a \musing{} along with its
+ outcome (a hint in case of success or a failure notification).
\hbugs{} tutors act as MONET services.
-\section{???}
+\section{An \hbugs{} Session Example}
+\label{usage}
+In this section we describe a typical \hbugs{} session. The aim of the
+session is to solve the following easy exercise:
+\begin{exercise}
+Let $x$ be a generic real number. Using the \helm{} proof-engine,
+prove that
+\begin{displaymath}
+x = \frac{(x+1)*(x+1) - 1 - x*x}{2}
+\end{displaymath}
+\end{exercise}
+
+Let us suppose that the \hbugs{} broker is already running and that the
+tutors already registered themselves to the broker.
+When the user starts our proof-engine \texttt{gTopLevel}, the system registers itself to
+the broker, that sends back the list of available tutors. By default,
+\texttt{gTopLevel} notifies to the broker its intention of subscribing to every
+tutor available. The user can always open a configuration window where she
+is presented the list of available tutors and she can independently subscribe
+and unsubscribe herself to each tutor.
+
+\myincludegraphics{step1}{t}{12cm}{Example session.}
+ {Example session.}
+%\myincludegraphics{step2}{t}{4cm}{Example session, snapshot 2.}
+% {Example session, snapshot 2.}
+
+The user can now insert into the system the statement of the theorem and start
+proving it. Let us suppose that the first step of the user is proving
+that the denominator 2 is different from 0. Once that this technical result
+is proven, the user must prove the goal shown in the upper right corner
+of the window in background in Fig. \ref{step1}.
+
+While the user is wondering how to proceed in the proof, the tutors are
+trying to progress in the proof. After a while, the tutors' suggestions
+start to appear in the lower part of the \hbugs{} interface window
+(the topmost window in Fig. \ref{step1}). In this case, the tutors are able
+to produce 23 hints. The first and not very useful hint suggests to proceed in
+the proof by exchanging the two sides of the equality.
+The second hint suggests to reduce both sides of the equality to their normal
+form by using only reductions which are justified by the ring structure of the
+real numbers; the two normal forms, though, are so different that the proof is
+not really simplified.
+All the residual 21 hints suggest to apply one lemma from the distributed
+library of \helm{}. The user can look at the statement of any lemma by clicking
+on its URI.
+
+The user can now look at the list of suggestions and realize that a good one is
+applying the lemma \texttt{r\_Rmult\_mult} that allows to multiply both equality
+members by the same scalar\footnote{Even if she does not receive the hint, the
+user probably already knows that this is the right way to proceed. The
+difficult part, accomplished by the hint, is guessing what is the name of the
+lemma to apply.}.
+Double-clicking on the hint automatically applies
+the lemma, reducing the proof to closing three new goals. The first one asks
+the user the scalar to use as an argument of the previous lemma; the second
+one states that the scalar is different from 0; the third lemma (the main
+one) asks to prove the equality between the two new members.
+% is shown in Fig. \ref{step2} where $?_3[H;x]$ stands for
+% the still unknown scalar argument, which can have only $H$ and $x$ as
+% free variables.
+
+The user proceeds by instantiating the scalar with the number 2. The
+\texttt{Assumption} tutor now suggests to close the second goal (that
+states that $2 \neq 0$) by applying the hypothesis $H$.
+No useful suggestions, instead, are generated for the main goal
+$2*x = 2*((x+1)*(x+1)-1-x*x)*2^{-1}$.
+To proceed in the proof the user needs to simplify the
+expression using the lemma $Rinv\_r\_simpl\_m$ that states that
+$\forall x,y.\;y = x * y * x^{-1}$. Since we do not provide yet any tutor
+suggesting simplifications, the user must find out this simplification by
+himself. Once she founds it, the goal is reduced to proving that
+$2*x = (x+1)*(x+1) - 1 - x*x$. This equality is easily solved by the
+\texttt{Ring} tutor, that suggests\footnote{The \texttt{Ring} suggestion is
+just one of the 22 hints that the user receives. It is the only hint that
+does not open new goals, but the user right now does not have any way to know
+that.} to the user how to complete the proof in one macrostep.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Comandi da dare a gTopLevel %
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% New proof:
+% !x.(not (eqT ? (Rplus R1 R1) R0)) -> (eqT ? x (Rdiv (Rminus (Rminus (Rmult (Rplus x R1) (Rplus x R1)) R1) (Rmult x x)) (Rplus R1 R1)))
+% Intros x H
+% Apply r_Rmult_mult
+% 3: Apply H
+% Simpl (per fare unfold di Rdiv)
+% Rewrite <-
+% (Rmult_assoc (Rplus R1 R1) (Rplus (Rplus (Rmult (Rplus x R1) (Rplus x R1)) (Ropp R1)) (Ropp (Rmult x x))) (Rinv (Rplus R1 R1)))
+% Rewrite ->
+% (Rinv_r_simpl_m (Rplus R1 R1) (Rplus (Rplus (Rmult (Rplus x R1) (Rplus x R1)) (Ropp R1)) (Ropp (Rmult x x))) H)
+% *** Ring
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\section{Implementation's Highlights}
\label{implementation}
+In this section we present some of the most relevant implementation details of
+the \hbugs{} architecture.
+
+
+ \paragraph{Proof status}
+ In our implementation of the \hbugs{} architecture we used the proof
+ assistant of the \helm{} project (codename \texttt{gTopLevel}) as an \hbugs{}
+ client. Thus we have implemented serialization/deserialization capabilities
+ for its internal status. In order to be able to describe \wss{} that
+ exchange status in WSDL using the XML Schema type system, we have chosen an
+ XML format as the target format for the serialization.
+
+% A schematic representation of the gTopLevel internal status is depicted in
+% Fig. \ref{status}.
+ Each proof is represented by a tuple of four elements:
+ \emph{uri}, \emph{metasenv}, \emph{proof}, \emph{thesis}.
+
+% \myincludegraphics{status}{t}{8cm}{gTopLevel proof status}{gTopLevel proof
+% status}
+
+ \begin{description}
+ \item[uri]: an URI chosen by the user at the beginning of the proof
+ process. Once (and if) proved, that URI will globally identify the term
+ inside the \helm{} library (given that the user decides to save it).
+ \item[thesis]: the ongoing proof thesis
+ \item[proof]: the current incomplete proof tree. It can contain
+ \emph{metavariables} (holes) that stands for the parts of the proof
+ that are still to be completed. Each metavariable appearing in the
+ tree references one element of the metavariables environment
+ (\emph{metasenv}).
+ \item[metasenv]: the metavariables environment is a list of
+ \emph{goals} (unproved conjectures).
+ In order to complete the proof, the user has to instantiate every
+ metavariable in the proof with a proof of the corresponding goal.
+ Each goal is identified by an unique identifier and has a context
+ and a type (the goal thesis). The context is a list of named
+ hypotheses (declarations and definitions). Thus the context and the goal
+ thesis form a sequent, which is the statement of the proof that will
+ be used to instantiate the metavariable occurrences.
+ \end{description}
+
+ Each of these information is represented in XML as described in
+ \cite{mowglicic}. Additionally, an \hbugs{} status carries the unique
+ identifier of the current goal, which is the goal the user is currently
+ focused on. Using this value it is possible to implement different client
+ side strategies: the user could ask the tutors to work on the goal
+ she is considering or to work on the other ``background'' goals.
+
+ \paragraph{Hints}
+ A hint in the \hbugs{} architecture should carry enough information to
+ permit the client to progress in the current proof. In our
+ implementation each hint corresponds to either one of the tactics available
+ to the user in gTopLevel (together with its actual arguments) or a set
+ of alternative suggestions (a list of hints).
+
+ For tactics that do not require any particular argument (like tactics that
+ apply type constructors or decision procedures)
+ only the tactic name is represented in the hint. For tactics that need
+ terms as arguments (for example the \texttt{Apply} tactic that apply a
+ given lemma) the hint includes a textual representation of them, using the
+ same representation used by the interactive proof assistant when querying
+ user for terms. In order to be transmitted between \wss{}, hints are
+ serialized in XML.
+
+ It is also possible for a tutor to return more hints at once,
+ grouping them in a particular XML element.
+ This feature turns out to be particularly useful for the
+ \emph{searchPatternApply} tutor (see Sect. \ref{tutors}) that
+ queries a lemma database and returns to the client a list of all lemmas that
+ could be used to complete the proof. This particular hint is encoded as a
+ list of \texttt{Apply} hints, each of them having one of the results as term
+ argument.
+
+ We would like to stress that the \hbugs{} architecture has no dependency
+ on either the hint or the status representation: the only message parts
+ that are fixed are those representing the administrative messages
+ (the envelopes in the \wss{} terminology). In particular, the broker can
+ manage at the same time several sessions working on different status/hints
+ formats. Of course, there must be an agreement between the clients
+ and the tutors on the format of the data exchanged.
+
+ In our implementation the client does not trust the tutors hints:
+ being encoded as references to available tactics imply
+ that an \hbugs{} client, at the receipt of a hint, simply try to replay
+ the work
+ done by a tutor on the local copy of the proof. The application of the hint
+ can even fail to type check and the client copy of the proof can be left
+ undamaged after spotting the error. Note, however, that it is still
+ possible to implement a complex tutor that looks for a proof doing
+ backtracking and that
+ send back to the client a hint whose argument is a witness (a trace) of
+ the proof found: the client applies the hint reconstructing (and checking
+ the correctness of) the proof from the witness, without having to
+ re-discover the proof itself.
+
+ An alternative implementation where the tutors are trusted would simply
+ send back to the client a new proof-status. Upon receiving the
+ proof-status, the client would just override its current proof status with
+ the suggested one. In the case of those clients which are implemented
+ using proof-objects (as the Coq proof-assistant, for instance), it is
+ still possible for the client to type-check the proof-object and reject
+ wrong hints. The systems that are not based on proof-objects
+ (as PVS, NuPRL, etc.), instead, must completely trust the new proof-status.
+ In this case the \hbugs{} architecture would need at least to be extended
+ with clients-tutors authentication.
+
+ \paragraph{Registries}
+ Being central in the \hbugs{} architecture, the broker is also responsible
+ of housekeeping operations both for clients and tutors. These operations are
+ implemented using three different data structures called \emph{registries}:
+ clients registry, tutors registry and \musings{} registry.
+
+ In order to use the suggestion engine a client should register itself to the
+ broker and subscribe to one or more tutors. The registration phase is
+ triggered by the client using the \texttt{Register\_client} method of the
+ broker to send him an unique identifier and its base URI as a \ws{}. After
+ the registration, the client can use the \texttt{List\_tutors} method of the
+ broker to get a list of available tutors. Eventually the client can
+ subscribe to one or more of these using the \texttt{Subscribe} method of the
+ broker. Clients can also unregister from brokers using
+ \texttt{Unregister\_client} method.
+
+ The broker keeps track of both registered clients and clients' subscriptions
+ in the clients registry.
+
+ In order to be advertised to clients during the subscription phase, tutors
+ should register to the broker using the \texttt{Register\_tutor} method of
+ the broker. This method is really similar to \texttt{Register\_client}:
+ tutors are required to send an unique identifier and a base URI for their
+ \ws{}.
+ Additionally tutors are required to send an human readable description of
+ their capabilities; this information could be used by the client user to
+ decide which tutors she wants to subscribe to. As the clients, tutors can
+ unregister from brokers using \texttt{Unregister\_broker} method.
+
+ Each time the client status changes, it get sent sent to the
+ broker using its \texttt{Status} method. Using both the clients registry (to
+ lookup the client's subscription) and the tutors registry (to check if some tutors
+ have unsubscribed), the broker is able to decide to which tutors the
+ new status have to be forwarded.
+% \ednote{CSC: qui o nei lavori futuri parlare
+% della possibilit\'a di avere un vero brocker che multiplexi le richieste
+% dei client localizzando i servizi, etc.}
+
+ The forwarding operation is performed using the \texttt{Start\_musing}
+ method of the tutors, that is a request to start a new computation
+ (\emph{\musing{}}) on a given status. The return value of
+ \texttt{Start\_musing} is a
+ \musing{} identifier that is saved in the \musings{} registry along with
+ the identifier of the client that triggered the \musing{}.
+
+ As soon as a tutor completes an \musing{}, it informs the broker
+ using its \texttt{Musing\_completed} method; the broker can now remove the
+ \musing{} entry from the \musings{} registry and, depending on its outcome,
+ inform the client. In case of success one of the \texttt{Musing\_completed}
+ arguments is a hint to be sent to the client; otherwise there is no need to
+ inform him and the \texttt{Musing\_completed} method is called
+ just to update the \musings{} registry.
+
+ Consulting the \musings{} registry, the broker is able to know, at each
+ time, which \musings{} are in execution on which tutor. This peculiarity is
+ exploited by the broker on invocation of the \texttt{Status} method.
+ Receiving a new status from the client implies indeed that the previous
+ status no longer exists and all \musings{} working on it should be stopped:
+ additionally to the already described behavior (i.e. starting new
+ \musings{} on the received status), the broker takes also care of stopping
+ ongoing computation invoking the \texttt{Stop\_musing} method of the tutors.
+
+%CASSATO
+% \paragraph{\wss{}}
+% As already discussed, all \hbugs{} actors act as \wss{} offering one or more
+% services to neighbor actors. To grant as most accessibility as possible to
+% our \wss{} we have chosen to bind them using the HTTP/POST\footnote{Given
+% that our proof assistant was entirely developed in the Objective Caml
+% language, we have chosen to develop also \hbugs{} in that language in order
+% to maximize code reuse. To develop \wss{} in Objective Caml we have
+% developed an auxiliary generic library (\emph{O'HTTP}) that can be used to
+% write HTTP 1.1 Web servers and abstracts over GET/POST parsing. This library
+% supports different kinds of Web servers architectures, including
+% multi-process and multi-threaded ones.} bindings described in
+% \cite{wsdlbindings}.
-\section{The \hbugs Tutors}
+ \paragraph{Tutors}
+ Each tutor exposes a \ws{} interface and should be able to work, not only for
+ many different clients referring to a common broker, but also for many
+ different brokers. The potential high number of concurrent clients imposes
+ a multi-threaded or multi-process architecture.
+
+ Our current implementation is based on a multi threaded architecture
+ exploiting the capabilities of the O'HTTP library \cite{zack}. Each tutor is
+ composed by one always running thread plus an additional thread for each
+ \musing{}.
+ One thread is devoted to listening for incoming \ws{} requests; when a
+ request is received the control is passed to a second thread, created on the
+ fly, that handle the incoming request (usual one-thread-per-request approach
+ in web servers design).
+ In particular if the received request is \texttt{Start\_musing}, a new thread is
+ spawned to handle it; the thread in duty to handle the HTTP request
+ returns an HTTP response containing the identifier of the just started
+ \texttt{musing}, and then dies. If the received request is
+ \texttt{Stop\_musing}, instead, the spawned thread kills the thread
+ responsible for the \texttt{musing} whose identifier is the argument
+ of the \texttt{Stop\_musing} method.
+
+ This architecture turns out to be scalable and allows the running threads
+ to share the cache of loaded (and type-checked) theorems.
+ As we will explain in Sect. \ref{tutors}, this feature turns out to be
+ really useful for tactics that rely on a huge but fixed set of lemmas,
+ as every reflexive tactic.
+
+ The implementation of a tutor within the described architecture is not that
+ difficult having a language with good threading capabilities (as OCaml has)
+ and a pool of already implemented tactics (as \texttt{gTopLevel} has).
+ Working with threads is known to be really error prone due to
+ concurrent programming intrinsic complexity. Moreover, there is a
+ non-neglectable part of code that needs to be duplicated in every tutor:
+ the code to register the tutor to the broker and to handle HTTP requests;
+ the code to manage the creation and termination of threads; and the code for
+ parsing the requests and serializing the answers. As a consequence we
+ have written a generic implementation of a tutor which is parameterized
+ over the code that actually proposes the hint and over some administrative
+ data (as the port the tutor will be listening to).
+
+ The generic tutor skeleton is really helpful in writing new tutors.
+ Nevertheless, the code obtained by converting existing tactics into tutors
+ is still quite repetitive: every tutor that wraps a tactic has to
+ instantiate its own copy of the proof-engine kernel and, for each request,
+ it has to override its status, guess the tactic arguments, apply the tactic
+ and, in case of success, send back a hint with the tactic name and the
+ chosen arguments. Of course, the complex part of the work is guessing the
+ right arguments. For the simple case of tactics that do not require
+ any argument, though, we are able to automatically generate the whole
+ tutor code given the tactic name. Concretely, we have written a
+ tactic-based tutor template and a script that parses an XML file with
+ the specification of the tutor and generates the tutor's code.
+ The XML file describes the tutor's port, the code to invoke the tactic,
+ the hint that is sent back upon successful application and a
+ human readable explanation of the tactic implemented by the tutor.
+
+\section{The Implemented \hbugs Tutors}
\label{tutors}
-To test the \hbugs architecture and to assess the utility of a suggestion
+To test the \hbugs{} architecture and to assess the utility of a suggestion
engine for the end user, we have implemented several tutors. In particular,
we have investigated three classes of tutors:
\begin{enumerate}
\item \emph{Tutors for beginners}. These are tutors that implement tactics
which are neither computationally expensive nor difficult to understand:
an expert user can always understand if the tactic can be applied or not
- withouth having to try it. For example, the following implemented tutors
+ without having to try it. For example, the following implemented tutors
belong to this class:
\begin{itemize}
\item \emph{Assumption Tutor}: it ends the proof if the thesis is
- equivalent\footnote{The equivalence relation is convertibility. In some
- cases, expecially when non-trivial computations are involved, the user
- is totally unable to figure out the convertibility of two terms.
- In these cases the tutor becomes handy also for expert users.}
- to one of the hypotheses.
+ equivalent\footnote{In our implementation, the equivalence relation
+ imposed by the logical framework is \emph{convertibility}. Two
+ expressions are convertible when they reduce to the same normal form.
+ Two ``equal'' terms depending on free variables can be non-convertible
+ since free variables stop the reduction. For example, $2x$ is convertible
+ with $(3-1)x$ because they both reduce to the same normal form
+ $x + x + 0$; but $2x$ is not convertible to $x2$ since the latter is
+ already in normal form.}
+ to one of the hypotheses\footnote{
+ In some cases, especially when non-trivial computations are involved,
+ the user is totally unable to figure out the convertibility of two terms.
+ In these cases the tutor becomes handy also for expert users.}.
\item \emph{Contradiction Tutor}: it ends the proof by \emph{reductio ad
adsurdum} if one hypothesis is equivalent to $False$.
\item \emph{Symmetry Tutor}: if the goal thesis is an equality, it
suggests to apply the commutative property.
- \item \emph{Left/Right/Exists/Split/Constructor Tutors}: the Constructor
- Tutor suggests to proceed in the proof by applying one or more
- constructors when the goal thesis is an inductive type or a
- proposition inductively defined according to the declarative style.
- Since disjunction, conjunction and existential quantifications are
- particular cases of inductive propositions,
- all the other tutors of this class implements restrictions of the
- the Constructor tactic: Left and Right suggest to prove a disjunction
+ \item \emph{Left/Right/Exists/Split/Reflexivity/Constructor Tutors}:
+ the Constructor Tutor suggests to proceed in the proof by applying one
+ or more constructors when the goal thesis is an inductive type or a
+ proposition inductively defined according to the declarative
+ style\footnote{An example of a proposition that can be given in
+ declarative style is the $\le$ relation over natural numbers:
+ $\le$ is the smallest relation
+ such that $n \le n$ for every $n$ and $n \le m$ for every $n,m$ such
+ that $n \le p$ where $p$ is the predecessor of $m$. Thus, a proof
+ of $n \le n$ is simply the application of the first constructor to
+ $n$ and a proof of $n \le m$ is the application of the second
+ constructor to $n,m$ and a proof of $n \le m$.}.
+ Since disjunction, conjunction, existential quantification and
+ Leibniz equality are particular cases of inductive propositions,
+ all the other tutors of this class are instantiations of the
+ the Constructor tactic. Left and Right suggest to prove a disjunction
by proving its left/right member; Split reduces the proof of a
conjunction to the two proof of its members; Exists suggests to
prove an existential quantification by providing a
- witness\footnote{This task is left to the user.}.
+ witness\footnote{This task is left to the user.}; Reflexivity proves
+ an equality whenever the two sides are convertible.
\end{itemize}
Beginners, when first faced with a tactic-based proof-assistant, get
lost quite soon since the set of tactics is large and their names and
semantics must be remembered by heart. Tutorials are provided to guide
the user step-by-step in a few proofs, suggesting the tactics that must
be used. We believe that our beginners tutors can provide an auxiliary
- learning tool: after the tutorial, the user is not suddendly left alone
- with the system, but she can experiment with variations of the proof given
+ learning tool: after the tutorial, the user is not suddenly left alone
+ with the system, but she can experiment with variations of the exercises given
in the tutorial as much as she like, still getting useful suggestions.
Thus the user is allowed to focus on learning how to do a formal proof
instead of wasting efforts trying to remember the interface to the system.
- \item{Tutors for Computationally Expensive Tactics}. Several tactics have
- an unpredictable behaviour, in the sense that it is unfeasible to understand
- wether they will succeed or they will failt when applied and what will be
+ \item \emph{Tutors for Computationally Expensive Tactics}. Several tactics have
+ an unpredictable behavior, in the sense that it is unfeasible to understand
+ whether they will succeed or they will fail when applied and what will be
their result. Among them, there are several tactics either computationally
- expensive or resources consuming. In the first case, the user is not
+ expensive or resource consuming. In the first case, the user is not
willing to try a tactic and wait for a long time just to understand its
outcome: she would prefer to keep on concentrating on the proof and
have the tactic applied in background and receive out-of-band notification
can easily pre-load the required theorems.
As an example of computationally expensive task, we have implemented
- a tutor for the \emph{Ring} tactic. The tutor is able to prove an equality
- over a ring by reducing both members to a common normal form. The reduction,
- which may require some time in complex cases,
+ a tutor for the \emph{Ring} tactic \cite{ringboutin}.
+ The tutor is able to prove an equality over a ring by reducing both members
+ to a common normal form. The reduction, which may require some time in
+ complex cases,
is based on the usual commutative, associative and neutral element properties
of a ring. The tactic is implemented using a reflexive technique, which
means that the reduction trace is not stored in the proof-object itself:
must be stored both the algorithm used for the reduction and the proof of
correctness of the algorithm, based on the ring axioms. This big proof
and all of its lemmas must be retrieved and loaded in order to apply the
- tactic. The Ring tutor loads and cache all the required theorems the
- first time it is conctacted.
- \item{Intelligent Tutors}. Expert users can already benefit from the previous
+ tactic. The Ring tutor loads and caches all the required theorems the
+ first time it is contacted.
+ \item \emph{Intelligent Tutors}. Expert users can already benefit from the previous
class of tutors. Nevertheless, to achieve a significative production gain,
they need more intelligent tutors implementing domain-specific theorem
provers or able to perform complex computations. These tutors are not just
such as proof-planners, CAS or theorem-provers.
To test the productivity impact of intelligent tutors, we have implemented
- a tutor that is interfaced with the HELM
- Proof-Engine\footnote{\url{http://mowgli.cs.unibo.it/library.html}} and that
+ a tutor that is interfaced with the \helm{}
+ Search-Engine\footnote{\url{http://helm.cs.unibo.it/library.html}} and that
is able to look for every theorem in the distributed library that can
be applied to proceed in the proof. Even if the tutor deductive power
is extremely limited\footnote{We do not attempt to check if the new goals
- obtained applying a lemma can be authomatically proved or, even better,
- auhomatically disproved to reject the lemma.}, it is not unusual for
+ obtained applying a lemma can be automatically proved or, even better,
+ automatically disproved to reject the lemma.}, it is not unusual for
the tutor to come up with precious hints that can save several minutes of
- works that would be spent in proving again already proven results or
+ work that would be spent in proving again already proven results or
figuring out where the lemmas could have been stored in the library.
\end{enumerate}
-Once the code that implements a tactic or decision procedure is available,
-transforming it into a tutor is not a difficult task, but it is surely
-repetitive and error prone.
-
-\section{???}
+\section{Conclusions and Future Work}
\label{conclusions}
-
-% \section{Introduction}
-% Since the development of the first proof-assistants based on the
-% Curry-Howard isomorphism, it became clear that directly writing
-% lambda-terms (henceforth called simply terms) was a difficult, repetitive,
-% time-expensive and error prone activity; hence the introduction of
-% meta-languages to describe procedures that are able to automatically
-% generate the low-level terms.
-% Nowadays, almost all the proof-assistants
-% using terms description of proofs have many levels of abstractions, i.e.
-% meta-languages, to create the terms, with the only remarkable exception
-% of the ALF family \cite{ALF} in which terms are still directly written
-% without any over-standing level of abstraction.
-%
-% In particular, there are
-% usually at least two levels, that of tactics and that of the language in
-% which the whole system and hence the tactics are written; once the tactics
-% are implemented, to do a proof the user enters to the system a sequence of
-% tactics, called a script; the script is then executed to create the term
-% encoding of the proof, which is type-checked by the kernel of the
-% proof-assistant. Writing a script interactively is much simpler than
-% writing the term by hands; once written, though, it becomes impossible
-% to understand a script without replaying it interactively. For this reason,
-% we can hardly speak of the language of tactics as a high level language,
-% even if it is ``compiled'' to the language of terms.
-%
-% To avoid confusion, in the rest of this paper we will
-% avoid the use of the term ``proof'', using only ``script'' and ``term'';
-% moreover, we will avoid also the terms ``proof-checking'' and ``type-checking'',
-% replacing them with ``retyping'' to mean the type-checking of an already
-% generated term; finally, we will use the term ``compiling'' to mean the
-% execution of a script. Usually, compilation ends with
-% the type-checking of the generated term; hence the choice of ``retyping'' for
-% the type-checking of an already generated term.
-%
-% A long term consequence of the introduction of tactics has been the
-% progressive lowering of interest in terms. In particular, users of
-% modern proof-assistants as Coq \cite{Coq} may even ignore the existence of
-% commands to show the terms generated by their scripts. These terms are
-% usually very huge and quite unreadable, so they don't add any easily
-% accessible information to the scripts. Hence implementors have loosed
-% interest in terms too, as far as their size and compilation time are
-% small enough to make the system response-time acceptable.
-% When this is not the case, it is sometimes possible to trade space
-% with time using reflexive tactics, in which the potentiality of complex
-% type-systems to speak about themselves are exploited: reflexive tactics
-% usually leads to a polynomial asympotical reduction in the size of the
-% terms, at the cost of an increased reduction time during retyping and
-% compilation. Often, though, reflexive tactics could not be used; moreover,
-% reflexive tactics suffer of the same implementative problems of other tactics
-% and so could be implemented in such a way to create huger than
-% needed terms, even if asymptotically smaller than the best ones created
-% without reflection.
-%
-% The low level of interest in terms of the implementors of
-% tactics often leads to naive implementations (``If it works, it is OK'') and
-% this to low-quality terms, which:
-% \begin{enumerate}
-% \item are huger than needed because particular cases are not taken
-% into account during tactic development
-% \item require more time than needed for retyping due to
-% their size
-% \item are particularly unreadable because they don't
-% correspond to the ``natural'' way of writing the proof by hand
-% \end{enumerate}
-% To cope with the second problem, retyping is usually avoided allowing
-% systems to reload saved terms without retyping them and using a
-% checksum to ensure that the saved file has not been modified. This is
-% perfectly reasonable accordingly to the traditional application-centric
-% architecture of proof-assistants in which you have only one tool integrating
-% all the functionalities and so you are free to use a proprietary format for data
-% representation.
-%
-% In the last months, though, an ever increasing number of people and projects
-% (see, for example, HELM \cite{EHELM}, MathWeb \cite{MATHWEB} and
-% Formavie \cite{FORMAVIE})
-% have been interested to switch from the application-centric model to the
-% newer content-centric one, in which information is stored in
-% standard formats (that is, XML based) to allow different applications to work
-% on the same set of data. As a consequence, term size really becomes an
-% important issue, due to the redundancy of standard formats, and retyping
-% is needed because the applications can not trust each other, hence needing
-% retyping and making retyping time critical.
-% Moreover, as showed by Yann Coscoy in its PhD.
-% thesis \cite{YANNTHESIS} or by the Alfa interface to the Agda system
-% \cite{ALFA}, it is perfectly reasonable and also feasible to try
-% to produce descriptions in natural languages of formal proofs encoded as
-% terms.
-% This approach, combined with the further possibility of applying the usual
-% two-dimensional mathematic notation to the formulas that appears in the
-% terms, is being followed by projects HELM \cite{HELM}, PCOQ \cite{PCOQ} and
-% MathWeb \cite{MATHWEB} with promising results. It must be understood, though,
-% that the quality (in terms of naturality and readability) of this kind of
-% proofs rendering heavily depends on the quality of terms, making also
-% the third characteristic of low-quality terms a critical issue.
-%
-% A totally different scenario in which term size and retyping time are
-% critical is the one introduced by Necula and Lee \cite{Necula} under
-% the name Proof Carrying Code (PCC). PCC is a technique that can be used
-% for safe execution of untrusted code. In a typical instance of PCC, a code
-% receiver establishes a set of safety rules that guarantee safe behavior
-% of programs, and the code producer creates a formal safety proof that
-% proves, for the untrusted code, adherence to the safety rules. Then, the
-% proof is transmitted to the receiver together with the code and it is
-% retyped before code execution. While very compact representation of the
-% terms, highly based on type-inference and unification, could be used
-% to reduce the size and retyping time \cite{Necula2}, designing proof-assistants
-% to produce terms characterized by an high level of quality is still necessary.
-%
-% In the next section we introduce a particular class of metrics for
-% tactics evaluation. In section \ref{equivalence} we consider the
-% notion of tactics equivalence and we describe one of the bad habits
-% of tactics implementors, which is overkilling; we also provide and analyze
-% a simple example of overkilling tactic. In the last section we describe
-% a concrete experience of fixing overkilling in the implementation of a
-% reflexive tactic in system Coq and we analyze the gain with respect to
-% term-size, retyping time and term readability.
-%
-% \section{From Metrics for Terms Evaluation to Metrics for Tactics Evaluation}
-% The aim of this section is to show how metrics for term evaluation could
-% induce metrics for tactic evaluation. Roughly speaking, this allows us to
-% valuate tactics in terms of the quality of the terms produced. Even if
-% we think that these kinds of metrics are interesting and worth studying,
-% it must be understood that many other valuable forms of metrics could be
-% defined on tactics, depending on what we are interested in. For example,
-% we could be interested on compilation time, that is the sum of the time
-% required to generate the term and the retyping time for it. Clearly, only
-% the second component could be measured with a term metric and a good
-% implementation of a tactic with respect to the metric considered could
-% effectively decide to sacrifice term quality (and hence retyping time) to
-% minimize the time spent to generate the term. The situation is very close to
-% the one already encountered in compilers implementation, where there is
-% always a compromise, usually user configurable, between minimizing compiling
-% time and maximizing code quality.
-%
-% The section is organized as follows: first we recall the definition of
-% tactic and we introduce metrics on terms; then we give the definition
-% of some metrics induced by term metrics on tactics.
-%
-% \begin{definition}[Of tactic]
-% We define a \emph{tactic} as a function that, given a goal $G$ (that is, a local
-% context plus a type to inhabit) that satisfies a list of assumptions
-% (preconditions) $P$,
-% returns a couple $(L,t)$ where
-% $L = {L_1,\ldots,L_n}$ is a (possible empty) list of proof-obligations
-% (i.e. goals) and $t$ is a function that, given a list $l = {l_1,\ldots,l_n}$
-% of terms such that $l_i$ inhabits\footnote{We say, with a small abuse of
-% language, that a term $t$ inhabits a goal $G=(\Gamma,T)$ when $t$ is of type
-% $T$ in the context $\Gamma$.} $L_i$ for each $i$ in ${1,\ldots,n}$, returns a
-% term $t(l)$ inhabiting $G$.
-% \end{definition}
-%
-% % You can get another looser definition of tactic just saying that a tactic
-% % is a partial function instead than a total one. In this paper when referring
-% % to tactics we always refer to the first definition.
-%
-% \begin{definition}[Of term metric]
-% For any goal $G$, a term metric $\mu_G$ is any function in
-% $\mathbb{N}^{\{t/t\;\mbox{inhabits}\;G\}}$.
-% Two important class of term metrics are functional metrics and monotone
-% metrics:
-% \begin{enumerate}
-% \item {\bf Functional metrics:} a metric $\mu_G$ is \emph{functional}
-% if for each term context (=term with an hole) $C[]$ and for all terms
-% $t_1$,$t_2$ if $\mu_G(t_1)=\mu_G(t_2)$ then $\mu_G(C[t_1])=\mu_G(C[t_2])$.
-% An equivalent definition is that a metric $\mu_G$ is functional
-% if for each term context $C[]$ the function
-% $\lambda t.\mu_G(C[\mu_G^{-1}(t)])$ is well defined.
-% \item {\bf Monotone metrics:} a metric $\mu_G$ is \emph{monotone} if for
-% each term context $C[]$ and for all terms $t_1$,$t_2$ if
-% $\mu_G(t_1)\le\mu_G(t_2)$ then $\mu_G(C[t_1])\le\mu_G(C[t_2])$.
-% An equivalent definition is that a metric $\mu_G$ is functional if
-% for each term context $C[]$ the function
-% $\lambda t.\mu_G(C[\mu_G^{-1}(t)])$ is well defined and monotone.
-% \end{enumerate}
-%
-% % Vecchie definizioni
-% %\begin{enumerate}
-% %\item {\bf Monotony:} a metric $\mu_G$ is \emph{monotone} if for each term
-% %context (=term with an hole) $C[]$ and for all terms $t_1$,$t_2$ if
-% %$\mu_G(t_1)\le\mu_G(t_2)$ then $\mu_G(C[t_1])\le\mu_G(C[t_2])$
-% %\item {\bf Strict monotony:} a monotone metric $\mu_G$ is \emph{strictly
-% %monotone} if for each term context $C[]$ and
-% %for all terms $t_1$,$t_2$ if $\mu_G(t_1)=\mu_G(t_2)$ then
-% %$\mu_G(C[t_1])=\mu_G(C[t_2])$
-% %\end{enumerate}
-% \end{definition}
-%
-% Typical examples of term metrics are the size of a term, the time required
-% to retype it or even an estimate of its ``naturality'' (or simplicity) to be
-% defined somehow; the first two are also examples of monotone metrics
-% and the third one could probably be defined as to be. So, in the rest
-% of this paper, we will restrict to monotone metrics, even if the
-% following definitions also work with weaker properties for general metrics.
-% Here, however, we are not interested in defining such metrics, but in showing
-% how they naturally induce metrics for tactics.
-%
-% Once a term metric is chosen, we get the notion of a best term (not unique!)
-% inhabiting a goal:
-% \begin{definition}[Of best terms inhabiting a goal]
-% the term $t$ inhabiting a goal $G$ is said to be a best term inhabiting $G$
-% w.r.t. the metric $\mu_G$ when
-% $\mu_G(t) = min\{\mu_G(t') / t'\;\mbox{inhabits}\;G\}$.
-% \end{definition}
-%
-% Using the previous notion, we can confront the behavior of two tactics
-% on the same goal:
-%
-% \begin{definition}
-% Let $\tau_1$ and $\tau_2$ be two tactics both applyable to a goal $G$
-% such that $\tau_1(G) = (L_1,t_1)$ and $\tau_2(G) = (L_2,t_2)$.
-% We say that $\tau_1$ is better or equal than $\tau_2$ for the goal $G$
-% with respect to $\mu_G$ if, for all $l_1$ and $l_2$ lists of best terms
-% inhabiting respectively $L_1$ and $L_2$, $\mu_G(t_1(l_1)) \le \mu_G(t_2(l_2))$
-% holds.
-% \end{definition}
-% Note that confronting in this way ``equivalent'' tactics
-% (whose definition is precised in the next section) gives us information
-% on which implementation is better; doing the same thing on tactics that
-% are not equivalent, instead, gives us information about what tactic to
-% apply to obtain the best proof.
-%
-% A (functional) metric to confront two tactics only on a particular goal
-% has the nice property to be a total order, but is quite useless. Hence,
-% we will now
-% define a bunch of different tactic metrics induced by term metrics
-% that can be used to confront the behavior of tactics when applied to
-% a generic goal. Some of them will be \emph{deterministic} partial orders;
-% others will be total orders, but will provide only a \emph{probabilistic}
-% estimate of the behavior. Both kinds of metrics are useful in practice
-% when rating tactics implementation.
-% \begin{definition}[Of locally deterministic better or equal tactic]
-% $\tau_1$ is a locally deterministic (or locally
-% uniform) better or equal tactic
-% than $\tau_2$ w.r.t. $\mu$ (and in that case we write $\tau_1 \le_{\mu} \tau_2$
-% or simply $\tau_1 \le \tau_2$), when
-% for all goals $G$ satisfying the preconditions of both tactics we have that
-% $\tau_1$ is better or equal than $\tau_2$ w.r.t. the metric $\mu_G$.
-% \end{definition}
-%
-% \begin{definition}[Of locally deterministic better tactic]
-% $\tau_1$ is a locally deterministic (or locally uniform)
-% better tactic than $\tau_2$
-% w.r.t. $\mu$ (and in that case we write $\tau_1 <_{\mu} \tau_2$
-% or simply $\tau_1 < \tau_2$), when $\tau_1 \le_{\mu} \tau_2$ and
-% exists a goal $G$ satisfying the preconditions of both tactics such that
-% $\tau_1$ is better (but not equal!) than $\tau_2$ w.r.t. the metric $\mu_G$.
-% \end{definition}
-%
-% \begin{definition}[Of locally probabilistic better or equal tactic of a factor K]
-% $\tau_1$ is said to be a tactic locally probabilistic better or equal of a
-% factor $0.5 \le K \le 1$ than $\tau_2$ w.r.t. $\mu$ and a particular expected
-% goals distribution when the probability of having $\tau_1$ better or equal than
-% $\tau_2$ w.r.t. the metric $\mu_G$ is greater or equal to $K$ when $G$ is
-% chosen randomly according to the distribution.
-% \end{definition}
-% The set of terms being discrete, you can note that a deterministically better
-% or equal tactic is a tactic probabilistically better or equal of a factor 1.
-%
-%
-% To end this section, we can remark the strong dependence of the $\le$
-% relation on the choice of metric $\mu$, so that it is easy to find
-% two metrics $\mu_1,\mu_2$ such that $\tau_1 <_{\mu_1} \tau_2$ and
-% $\tau_2 <_{\mu_2} \tau_1$. Luckily, tough, the main interesting metrics,
-% term size, retyping time and naturality, are in practice highly correlated,
-% though the correlation of the third one with the previous two could be a
-% bit surprising. So, in the following section, we
-% will not state what is the chosen term metric; you may think as
-% any of them or even at some kind of weighted mean.
-%
-%
-% \section{Equivalent Tactics and Overkilling}
-% \label{equivalence}
-% We are now interested in using the metrics defined in the previous section
-% to confront tactics implementation. Before doing so, though, we have to
-% identify what we consider to be different implementations of the
-% same tactic. Our approach consists in identifying every implementation
-% with the tactic it implements and then defining appropriate notions of
-% equivalence for tactics: two equivalent tactics will then be considered
-% as equivalent implementations and will be confronted using metrics.
-%
-% Defining two tactics as equivalent when they can solve exactly the same
-% set of goals generating the same set of proof-obligations seems quite natural,
-% but is highly unsatisfactory if not completely wrong. The reason is that, for
-% equivalent tactics, we would like to have the \emph{property of substitutivity},
-% that is substituting a tactic for an equivalent one in a script should give
-% back an error-free script\footnote{A weaker notion of substitutivity is that
-% substituting the term generated by a tactic for the term generated by an
-% equivalent one in a generic well-typed term should always give back a
-% well-typed term.}. In logical frameworks with dependent types,
-% without proof-irrelevance and with universes as CIC \cite{Werner} though,
-% it is possible for a term to inspect the term of a previous proof, behaving
-% in a different way, for example, if the constructive proof of a conjunction
-% is made proving the left or right side.
-% So, two tactics, equivalent w.r.t. the previous
-% definition, that prove $A \vee A$ having at their disposal an
-% hypothesis $A$ proving the first one the left and the second one
-% the right part of the conjunction, could not be substituted one for the
-% other if a subsequent term inspects the form of the generated proof.
-%
-% Put in another way, it seems quite reasonable to derive equivalence for
-% tactics from the definition of an underlying equivalence for terms.
-% The simplest form of such an equivalence relation is convertibility
-% (up to proof-irrelevance) of closed terms and this is the relation
-% we will use in this section and the following one. In particular,
-% we will restrict ourselves to CIC and hence to
-% $\beta\delta\iota$-convertibility\footnote{The Coq proof-assistant
-% introduces the notion of \emph{opaque} and \emph{transparent} terms,
-% differing only for the possibility of being inspected. Because the
-% user could change the opacity status at any time, the notion of
-% convertibility we must conservatively choose for the terms of Coq is
-% $\beta\delta\iota$-convertibility after having set all the definitions
-% as transparent.}.
-% Convertibility, though, is a too restrictive notion that does not take
-% in account, for example, commuting conversions. Looking for more suitable
-% notions of equivalence is our main open issue for future work.
-%
-% \begin{definition}[Of terms closed in a local environment]
-% A term $t$ is \emph{closed} in a local environment $\Gamma$ when $\Gamma$
-% is defined on any free variable of $t$.
-% \end{definition}
-%
-% \begin{definition}[Of equivalent tactics]
-% We define two tactics $\tau_1$ and $\tau_2$ to be equivalent (and
-% we write $\tau_1 \approx \tau_2$) when for each goal $G = (\Gamma,T)$ and for
-% each list of terms closed in $\Gamma$ and inhabiting the proof-obligations
-% generated respectively by $\tau_1$ and $\tau_2$, we have that the result terms
-% produced by $\tau_1$ and $\tau_2$ are $\beta\delta\iota$-convertible.
-% \end{definition}
-%
-% Once we have the definition of equivalent tactics, we can use metrics,
-% either deterministic or probabilistic, to confront them. In particular,
-% in the rest of this section and in the following one we will focus on the
-% notion of deterministically overkilling tactic, defined as follows:
-%
-% \begin{definition}[Of overkilling tactics]
-% A tactic $\tau_1$ is (deterministically) overkilling w.r.t. a metric
-% $\mu$ when there exists another tactic $\tau_2$ such that
-% $\tau_1 \approx \tau_2$ and $\tau_2 <_\mu \tau_1$.
-% \end{definition}
-%
-% Fixing an overkilling tactic $\tau_1$ means replacing it with the
-% tactic $\tau_2$ which is the witness of $\tau_1$ being overkilling.
-% Note that the fixed tactic could still be overkilling.
-%
-% The name overkilling has been chosen because most of the time overkilling
-% tactics are tactics that do not consider special cases, following the general
-% algorithm. While in computer science it is often a good design pattern to
-% prefer general solutions to ad-hoc ones, this is not a silver bullet:
-% an example comes another time from compiler technology, where
-% ad-hoc cases, i.e. optimizations, are greatly valuable if not necessary.
-% In our context, ad-hoc cases could be considered either as optimizations,
-% or as applications of Occam's razor to proofs to keep the simplest one.
-%
-% \subsection{A Simple Example of Overkilling Tactic}
-% A first example of overkilling tactic in system Coq is
-% \emph{Replace}, that works in this way: when the current goal
-% is $G = (\Gamma,T)$, the
-% tactic ``{\texttt Replace E$_1$ with E$_2$.}'' always produces a new
-% principal proof-obligation $(\Gamma, T\{E_2/E_1\})$ and an auxiliary
-% proof-obligation $(\Gamma, E_1=E_2)$ and uses the elimination scheme
-% of equality on the term $E_1 = E_2$ and the two terms that inhabit the
-% obligations to prove the current goal.
-%
-% To show that this tactic is overkilling, we will provide an example
-% in which the tactic fails to find the best term, we will
-% propose a different implementation that produces the best term and we will
-% show the equivalence with the actual one.
-%
-% The example consists in applying the tactic in the case in which $E_1$ is
-% convertible to $E_2$: the tactic proposes to the user the two
-% proof-obligations and then builds the term as described above. We claim
-% that the term inhabiting the principal proof-obligation also inhabits
-% the goal and, used as the generated term, is surely smaller
-% and quicker to retype than the one that is generated in the
-% implementation; moreover, it
-% is also as natural as the previous one, in the sense that the apparently
-% lost information has simply become implicit in the reduction and could
-% be easily rediscovered using type-inference algorithms as the one described
-% in Coscoy's thesis \cite{YANNTHESIS}. So, a new implementation could
-% simply recognize this special case and generate the better term.
-%
-% We will now show that the terms provided by the two implementations are
-% $\beta\delta\iota$-convertible.
-% Each closed terms in $\beta\delta\iota$-normal form
-% inhabiting the proof that $E_1$ is equal to $E_2$ is equal to the only
-% constructor of equality applied to a term convertible to the type of
-% $E_1$ and to another term convertible to $E_1$; hence, once the principle
-% of elimination of equality is applied to this term, we can first apply
-% $\beta$-reduction and then $\iota$-reduction to obtain the term inhabiting
-% the principal proof-obligation in which $E_1$ has been replaced by $E_2$.
-% Since $E_1$ and $E_2$ are $\beta\delta\iota$-convertible by hypothesis and
-% for the congruence properties of convertibility in CIC, we have that the
-% generated term is $\beta\delta\iota$-convertible to the one inhabiting the
-% principal proof-obligation.
-%
-% %The simplest example is when $E_1$ and $E_2$ are syntactically equal:
-% %in this case the principal obligation proposed is identical to the current goal
-% %and the equality elimination introduced could be replaced by the proof of
-% %this obligation, leading to a smaller, quicker to retype and also more
-% %natural\footnote{Even if naturality is in some way a subjective metric,
-% %who would dare say that a proof in which you rewrite an expression with
-% %itself is natural?} term. To show that handling this special case in this
-% %way is equivalent to the current solution, we have to show that the two
-% %terms are $\beta\delta\iota$-convertible when so are the subterms inhabiting
-% %the obligations.
-% %The only closed term in $\beta\delta\iota$-normal form
-% %inhabiting the proof that $E_1$ is equal to $E_1$ is the only constructor
-% %of equality applied to the type of $E_1$ and to $E_1$; hence we can
-% %first apply $\beta$-reduction and then $\iota$-reduction to obtain
-% %the second proof in which $E_1$ has been replaced by $E_1$, i.e. the
-% %second proof.
-%
-% %So, for this example, the simple fix to avoid overkilling is checking
-% %if $E_1$ and $E_2$ are syntactically equal and in case omitting the elimination;
-% %curiously, this is done in Coq in the implementation of a very similar tactic
-% %called \emph{Rewriting}.
-%
-%
-% %A second, more involved, example is when $E_1$ and $E_2$ are not
-% %syntactically equal, but $E_1$ reduces to $E_2$. Even in this case
-% %the elimination could simply be avoided because the typing rules of
-% %the logical system ensures us that a term that inhabits the principal
-% %obligation also inhabits the current goal: the proof is equivalent to the
-% %previous one, but for the last step in which $E_2$ is actually substituted for
-% %$E_1$; by hypothesis, though, the two terms are $\beta\delta\iota$-convertible
-% %and hence the thesis.
-%
-% %Surely smaller and faster to retype, the new term is also as natural
-% %as the previous one, in the sense that the apparently lost information has
-% %simply become implicit in the reduction and could be easily rediscovered
-% %using type-inference algorithms as the one described in chapter ???
-% %of Coscoy's thesis \ref{YANNTHESIS}.
-%
-% This example may seem quite stupid because, if the user is already able to
-% prove the principal proof-obligation and because this new goal is totally
-% equivalent to the original one, the user could simply redo the same steps
-% without applying the rewriting at all. Most of the time, though, the
-% convertibility of the two terms could be really complex to understand,
-% greatly depending on the exact definitions given; indeed, the user could
-% often be completely unaware of the convertibility of the two terms. Moreover,
-% even in the cases in which the user understands the convertibility, the
-% tactic has the important effect of changing the form of the current
-% goal in order to simplify the task of completing the proof, which is the reason
-% for the user to apply it.
-%
-% ~\\
-%
-% The previous example shows only a very small improvement in the produced
-% term and could make you wonder if the effort of fixing overkilling and
-% more in general if putting more attention to terms when implementing
-% tactics is really worth the trouble. In the next section we describe as
-% another example a concrete experience of fixing a complex reflexive tactic
-% in system Coq that has lead to really significant improvements in term
-% size, retyping time and naturality.
-%
-% \section{Fixing Overkilling: a Concrete Experience}
-% Coq provides a reflexive tactic called \emph{Ring} to do associative-commutative
-% rewriting in ring and semi-ring structures. The usual usage is,
-% given the goal $E_1 = E_2$ where $E_1$ and $E_2$ are two expressions defined
-% on the ring-structure, to prove the goal reducing it to proving
-% $E'_1 = E'_2$ where $E'_i$ is the normal form of $E_i$. In fact, once
-% obtained the goal $E'_1 = E'_2$, the tactic also tries to apply simple
-% heuristics to automatically solve the goal.
-%
-% The actual implementation of the tactic by reflexion is quite complex and
-% is described in \cite{Ring}. The main idea is described in Fig. \ref{ring1}:
-% first of all, an inductive data type to describe abstract polynomial is
-% made available. On this abstract polynomial, using well-founded recursion in
-% Coq, a normalization function named $apolynomial\_normalize$ is defined;
-% for technical reasons, the abstract data type of normalized polynomials
-% is different from the one of un-normalized polynomials. Then, two
-% interpretation functions, named $interp\_ap$ and $interp\_sacs$ are given
-% to map the two forms of abstract polynomials to the concrete one. Finally,
-% a theorem named $apolynomial\_normalize\_ok$ stating the equality of
-% the interpretation of an abstract polynomial and the interpretation of
-% its normal form is defined in Coq using well-founded induction. The above
-% machinery could be used in this way: to prove that $E^I$ is equal to its
-% normal form $E^{IV}$, the tactic computes an abstract polynomial $E^{II}$ that,
-% once interpreted, reduces to $E^{I}$, and such that the interpretation
-% of $E^{III} = (apolynomial\_normalize E^{II})$ could be shown to be equal
-% to $E^{IV}$ applying $apolynomial\_normalize\_ok$.
-%
-% %such that $(interp\_ap\;E^{II})$ could be proved (theorem
-% %$apolynomial\_normalize\_ok$) in Coq to be equal to
-% %$(interp\_sacs\;E^{III})$ where
-% %$E^{III} = (apolynomial\_normalize E^{II})$ is another abstract polynomial
-% %in normal form and the three functions $interp\_ap$, $interp\_sacs$ and
-% %$apolynomial\_normalize$ could all be defined inside Coq using well-founded
-% %recursion/induction on the abstract polynomial definition.
-%
-% % \myincludegraphics{ring1}{t}{12cm}{Reflexion in Ring}{Reflexion in Ring}
-% % \myincludegraphics{ring2}{t}{10cm}{Ring implementation (first half)}{Ring implementation (first half)}
-%
-% In Fig. \ref{ring2} the first half of the steps taken
-% by the Ring tactic to prove $E_1 = E_2$ are shown\footnote{Here $E_1$
-% stands for $E^I$.}.
-% The first step is replacing $E_1 = E_2$ with $(interp\_ap\;E^{II}_1) = E_2$,
-% justifying the rewriting using the only one constructor of equality due to
-% the $\beta\delta\iota$-convertibility of $(interp\_ap\;E^{II}_1)$ with $E_1$.
-% The second one is replacing $(interp\_ap\;E^{II})$ with
-% $(interp\_sacs\;E^{III})$, justifying the rewriting using
-% $apolynomial\_normalize\_ok$.
-%
-% Next, the two steps are done again on the left part of the equality,
-% obtaining $(interp\_sacs\;E^{III}_1) = (interp\_sacs\;E^{III}_2)$,
-% that is eventually solved trying simpler tactics as \emph{Reflexivity} or left
-% to the user.
-%
-% The tactic is clearly overkilling, at least due to the usage of rewriting for
-% convertible terms. Let's consider as a simple example the session in Fig.
-% \ref{session}:
-% \begin{figure}[t]
-% %\begin{verbatim}
-% \mbox{\hspace{3cm}\tt Coq $<$ Goal ``0*0==0``.}\\
-% \mbox{\hspace{3cm}\tt 1 subgoal}\\
-% ~\\
-% \mbox{\hspace{3cm}\tt ~~=================}\\
-% \mbox{\hspace{3cm}\tt ~~~~``0*0 == 0``}\\
-% ~\\
-% \mbox{\hspace{3cm}\tt Unnamed\_thm $<$ Ring.}\\
-% \mbox{\hspace{3cm}\tt Subtree proved!}
-% %\end{verbatim}
-% \caption{A Coq session.}
-% \label{session}
-% \end{figure}
-% in Fig. \ref{before} the $\lambda$-term created by the
-% original overkilling implementation of Ring is shown. Following the previous
-% explanation, it should be easily understandable. In particular, the
-% four rewritings are clearly visible as applications of $eqT\_ind$, as
-% are the two applications of $apolynomial\_normalize\_ok$ and the
-% three usage of reflexivity, i.e. the two applications of $refl\_eqT$
-% to justify the rewritings on the left and right members of the equality
-% and the one that ends the proof.
-%
-% Let's start the analysis of overkilling in this implementation:
-% \begin{description}
-% \item[Always overkilling rewritings:] as already stated, four of the rewriting
-% steps are always overkilling because the rewritten term is convertible to
-% the original one due to the tactic implementation.
-% As proved in the previous section, all these rewritings could be simply
-% removed obtaining an equivalent tactic.
-% \item[Overkilling rewritings due to members already normalized:] it may happen,
-% as in our example, that one (or even both) of the two members is already in
-% normal form. In this case the two rewriting steps for that member could be
-% simply removed obtaining an equivalent tactic as shown in the previous section.
-% \item[Rewriting followed by reflexivity:] after having removed all
-% the overkilling rewritings, the general form of the $\lambda$-term produced
-% for $E_1 = E_2$ is the application of two rewritings ($E'_1$ for $E_1$ and
-% $E'_2$ for $E_2$), followed by a proof of $E'_1 = E'_2$. In many cases,
-% $E'_1$ and $E'_2$ are simply convertible and so the tactic finishes the
-% proof with an application of reflexivity to prove the equivalent goal
-% $E'_1 = E'_1$.
-% A smaller and also more natural solution is just to
-% rewrite $E'_1$ for $E_1$ and then proving $E'_1 = E_2$ applying the lemma
-% stating the symmetry of equality to the proof of $E_2 = E'_2$.
-% The equivalence to the original
-% tactic is trivial by $\beta\iota$-reduction because the lemma is proved
-% exactly doing the rewriting and then applying reflexivity:
-% $$
-% \begin{array}{l}
-% \lambda A:Type.\\
-% \hspace{0.2cm}\lambda x,y:A.\\
-% \hspace{0.4cm}\lambda H:(x==y).\\
-% \hspace{0.6cm}(eqT\_ind~A~x~ [x:A]a==x~(refl\_eqT~A~x)~y~H)
-% \end{array}
-% $$
-% \end{description}
-% In Fig. \ref{after} is shown the $\lambda$-term created by the same
-% tactic after having fixed all the overkilling problems described above.
-%
-% \begin{figure}
-% \begin{verbatim}
-% Unnamed_thm < Show Proof.
-% LOC:
-% Subgoals
-% Proof:
-% (eqT_ind R
-% (interp_ap R Rplus Rmult ``1`` ``0`` Ropp (Empty_vm R)
-% (APmult AP0 AP0)) [r:R]``r == 0``
-% (eqT_ind R
-% (interp_sacs R Rplus Rmult ``1`` ``0`` Ropp (Empty_vm R)
-% Nil_varlist) [r:R]``r == 0``
-% (eqT_ind R
-% (interp_ap R Rplus Rmult ``1`` ``0`` Ropp (Empty_vm R) AP0)
-% [r:R]
-% ``(interp_sacs R Rplus Rmult 1 r Ropp (Empty_vm R) Nil_varlist)
-% == r``
-% (eqT_ind R
-% (interp_sacs R Rplus Rmult ``1`` ``0`` Ropp (Empty_vm R)
-% Nil_varlist)
-% [r:R]
-% ``(interp_sacs R Rplus Rmult 1 r Ropp (Empty_vm R)
-% Nil_varlist) == r`` (refl_eqT R ``0``)
-% (interp_ap R Rplus Rmult ``1`` ``0`` Ropp (Empty_vm R) AP0)
-% (apolynomial_normalize_ok R Rplus Rmult ``1`` ``0`` Ropp
-% [_,_:R]false (Empty_vm R) RTheory AP0)) ``0``
-% (refl_eqT R ``0``))
-% (interp_ap R Rplus Rmult ``1`` ``0`` Ropp (Empty_vm R)
-% (APmult AP0 AP0))
-% (apolynomial_normalize_ok R Rplus Rmult ``1`` ``0`` Ropp
-% [_,_:R]false (Empty_vm R) RTheory (APmult AP0 AP0))) ``0*0``
-% (refl_eqT R ``0*0``))
-% \end{verbatim}
-% \caption{The $\lambda$-term created by the original overkilling implementation}
-% \label{before}
-% \end{figure}
-%
-% \begin{figure}
-% \begin{verbatim}
-% Unnamed_thm < Show Proof.
-% LOC:
-% Subgoals
-% Proof:
-% (sym_eqT R ``0`` ``0*0``
-% (apolynomial_normalize_ok R Rplus Rmult ``1`` ``0`` Ropp
-% [_,_:R]false (Empty_vm R) RTheory (APmult AP0 AP0)))
-% \end{verbatim}
-% \caption{The $\lambda$-term created by the new implementation}
-% \label{after}
-% \end{figure}
-%
-% \clearpage
-% \subsection{A Quantitative Analysis of the Gain Obtained}
-% Let's now try a quantitative analysis of the gain with respect to term size,
-% retyping time and naturality, considering the two interesting cases of
-% no member or only one member already in normal form\footnote{If the two
-% members are already in normal form, the new implementation simply applies
-% once the only constructor of the equality to one of the two members. The tactic
-% is also implemented to do the same thing also when the two members are not yet
-% in normal forms, but are already convertible. We omit this other improvement
-% in our analysis.}.
-%
-% \subsubsection{Term Size.}
-% \paragraph{Terms metric definition:} given a term $t$, the metric $|.|$ associates to it its number of nodes $|t|$.
-% \paragraph{Notation}: $|T|$ stands for the number of nodes in the actual parameters
-% given to $interp\_ap$, $interp\_sacs$ and $apolynomial\_normalize\_ok$ to
-% describe the concrete (semi)ring theory and the list of non-primitive
-% terms occurring in the goal to solve. In the example in figures \ref{before}
-% and \ref{after}, $|T|$ is the number of nodes in
-% \begin{texttt}[R Rplus Rmult ``1`` ``0`` Ropp (Empty\_vm R)]\end{texttt}.
-% $|R|$ stands for the number of nodes in the term which is the carrier
-% of the ring structure. In the same examples, $|R|$ is simply 1, i.e.
-% the number of nodes in \begin{texttt}R\end{texttt}.
-%
-% \begin{displaymath}
-% \begin{array}{l}
-% \mbox{\bf Original version:}\\
-% \begin{array}{ll}
-% 1 + (|E^{II}_1| + |T| + 1) + |E_2| + |E_1| + &
-% \mbox{(I rewriting Left)} \\
-% 1 + |E_1| + &
-% \mbox{(justification)} \\
-% 1 + (|E^{III}_1| + |T| + 1) + |E_2| + (|E^{II}_1| + |T| + 1) + &
-% \mbox{(II rewriting Left)} \\
-% (|E^{II}_1| + |T| + 1) + &
-% \mbox{(justification)} \\
-% 1 + (|E^{II}_2| + |T| + 1) + (|E^{III}_1| + |T| + 1) + |E_2| + &
-% \mbox{(I rewriting Right)} \\
-% 1 + |E_2| + &
-% \mbox{(justification)} \\
-% 1 + (|E^{III}_2| + |T| + 1) + (|E^{III}_1| + |T| + 1) + &
-% \mbox{(II rewriting Right)} \\
-% ~(|E^{II}_2| + |T| + 1) +& \\
-% (|E^{II}_2| + |T| + 1) + &
-% \mbox{(justification)} \\
-% 1 + |E_1| = &
-% \mbox{(reflexivity application)} \\
-% \hline
-% 4|E_1| + 2|E_2| + 3|E^{II}_1| + 3|E^{II}_2| + 3|E^{III}_1| + |E^{III}_2| +~ &
-% \mbox{\bf Total number} \\
-% ~10|T| + 17 &
-% \end{array}
-% \end{array}
-% \end{displaymath}
-%
-% \begin{displaymath}
-% \begin{array}{l}
-% \mbox{\bf New version, both members not in normal form:}\\
-% \begin{array}{ll}
-% 1 + |R| + |E_1| + |E'_2| + &
-% \mbox{(Rewriting Right)} \\
-% 1 + |T| + |E^{II}_2| + &
-% \mbox{(justification)} \\
-% 1 + |R| + |E'_2| + |E'_1| + |E_2| + &
-% \mbox{(Symmetry application)} \\
-% 1 + |T| + |E^{II}_1| = &
-% \mbox{(justification)} \\
-% \hline
-% 2|E_1| + |E_2| + |E^{II}_1| + |E^{II}_2| + 2|E'_2| + 2|T| +~ &
-% \mbox{\bf Total number} \\
-% ~2|R| + 4 & \\
-% ~ &
-% \end{array}
-% \end{array}
-% \end{displaymath}
-% \begin{displaymath}
-% \begin{array}{l}
-% \mbox{\bf New version, only the first member not in normal form:}\\
-% \begin{array}{ll}
-% 1 + |R| + |E_1| + |E'_2| + &
-% \mbox{(Rewriting)} \\
-% 1 + |T| + |E^{II}_2| = &
-% \mbox{(justification)} \\
-% \hline
-% |E_1| + |E'_2| + |E^{II}_2| + |T| + |R| + 2~~~ &
-% \mbox{\bf Total number} \\
-% ~ &
-% \end{array}
-% \end{array}
-% \end{displaymath}
-%
-% While the overall space complexity of the terms generated by the new
-% implementation is asymptotically equal to the one of the old implementation,
-% all the constants involved are much smaller, but for the one of
-% $E'_2$ (the two normal forms) that before was 0 and now is
-% equal to 2. Is it possible to have goals for which the new implementation
-% behaves worst than the old one? Unfortunately, yes. This happens when
-% the size of the two normal forms $E'_1$ and $E'_2$ is greatly huger than
-% ($E^{II}_1 + |T| + 1)$ and $(E^{II}_2 + |T| + 1)$. This happens when
-% the number of occurrences of non-primitive terms is much higher than
-% the number of non-primitive terms and the size of them is big. More
-% formally, being $m$ the number of non-primitive terms, $d$ the average
-% size and $n$ the number of occurrences, the new implementation creates bigger
-% terms than the previous one if
-% \begin{displaymath}
-% n \log_2 m + m d < n d
-% \end{displaymath}
-% where the difference between the two members is great enough to hide the gain
-% achieved lowering all the other constants.
-% The logarithmic factor in the previous
-% formula derives from the implementation of the map of variables to
-% non-primitive terms as a tree and the representation of occurrences with
-% the path inside the tree to retrieve the term.
-%
-% To fix the problem, for each non-primitive term occurring more than once
-% inside the normal forms, we can use a \emph{let \ldots in} local definition
-% to bind it to a fresh identifier; then we replace every occurrence of
-% the term inside the normal forms with the appropriate
-% identifier\footnote{This has not yet been implemented in Coq.}.
-% In this way, the above inequation becomes
-% \begin{displaymath}
-% n \log_2 m + m d < n + m d
-% \end{displaymath}
-% that is never satisfied.
-%
-% Here it is important to stress how the latest problem was easily
-% overlooked during the implementation and has been discovered
-% only during the previous analysis, strengthening our belief in
-% the importance of this kind of analysis for tactic implementations.
-%
-% In the next two paragraphs we will consider only the new implementation
-% with the above fixing.
-%
-% \subsubsection{Retyping Time.}
-% \paragraph{Terms metric definition:} given a term $t$, the metric $|.|$ associates to it the time $|t|$ required to retype it.
-%
-% Due to lack of space, we will omit a detailed analysis as the one given
-% for terms size. Nevertheless, we can observe that the retyping time required
-% is surely smaller because all the type-checking operations required for
-% the new implementation are already present in the old one, but for the
-% type-checking of the two normal forms, that have fewer complexity
-% than the type-checking of the two abstract normal forms, and the
-% \emph{let \ldots in} definitions that have the same complexity of the
-% type-checking of the variable map. Moreover, the quite expensive operation
-% of computing the two normal forms is already done during proof construction.
-%
-% %In the case in which both the members of the equality are not in normal form,
-% %we can't expect a great improvement in retyping time but for very cheap
-% %normalizations; this because retyping time is dominated by the factor due to
-% %$apolynomial\_normalize$ that is present in both implementations and is
-% %usually much higher than the factor due to the removed applications of
-% %$interp\_ap$, $interp\_sacs$ and the eliminations of equality.
-%
-% %The situation is very different if one of the two members is already
-% %convertible to its normal form and the reduction involved in the normalization
-% %is expensive. In this rather unlikely case, the new implementation
-% %avoids the reduction at all, roughly halving the overall retyping time.
-%
-% In section \ref{benchmarks} we present some benchmarks to give an idea of
-% the real gain obtained.
-%
-% \subsubsection{Naturality.}~\\~\\
-% The idea behind the \emph{Ring} tactic is to be able to prove
-% an equality showing that both members have the same normal form.
-% This simply amounts to show that each member is equal to the same
-% normal form, that is exactly what is done in the new implementation.
-% Indeed, every step that belonged to the old implementation and has been
-% changed or removed to fix overkilling used to lead to some unnatural step:
-% \begin{enumerate}
-% \item The fact that the normalization is not done on the concrete
-% representation, but passing through two abstract ones that are
-% interpreted on the concrete terms is an implementative detail that
-% was not hidden as much as possible as it should be.
-% \item Normalizing a member of the equality that is already in normal form,
-% is illogical and so unnatural. Hence it should be avoided, but it was not.
-% \item The natural way to show $A=B$ under the hypothesis $B=A$ is just
-% to use the symmetric property of equality. Instead, the old implementation
-% rewrote $B$ with $A$ using the hypothesis and proved the goal by reflexivity.
-% \item Using local definitions (\emph{let \ldots in}) as abbreviations
-% rises the readability of the proof by shrinking its size removing
-% subexpressions that are not involved in the computation.
-% \end{enumerate}
-%
-% \subsection{Some Benchmarks}
-% \label{benchmarks}To understand the actual gain in term size and retyping
-% time on real-life examples, we have done some benchmarks on the whole set
-% of theorems in the standard library of Coq that use the Ring tactic. The
-% results are shown in table~\ref{benchs}.
-%
-% Term size is the size of the disk dump of the terms. Re-typing time is the
-% user time spent by Coq in proof-checking already parsed terms. The reduction
-% of the terms size implies also a reduction in Coq parsing time, that is
-% difficult to compute because Coq files do not hold single terms, but whole
-% theories. Hence, the parsing time shown is really the user time spent by Coq
-% to parse not only the terms on which we are interested, but also all the
-% terms in their theories and the theories on which they depend. So, this last
-% measure greatly under-estimates the actual gain.
-%
-% Every benchmark has been repeated 100 times under different load conditions on
-% a 600Mhz Pentium III bi-processor equipped with 256Mb RAM. The timings shown
-% are mean values.
-%
-% \begin{table}
-% \begin{center}
-% \begin{tabular}{|l|c|c|c|}
-% \hline
-% & ~Term size~ & Re-typing time & Parsing time\\
-% \hline
-% Old implementation & 20.27Mb & 4.59s & 2.425s \\
-% \hline
-% New implementation & 12.99Mb & 2.94s & 2.210s \\
-% \hline
-% Percentage reduction & 35.74\% & 35.95\% & 8.87\% \\
-% \hline
-% \end{tabular}
-% \end{center}
-% \caption{Some benchmarks}
-% \label{benchs}
-% \end{table}
-%
-% \section{Conclusions and Future Work}
-% Naive ways of implementing tactics lead to low quality terms that are
-% difficult to inspect and process. To improve the situation, we show
-% how metrics defined for terms naturally induce metrics for tactics and
-% tactics implementation and we advocate the usage of such metrics for
-% tactics evaluation and implementation. In particular, metrics could
-% be used to analyze the quality of an implementation or could be used at run
-% time by a tactic to choose what is the best way to proceed.
-%
-% To safely replace a tactic implementation with another one, it is important
-% to define when two tactics are equivalent, i.e. generate equivalent terms.
-% In this work, the equivalence relation chosen for terms has simply been
-% $\beta\delta\iota$-convertibility, that in many situations seems too strong.
-% Hence, an important future work is the study of weaker forms of term
-% equivalence and the equivalence relations they induce on tactics. In particular,
-% it seems that proof-irrelevance, $\eta$-conversion and commuting conversions
-% must all be considered in the definition of a suitable equivalence relation.
+ In this paper we described a suggestion engine architecture for
+ proof-assistants: the client (a proof-assistant) sends the current proof
+ status to several distributed \wss{} (called tutors) that try to progress
+ in the proof and, in case of success, send back an appropriate hint
+ (a proof-plan) to the user. The user, that in the meantime was able to
+ reason and progress in the proof, is notified with the hints and can decide
+ to apply or ignore them. A broker is provided to decouple the clients and
+ the tutors and to allow the client to locate and invoke the available remote
+ services. The whole architecture is an instance of the MONET architecture
+ for Mathematical \wss{}. It constitutes a reimplementation of the core
+ features of the pioneering \OmegaAnts{} system in the new \wss{}
+ framework.
+
+ A running prototype has been implemented as part of the
+ \helm{} project \cite{helm}
+ and we already provide several tutors. Some of them are simple tutors that
+ try to apply one or more tactics of the \helm{} Proof-Engine, which is also
+ our client. We also have a much more complex tutor that is interfaced
+ with the \helm{} Search-Engine and looks for lemmas that can be directly
+ applied.
+
+ Future works comprise the implementation of new features and tutors, and
+ the embedding of the system in larger test cases. For instance, one
+ interesting case study would be interfacing a CAS as Maple to the
+ \hbugs{} broker, developing at the same time a tutor that implements the
+ Field tactic of Coq, which proves the equality of two expressions in an
+ abstract field by reducing both members to the same normal form. CASs can
+ produce several compact normal forms, which are particularly informative
+ to the user and that may suggest how to proceed in a proof. Unfortunately,
+ CASs do not
+ provide any certificate about the correctness of the simplification. On
+ the contrary, the Field tactic certifies the equality of two expressions,
+ but produces normal forms that are hardly a simplification of the original
+ formula. The benefits for the CAS would be obtained by using the Field tutor
+ to certify the CAS simplifications, proving that the Field normal form
+ of an expression is preserved by the simplification.
+ More advanced tutors could exploit the CAS to reduce the
+ goal to compact normal forms \cite{maplemodeforCoq}, making the Field tutor
+ certify the simplification according to the skeptical approach.
+
+ We have many plans for further developing both the \hbugs{} architecture and
+ our prototype. Interesting results could be obtained
+ augmenting the informative content of each suggestion. We can for example
+ modify the broker so that also negative results are sent back to the client.
+ Those negative suggestions could be reflected in the user interface by
+ deactivating commands to narrow the choice of tactics available to the user.
+ This approach could be interesting especially for novice users, but requires
+ the client to increase their level of trust in the other actors.
+
+ We plan also to add some rating mechanism to the architecture. A first
+ improvement in this direction could be distinguishing between hints that, when
+ applied, are able to completely close one or more goals, and
+ tactics that progress in the proof by reducing one or more goals to new goals:
+ since the new goals can be false, the user can be forced later on to
+ backtrack.
+
+ Other heuristics and or measures could be added to rate
+ hints and show them to the user in a particular order: an interesting one
+ could be a measure that try to minimize the size of the generated proof,
+ privileging therefore non-overkilling solutions \cite{ring}.
+
+ We are also considering to follow the \OmegaAnts{} path adding
+ ``recursion'' to the system so that the proof status resulting from the
+ application of old hints are cached somewhere and could be used as a starting
+ point for new hint searches. The approach is interesting, but it represents
+ a big shift towards automatic theorem proving: thus we must consider if it is
+ worth the effort given the increasing availability of automation in proof
+ assistants tactics and the ongoing development of \wss{} based on
+ already existent and well developed theorem provers.
+
+ Even if not strictly part of the \hbugs{} architecture, the graphical user
+ interface (GUI) of our prototype needs a lot of improvement if we want
+ it to be really usable by novices. In particular, a critical issue
+ is avoiding continuous distractions for the user determined by the hints
+ that are asynchronously pushed to her.
+
+ Our \wss{} still lack a real integration in the MONET architecture,
+ since we do not provide the different ontologies to describe our problems,
+ solutions, queries, and services. In the short term, completing this task
+ could provide a significative feedback to the MONET consortium and would
+ enlarge the current set of available MONET actors on the Web. In the long
+ term, new more intelligent tutors could be developed on top of already
+ existent MONET \wss{}.
+
+ To conclude, \hbugs{} is a nice experiment meant to understand whether the
+ current \wss{} technology is mature enough to have a concrete and useful
+ impact on the daily work of proof-assistants users. So far, only the tutor
+ that is interfaced with the \helm{} Search-Engine has effectively increased
+ the productivity of experts users. The usefulness of the tutors developed for
+ beginners, instead, need further assessment.
\begin{thebibliography}{01}
-% \bibitem{ALF} The ALF family of proof-assistants:\\
-% {\tt http://www.cs.chalmers.se/ComputingScience/Research/\\Logic/implementation.mhtml}
-%
-% \bibitem{Coq} The Coq proof-assistant:\\
-% {\tt http://coq.inria.fr/}
-%
-% \bibitem{FORMAVIE} The Formavie project:\\
-% {\tt http://http://www-sop.inria.fr/oasis/Formavie/}
-%
-% \bibitem{EHELM} The HELM project:\\
-% {\tt http://www.cs.unibo.it/helm/}
-%
-% \bibitem{MATHWEB} The MathWeb project:\\
-% {\tt http://www.mathweb.org/}
-%
-% \bibitem{PCOQ} The PCoq project:\\
-% {\tt http://www-sop.inria.fr/lemme/pcoq/}
-%
-% \bibitem{HELM} A.Asperti, L.Padovani, C.Sacerdoti Coen, I.Schena.
-% Towards a library of formal mathematics. Panel session of
-% the 13th International Conference on Theorem Proving in Higher Order Logics (TPHOLS'2000),
-% Portland, Oregon, USA.
-%
-% \bibitem{Ring} S. Boutin. Using reflection to build efficient and certified
-% decision procedures. In Martin Abadi and Takahashi Ito, editors, TACS'97,
-% volume 1281. LNCS, Springer-Verlag, 1997.
-%
-% \bibitem{YANNTHESIS} Y.Coscoy. \emph{Explication textuelle de preuves pour le
-% Calcul des Constructions Inductives}, PhD. Thesis, Universit\'e de Nice-Sophia
-% Antipolis, 2000.
-%
-% \bibitem{ALFA} T. Hallgreen, Aarne Ranta. An Extensible Proof Text Editor.
-% Presented at LPAR2000.
-%
-% \bibitem{Necula} G. Necula, P. Lee. Safe Kernel Extensions Without Run-Time
-% Checking. Presented at OSDI'96, October 1996.
-%
-% \bibitem{Necula2} G. Necula, P. Lee. Efficient Representation and Validation of Proofs. Presented at LICS'98, June 1998
-%
-% \bibitem{Werner} B. Werner. \emph{Une Th\'eorie des Constructions Inductives},
-% PhD. Thesis, Universit\'e Paris VII, May 1994.
+\bibitem{ws-glossary} Web Services Glossary, W3C Working Draft, 14 May 2003.\\
+ \url{http://www.w3.org/TR/2003/WD-ws-gloss-20030514/}
+
+\bibitem{wsdlbindings} Web Services Description Language (WSDL)
+ Version 1.2: Bindings, W3C Working Draft, 24 January 2003.\\
+ \url{http://www.w3.org/TR/wsdl12-bindings/}
+
+\bibitem{ws1}A. Armando, D. Zini. Interfacing Computer Algebra and
+ Deduction Systems via the Logic Broker Architecture. In Proceedings
+ of the Eighth Calculemus symphosium, St. Andrews, Scotland, 6--7 August 2000.
+
+\bibitem{ws2} O. Caprotti. Symbolic Evaluator Service. Project Report of
+ the MathBrocker Project, RISC-Linz, Johannes Kepler University, Linz,
+ Austria, May 2002.
+
+\bibitem{helm} A. Asperti, F. Guidi, L. Padovani, C. Sacerdoti Coen, I. Schena.
+ Mathematical Knowledge Management in HELM. In Annals of Mathematics and
+ Artificial Intelligence, 38(1): 27--46, May 2003.
+
+\bibitem{omegaants1} C. Benzm\"uller, V. Sorge. O-Ants -- An Open Approach
+ at Combining Interactive and Automated Theorem Proving. In M. Kerber and
+ M. Kohlhase (eds.), Integration of Symbolic and Mechanized Reasoning, pp.
+ 81--97, 2000.
+
+\bibitem{omegaants2} C. Benzm\"uller, M. Jamnik, M. Kerber, V. Sorge.
+ Agent-based Mathematical Reasoning. In A. Armando and T. Jebelean (eds.),
+ Electronic Notes in Theoretical Computer Science, (1999) 23(3), Elsevier.
+
+\bibitem{omega} C. Benzm\"uller, L. Cheikhrouhou, D. Fehrer, A. Fiedler,
+ X. Huang, M. Kerber, M. Kohlhase, K. Konrad, E. Melis, A. Meier,
+ W. Schaarschmidt, J. Siekmann, V. Sorge. OMEGA: Towards a Mathematical
+ Assistant. In W. McCune (ed), Proceedings of the 14th Conference on
+ Automated Deduction (CADE-14), Springer LNAI vol. 1249, pp. 252--255,
+ Townsville, Australia, 1997.
+
+\bibitem{ringboutin} S. Boutin. Using reflection to build efficient and
+ certified decision procedures. In Martin Abadi and Takahashi Ito, editors,
+ TACS'97, volume 1281. LNCS, Springer-Verlag, 1997.
+
+\bibitem{maplemodeforCoq} David Delahaye, Micaela Mayero.
+ A Maple Mode for Coq. Contribution to the Coq library.\\
+ \url{htpp://coq.inria.fr/contribs/MapleMode.html}
+
+\bibitem{MONET-Overview} The MONET Consortium, MONET Architecture Overview,
+ Public Deliverable D04 of the MONET Project.\\
+ \url{http://monet.nag.co.uk/cocoon/monet/publicsdocs/monet-overview.pdf}
+
+\bibitem{mowglicic} C. Sacerdoti Coen. Exportation Module, MoWGLI Deliverable
+ D2.a.\\
+ \url{http://mowgli.cs.unibo.it/html\_no\_frames/deliverables/transformation/d2a.html}
+
+\bibitem{ring} C. Sacerdoti Coen. Tactics in Modern Proof-Assistants: the
+ Bad Habit of Overkilling. In Supplementary Proceedings of the 14th
+ International Conference TPHOLS 2001, pp. 352--367, Edinburgh.
+
+\bibitem{zack} S. Zacchiroli. \emph{Web services per il supporto alla
+ dimostrazione interattiva}, Master Thesis, University of Bologna, 2002.
+
+\bibitem{ws3} J. Zimmer and M. Kohlhase. System Description: The MathWeb
+ Software Bus for Distributed Mathematical Reasoning.
+ In Proceedings of the 18th International Conference on Automated Deduction
+ CADE 18, LNAI 2392, Springer Verlag, 2002.
+
+\bibitem{ws4} R. Zippel. The MathBus. In Workshop on Internet Accessible
+ Mathematical Computation at ISSAC'99, Vancouver, Canada, July 28--31, 1999.
\end{thebibliography}
projects / helm.git / blobdiff