Proof-planners, proof-assistants, CAS 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 insufficient to fully assess the concrete benefits of this framework.
+ 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
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{} interfaces to its neighbors \hbugs{}
+ Each actor presents one or more \ws{} interfaces to its neighbors \hbugs{}
actors.
In this section we detail the role and requirements of each kind of
- actors and discuss about the correspondences between them and the MONET
+ 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, the
- comparison with \Omegapp{} is less interesting since the functionalities we
- provide so far are clearly a subset of the \OmegaAnts ones.
+ 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
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. More structured hints can also be used: a hint can be
+ 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
- for the broker (to receive hints) and as requesters (to submit new status).
+ 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
+ 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).
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 a new problem. 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, however,
- that all the tutors must expose the same interface to the broker.
+ 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,
+ however, 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
+ 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
\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 the system to each tutor.
+and unsubscribe herself to each tutor.
\myincludegraphics{step1}{t}{12cm}{Example session.}
{Example session.}
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 the lemma by clicking
+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 where the hint helps is guessing what is the name of the lemma
-to apply.}.
+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
\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 directly finish the proof.
+that.} to the user how to complete the proof in one macrostep.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Comandi da dare a gTopLevel %
\paragraph{Proof status}
In our implementation of the \hbugs{} architecture we used the proof
- assistant of the \helm{} project (codename ``gTopLevel'') as an \hbugs{}
+ 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
to the user in gTopLevel (together with its actual arguments) or a set
of alternative suggestions (a list of hints).
- For tactics that don't require any particular argument (like tactics that
+ 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
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
+ 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
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, have to trust the new proof-status. In this
- case the \hbugs{} architecture needs at least to be extended with
- clients-tutors authentication.
+ (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
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 broker's
- \texttt{List\_tutors} method to get a list of available tutors.
- Eventually the client can subscribe to one or more of these using broker's
- \texttt{Subscribe} method. Clients can also unregister from brokers using
+ 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 broker's \texttt{Register\_tutor}
- method. This method is really similar to \texttt{Register\_client}:
+ 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 client's user to
- decide which tutors he wants to subscribe to. As the clients, tutors can
+ 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 clients registry (to
- lookup client's subscription) and tutors registry (to check if some tutors
- has unsubscribed), the broker is able to decide to which tutors 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
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's no need to
+ 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.
\musings{} on the received status), the broker takes also care of stopping
ongoing computation invoking the \texttt{Stop\_musing} method of the tutors.
- \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 abstract 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}.
+%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}.
\paragraph{Tutors}
Each tutor exposes a \ws{} interface and should be able to work, not only for
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 thread always running plus
- an additional thread for each running \musing{}. One thread is devoted to
- listening for incoming \ws{} request; upon correct receiving requests it
- pass the control to a second thread, created on the fly, to handle the
- incoming request following the classical one-thread-per-request approach in
- web servers design.
- If the received request is \texttt{Start\_musing}, a new thread 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
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 gTopLevel has).
- Still working with threads is known to be really error prone due to
+ 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 propose the hint and some administrative
+ 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.
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 suddenly left alone
- with the system, but she can experiment with variations of the proof given
+ 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.
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. CAS can
+ 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 help in proceeding in a proof. Unfortunately, CAS do not
+ 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
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
+ 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:
- the new goals could be false and the proof can be closed only by backtracking.
+ 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
+ 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}.
projects / helm.git / commitdiff