From: Stefano Zacchiroli Date: Tue, 15 Jul 2003 10:14:24 +0000 (+0000) Subject: fixed "s" typos X-Git-Tag: camera_ready~7 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=ad108104cc0f5a67bdd7c3af9687df38fb99e8b6 fixed "s" typos --- diff --git a/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex b/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex index 24da5532d..3b778e48f 100644 --- a/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex +++ b/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex @@ -54,10 +54,10 @@ \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 - 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. + 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) @@ -76,11 +76,10 @@ 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 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. + 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}} @@ -109,18 +108,18 @@ suggest possible ways to proceed in a proof. The tutors are orchestrated 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. + 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 in the MONET framework. + 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{} are that the latter is based on a + between \hbugs{} and \OmegaAnts{} is that the latter is based on a black-board architecture and it is not implemented using \wss{} and brokers. @@ -142,14 +141,13 @@ In this section we detail the role and requirements of each kind of actors and 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 ones of - \OmegaAnts. + 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. \paragraph{Clients} An \hbugs{} client is a software component able to produce \emph{proof @@ -166,24 +164,23 @@ 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). Clients - additionally use broker service to know which tutors are available and to - subscribe to one or more of them. + providers and requesters, see Fig. \ref{interfaces}. They act as providers + for the broker (to receive hints) and as requesters (to submit new status). + 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 + 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 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{} client and tutors contact 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 in the \helm{} library. + 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 @@ -243,11 +240,11 @@ appropriate actor's method. \paragraph{Tutors} - Tutors are software component able to consume proof status producing hints. + 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. + 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 @@ -377,7 +374,7 @@ the \hbugs{} architecture. \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 thesis of the ongoing proof + \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 @@ -395,7 +392,7 @@ the \hbugs{} architecture. \end{description} Each of these information is represented in XML as described in - \cite{mowglicic}. Additionally, an \hbugs{} status carry the unique + \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 @@ -421,7 +418,7 @@ the \hbugs{} architecture. 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 - query a lemma database and return to the client a list of all lemmas 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. @@ -429,7 +426,7 @@ the \hbugs{} architecture. 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 envelops in the \wss{} terminology). In particular, the broker can + (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. @@ -481,14 +478,14 @@ the \hbugs{} architecture. 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}: - tutors are required to send an unique identify and a base URI for their + 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 needs to subscribe to. As the clients, tutors can + decide which tutors he wants to subscribe to. As the clients, tutors can unregister from brokers using \texttt{Unregister\_broker} method. - Each time the client status change, it get sent sent to the + 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 @@ -530,19 +527,19 @@ the \hbugs{} architecture. 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 architecture, including + supports different kinds of Web servers architectures, including multi-process and multi-threaded ones.} bindings described in \cite{wsdlbindings}. \paragraph{Tutors} - Each tutor expose a \ws{} interface and should be able to work, not only for + 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. Each tutor is composed - by one thread always running plus + 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 @@ -551,7 +548,7 @@ the \hbugs{} architecture. 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 dyes. If the received request is + \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. @@ -562,7 +559,7 @@ the \hbugs{} architecture. really useful for tactics that rely on a huge but fixed set of lemmas, as every reflexive tactic. - The implementation of a tutor with the described architecture is not that + 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 @@ -652,11 +649,11 @@ we have investigated three classes of tutors: 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 + \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 @@ -685,9 +682,9 @@ we have investigated three classes of tutors: 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 + tactic. The Ring tutor loads and caches all the required theorems the first time it is contacted. - \item{Intelligent Tutors}. Expert users can already benefit from the previous + \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 @@ -753,7 +750,7 @@ we have investigated three classes of tutors: 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 require + This approach could be interesting especially for novice users, but requires the client to trust other actors a bit more than in the current approach. We plan also to add some rating mechanism to the architecture. A first @@ -783,7 +780,7 @@ we have investigated three classes of tutors: 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 + 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