From: Stefano Zacchiroli Date: Thu, 26 Jan 2006 17:02:43 +0000 (+0000) Subject: spell checking X-Git-Tag: make_still_working~7758 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7aed83dc33c168b0d2d80702c2c0fa076b13a215;hp=8b4337c1d962a6960df64d331a1826cad0b662c7;p=helm.git spell checking --- diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex index eded34c23..ef4ebb1f3 100644 --- a/helm/papers/matita/matita2.tex +++ b/helm/papers/matita/matita2.tex @@ -259,8 +259,6 @@ Moreover, the complexity of the code of \MATITA{} is greatly reduced with respect to \COQ. For instance, the API of the components of \MATITA{} comprise 989 functions, to be compared with the 4'286 functions of \COQ. -FINQUI SPELL CHECKATO - Finally, \MATITA{} has several innovative features over \COQ{} that derive from the integration of Mathematical Knowledge Management tools with proof assistants. Among them, the advanced indexing tools over the library and @@ -275,15 +273,15 @@ and integrated in the system. Moreover, there exists a lot of developments for \COQ{} that require backward compatibility between each pair of releases; since many central functionalities of a proof assistant are based on heuristics or arbitrary choices to overcome undecidability (e.g. for higher order -unification), changing these functionalities mantaining backward compatibility +unification), changing these functionalities maintaining backward compatibility is very difficult. Finally, the code of \COQ{} has been greatly optimized -over the years; optimization reduces maintenability and rises the complexity +over the years; optimization reduces maintainability and rises the complexity of the code. In writing \MATITA{} we have not been hindered by backward compatibility and we have took advantage of the research results and experiences previously developed by others, comprising the authors of \COQ. Moreover, starting from -scratch, we have designed in advance the architecture and we have splitted +scratch, we have designed in advance the architecture and we have split the code in coherent minimally coupled components. In the future we plan to exploit \MATITA{} as a test bench for new ideas and @@ -326,13 +324,13 @@ applications meant to be used directly by the user. All the other applications are Web services developed in the HELM and MoWGLI projects and already described elsewhere. In particular: \begin{itemize} - \item The \emph{Getter} is a Web service to retrieve an (XML) document + \item The \emph{\GETTER} is a Web service to retrieve an (XML) document from a physical location (URL) given its logical name (URI). The Getter is responsible of updating a table that maps URIs to URLs. Thanks to the Getter it is possible to work on a logically monolithic library that is physically distributed on the network. More information on the Getter can be found in~\cite{zack-master}. - \item \emph{Whelp} is a search engine to index and locate mathematical + \item \emph{\WHELP} is a search engine to index and locate mathematical notions (axioms, theorems, definitions) in the logical library managed by the Getter. Typical examples of a query to Whelp are queries that search for a theorem that generalize or instantiate a given formula, or that @@ -340,14 +338,14 @@ elsewhere. In particular: an XML document that lists the URIs of a complete set of candidates that are likely to satisfy the given query. The set is complete in the sense that no notion that actually satisfies the query is thrown away. However, - the query is only approssimated in the sense that false matches can be + the query is only approximated in the sense that false matches can be returned. Whelp has been described in~\cite{whelp}. - \item \emph{Uwobo} is a Web service that, given the URI of a mathematical + \item \emph{\UWOBO} is a Web service that, given the URI of a mathematical notion in the distributed library, renders it according to the user provided - two dimensional mathematical notation. Uwobo may also embed the rendering + two dimensional mathematical notation. \UWOBO{} may also embed the rendering of mathematical notions into arbitrary documents before returning them. - The Getter is used by Uwobo to retrieve the document to be rendered. - Uwobo has been described in~\cite{zack-master}. + The Getter is used by \UWOBO{} to retrieve the document to be rendered. + \UWOBO{} has been described in~\cite{zack-master}. \item The \emph{Proof Checker} is a Web service that, given the URI of notion in the distributed library, checks its correctness. Since the notion is likely to depend in an acyclic way over other notions, the proof checker @@ -355,7 +353,7 @@ elsewhere. In particular: dependencies, checking in turn every notion for correctness. The proof checker has been described in~\cite{zack-master}. \item The \emph{Dependency Analyzer} is a Web service that can produce - a textual or graphical representation of the dependecies of an object. + a textual or graphical representation of the dependencies of an object. The dependency analyzer has been described in~\cite{zack-master}. \end{itemize} @@ -500,8 +498,8 @@ information that can be inferred by the refiner. \subsection{Content level terms} \label{sec:contentintro} -The language used to communicate proofs and expecially formulae with the -user does not only needs to be extendible and accomodate the usual mathematical +The language used to communicate proofs and especially formulae with the +user does not only needs to be extendible and accommodate the usual mathematical notation. It must also reflect the comfortable degree of imprecision and ambiguity that the mathematical language provides. @@ -565,7 +563,7 @@ is guided by an \emph{interpretation}, that is a function that chooses for every ambiguous formula one partially specified term. The \texttt{cic\_disambiguation} \component{} implements the disambiguation algorithm we presented in~\cite{disambiguation} that is -responsible of building in an efficicent way the set of all ``correct'' +responsible of building in an efficient way the set of all ``correct'' interpretations. An interpretation is correct if the partially specified term obtained using the interpretation is refinable. @@ -755,7 +753,7 @@ is still under design. Scripts are not seen as constituents of the library. They are not published and indexed, so they cannot be searched or browsed using \HELM{} tools. -However, they play a central role for the mainteinance of the library. +However, they play a central role for the maintenance of the library. Indeed, once a notion is invalidated, the only way to restore it is to fix the possibly broken script that used to generate it. Moreover, during the authoring phase, scripts are a natural way to @@ -846,12 +844,12 @@ aliases}. Disambiguation aliases are one-to-many mappings from ambiguous expressions to partially specified terms, which are part of the runtime status of \MATITA. They can be provided by users with the \texttt{alias} statement, but are usually automatically added when evaluating \texttt{include} statements -(\emph{implicit aliases}). Aliases implicitely inferred during disambiguation +(\emph{implicit aliases}). Aliases implicitly inferred during disambiguation are remembered as well. Moreover, \MATITA{} does it best to ensure that terms which require interactive choice are saved in batch compilable format. Thus, after evaluating the above theorem the script will be changed to the following snippet (assuming that the interpretation of \OP{<} over integers has been -choosed): +chosen): \begin{grafite} alias symbol "lt" = "integer 'less than'". @@ -860,7 +858,7 @@ theorem Zlt_compat: \end{grafite} But how are disambiguation aliases used? Since they come from the parts of the -library explicitely included we may be tempted of using them as the only +library explicitly included we may be tempted of using them as the only available interpretations. This would speed up the disambiguation, but may fail. Consider for example: @@ -934,7 +932,7 @@ theorem power_deriv: and suppose there exists a \texttt{R \TEXMACRO{to} nat \TEXMACRO{to} R} interpretation for \OP{\^}, and a real number interpretation for \OP{*}. -Mathematichans would write the term that way since it is well known that the +Mathematicians would write the term that way since it is well known that the natural number \texttt{n} could be ``injected'' in \IR{} and considered a real number for the purpose of real multiplication. The refiner of \MATITA{} supports \emph{implicit coercions} for this reason: given as input the above content @@ -1000,7 +998,7 @@ preserves the consistency and the availability of the library using the \WHELP{} technology, in response to the user alteration or removal of mathematical objects. -As already sketched in Sec.~\ref{sec:fullyspec} what we generate +As already sketched in Sect.~\ref{sec:fullyspec} what we generate from a script is split among two storage media, a classical filesystem and a relational database. The former is used to store the XML encoding of the objects defined in the script, the @@ -1117,9 +1115,9 @@ names occurring in a left to right traversal of the statement; \item all identifiers should (but this is not strictly compulsory) separated by an underscore, \item identifiers in two different hypothesis, or in an hypothesis -and in the conlcusion must be separated by the string ``\verb+_to_+''; +and in the conclusion must be separated by the string ``\verb+_to_+''; \item the identifier may be followed by a numerical suffix, or a -single or duoble apostrophe. +single or double apostrophe. \end{itemize} Take for instance the theorem @@ -1142,7 +1140,7 @@ Then, you may state the symmetry of equality as \[ \forall A:Type. symmetric \;A\;(eq \; A)\] and \verb+symmetric_eq+ is valid \MATITA{} name for such a theorem. So, somehow unexpectedly, the introduction of semi-rigid naming convention -has an important benefical effect on the global organization of the library, +has an important beneficial effect on the global organization of the library, forcing the user to define abstract notions and properties before using them (and formalizing such use). @@ -1194,7 +1192,7 @@ natural language, automatically generated from the low-level lambda-terms, using techniques inspired by \cite{natural,YANNTHESIS} and already described in~\cite{remathematization}. -Note that the syntax used in the script view is \TeX-like, however unicode is +Note that the syntax used in the script view is \TeX-like, however Unicode is fully supported so that mathematical glyphs can be input as such. \begin{figure}[!ht] @@ -1320,7 +1318,7 @@ second searches the $\NT{wanted}$ term starting from these roots. $\NT{sequent\_path}$ starting from a visual selection. \NOTE{Questo ancora non va in matita} - A $\NT{multipath}$ is a CiC term in which a special constant $\%$ + A $\NT{multipath}$ is a CIC term in which a special constant $\%$ is allowed. The roots of discharged subterms are marked with $?$, while $\%$ is used to select roots. The default $\NT{multipath}$, the one that @@ -1376,7 +1374,7 @@ aware that the notation $m+n=n$ hides the term $(eq~nat~(m+n)~n)$, so that the pattern selects only the third argument of $eq$. The experienced user may also write by hand a concise pattern -to change at once all the occcurrences of $n$ in the hypothesis $H$: +to change at once all the occurrences of $n$ in the hypothesis $H$: \begin{grafite} change in H match n with (O + n). \end{grafite} @@ -1405,7 +1403,7 @@ in un pattern phase1only come faccio nell'ultimo esempio. lo si fa con una pattern\_of(select(pattern))} \subsubsection{Comparison with \COQ{}} -\COQ{} has a two different ways of restricting the application of tactis to +\COQ{} has two different ways of restricting the application of tactics to subterms of the sequent, both relaying on the same special syntax to identify a term occurrence. @@ -1418,7 +1416,7 @@ with pattern and do not accept directly this special syntax. The base idea is that to identify a subterm of the sequent we can write it and say that we want, for example, the third and the fifth -occurce of it (counting from left to right). In our previous example, +occurrences of it (counting from left to right). In our previous example, to change only the left part of the equivalence, the correct command is \begin{grafite} @@ -1461,7 +1459,7 @@ integrations) or even puts them inside a bidimensional matrix. In these cases using the mouse to select the wanted term is probably the only way to tell the system exactly what you want to do. -One of the goals of \MATITA{} is to use modern publishing techiques, and +One of the goals of \MATITA{} is to use modern publishing techniques, and adopting a method for restricting tactics application domain that discourages using heavy math notation, would definitively be a bad choice. @@ -1469,8 +1467,8 @@ using heavy math notation, would definitively be a bad choice. \subsection{Tacticals} There are mainly two kinds of languages used by proof assistants to recorder proofs: tactic based and declarative. We will not investigate the philosophy -aroud the choice that many proof assistant made, \MATITA{} included, and we -will not compare the two diffrent approaches. We will describe the common +around the choice that many proof assistant made, \MATITA{} included, and we +will not compare the two different approaches. We will describe the common issues of the tactic-based language approach and how \MATITA{} tries to solve them. @@ -1688,7 +1686,7 @@ totient.ma& & \\ \end{figure} We do not plan to maintain the library in a centralized way, -as most of the systems do. On the contary we are currently +as most of the systems do. On the contrary we are currently developing wiki-technologies to support a collaborative development of the library, encouraging people to expand, modify and elaborate previous contributions.