From: Claudio Sacerdoti Coen Date: Thu, 29 May 2003 13:43:15 +0000 (+0000) Subject: Everything Ispell-ed. X-Git-Tag: submitted~15 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=754e9194441e8df1d52e5a66ad6a3a640b992182;p=helm.git Everything Ispell-ed. --- diff --git a/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex b/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex index 78f614de2..723d21dd1 100644 --- a/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex +++ b/helm/papers/calculemus-2003/hbugs-calculemus-2003.tex @@ -54,7 +54,7 @@ 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 + 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 @@ -67,7 +67,7 @@ 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 + \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 @@ -91,8 +91,8 @@ 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 formers are implemented on top of - Computer Algebra Systems; the latters provide interfaces to well-known + 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, CAS and domain-specific problem solvers are natural candidates to be client of these @@ -128,17 +128,17 @@ Sect. \ref{tutors} is an overview of the tutors that have been implemented. As usual, the paper ends with the conclusions and future works. -\section{An \hbugs{} Bird'S Eye View} +\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{} interfaces to its neighbours \hbugs{} + Each actor present one or more \ws{} interfaces to its neighbors \hbugs{} actors. In this section we will detail the role and requirements of each kind of - actors and discuss about the correspondencies between them and the MONET + actors and discuss about the correspondences between them and the MONET entities described in \cite{MONET-Overview}. \paragraph{Clients} @@ -210,7 +210,7 @@ \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 + 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 @@ -220,10 +220,10 @@ URL).\ednote{CSC: OK, sto barando: \hbugs{} non \'e ancora cos\'i multi-sessione. Ma mi sembra la strada che prenderemmo, no?} - The MONET architecture specification does not state explicitely whether - the service and broker answers can be asyncronous. Nevertheless, the - described information flow implicitly suggests a syncronous implementation. - On the contrary, in \hbugs{} every request is asyncronous: the connection + 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. @@ -258,7 +258,7 @@ the \hbugs{} architecture. 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 representated by a tuple of four elements: + 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 @@ -282,7 +282,7 @@ the \hbugs{} architecture. 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 instatiate the metavariable occurrences. + be used to instantiate the metavariable occurrences. \end{description} Each of these information is represented in XML as described in @@ -305,12 +305,12 @@ the \hbugs{} architecture. 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 trasmitted between \wss{}, hints are + 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 particulary useful for the + 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 could be used to complete the proof. This particular hint is encoded as a @@ -322,7 +322,7 @@ the \hbugs{} architecture. that are fixed are those representing the administrative messages (the envelops in the \wss{} terminology). In particular, the broker can manage at the same time several sessions working on different status/hints - formats. Of couse, there must be an agreement between the clients + 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: @@ -339,7 +339,7 @@ the \hbugs{} architecture. re-discover the proof itself. An alternative implementation where the tutors are trusted would simply - send back to the client a new proof-status. Upong receiving the + 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 @@ -347,7 +347,7 @@ the \hbugs{} architecture. 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 autentication. + clients-tutors authentication. \paragraph{Registries} Being central in the \hbugs{} architecture, the broker is also responsible @@ -408,14 +408,14 @@ the \hbugs{} architecture. exploited by the broker on invocation of 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 behaviour (i.e. starting new \musings{} on the + the already described behavior (i.e. starting new \musings{} on the received status), the tutor\ednote{CSC: Ma sei veramente veramente sicuro?} takes also care of stopping ongoing computation invoking \texttt{Stop\_musing} tutors' method. \paragraph{\wss{}} As already discussed, all \hbugs{} actors act as \wss{} offering one or more - services to neighbour actors. To grant as most accessibility as possible to + services to neighbor actors. To grant as most accessibility as possible to our \wss{} we have chosen to bind them using the HTTP/POST bindings described in \cite{wsdlbindings}\footnote{Given that our proof assistant was entirely developed in the Objective Caml language, we have chosen to @@ -478,7 +478,7 @@ the \hbugs{} architecture. 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 successfull application and a + 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} @@ -490,7 +490,7 @@ we have investigated three classes of tutors: \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 @@ -503,7 +503,7 @@ we have investigated three classes of tutors: $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, expecially when non-trivial computations are involved, + 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 @@ -536,14 +536,14 @@ we have investigated three classes of tutors: 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 + 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 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 fail when applied and what will be + 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 willing to try a tactic and wait for a long time just to understand its @@ -575,7 +575,7 @@ we have investigated three classes of tutors: 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. + first time it is contacted. \item{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 @@ -590,8 +590,8 @@ we have investigated three classes of tutors: 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 work that would be spent in proving again already proven results or figuring out where the lemmas could have been stored in the library. @@ -624,14 +624,14 @@ 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 expecially for novice users, but require + This approach could be interesting especially for novice users, but require 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 improvement in this direction could be to distinguish 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: - the new goals could be false and the proof can be closed only by backtraking. + the new goals could be false and the proof can be closed only by backtracking. Other heuristics and/or measures could be added to rate hints and show them to the user in a particular order: an interesting one @@ -664,7 +664,7 @@ we have investigated three classes of tutors: current \wss{} technology is mature enough to have a concrete and useful impact on the daily work of users of proof-assistants. So far, only the tutor that is interfaced with the \helm{} Search-Engine has effectively increased - the productivity of experts users. The usefullness of the tutors developed for + the productivity of experts users. The usefulness of the tutors developed for beginners, instead, need further assessment. \begin{thebibliography}{01}