From: Claudio Sacerdoti Coen Date: Fri, 27 Jan 2006 12:03:43 +0000 (+0000) Subject: Cambiamenti nella parte sulla disambiguazione. X-Git-Tag: make_still_working~7749 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=b54d416a511fcb2a01200a545506f83c70d24b96;p=helm.git Cambiamenti nella parte sulla disambiguazione. --- diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex index 2e3944bb5..c6637afd5 100644 --- a/helm/papers/matita/matita2.tex +++ b/helm/papers/matita/matita2.tex @@ -234,8 +234,8 @@ standard way to interact with the system. Several procedural proof assistants have either adopted or cloned Proof General as their main user interface. The authoring interface of \MATITA{} is a clone of the Proof General interface. +TODO \begin{itemize} - \item scelta del sistema fondazional. \item sistema indipendente (da \COQ) \item compatibilit\`a con sistemi legacy \end{itemize} @@ -407,7 +407,7 @@ content level terms; presentation level terms. providing a mapping from logical names (URIs) to the physical location of a notion (an URL). The \texttt{urimanager} \component{} provides the URI data type and several utility functions over URIs. The - \texttt{cic\_proof\_checking} \component{} calls the \GETTER + \texttt{cic\_proof\_checking} \component{} calls the \GETTER{} \component{} every time it needs to retrieve the definition of a mathematical notion referenced by a term that is being type-checked. @@ -794,65 +794,38 @@ expressiveness. \subsubsection{Disambiguation aliases} \label{sec:disambaliases} -Let us start with the definition of the ``strictly greater then'' notion over -(Peano) natural numbers. -\begin{grafite} -include "nat/nat.ma". -.. -definition gt: nat \to nat \to Prop \def - \lambda n, m. m < n. -\end{grafite} - -The \texttt{include} statement adds the requirement that the part of the library -defining the notion of natural numbers should be defined before -processing what follows. Note indeed that the algorithm presented -in~\cite{disambiguation} does not describe where interpretations for ambiguous -expressions come from, since it is application-specific. As a first -approximation, we will assume that in \MATITA{} they come from the library (i.e. -all interpretations available in the library are used) and the \texttt{include} -statements are used to ensure the availability of required library slices (see -Sect.~\ref{sec:libmanagement}). - -While processing the \texttt{gt} definition, \MATITA{} has to disambiguate two -terms: its type and its body. Being available in the required library only one -interpretation both for the unbound identifier \texttt{nat} and for the -\OP{<} operator, and being the resulting partially specified term refinable, -both type and body are easily disambiguated. - -Now suppose we have defined integers as signed natural numbers, and that we want -to prove a theorem about an order relationship already defined on them (which of -course overload the \OP{<} operator): +Consider the following command to state a theorem over integer numbers. \begin{grafite} -include "Z/z.ma". -.. theorem Zlt_compat: \forall x, y, z. x < y \to y < z \to x < z. \end{grafite} -Since integers are defined on top of natural numbers, the part of the library -concerning the latters is available when disambiguating \texttt{Zlt\_compat}'s -type. Thus, according to the disambiguation algorithm, two different partially -specified terms could be associated to it. At first, this might not be seen as a -problem, since the user is asked and can choose interactively which of the two -she had in mind. However in the long run it has the drawbacks of inhibiting -batch compilation of the library (a technique used in \MATITA{} for behind the -scene compilation when needed, e.g. when an \texttt{include} is issued) and -yields to poor user interaction (imagine how tedious would be to be asked for a -choice each time you re-evaluate \texttt{Zlt\_compat}!). - -For this reason we added to \MATITA{} the concept of \emph{disambiguation -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 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 -chosen): +The symbol ``\texttt{<}'' is likely to be overloaded in the library +(at least over natural numbers). +Thus, according to the disambiguation algorithm, two different +refinable partially specified terms could be associated to it. +\MATITA{} asks the user what interpretation he meant. However, to avoid +posing the same question in case of a future re-execution (e.g. undo/redo), +the choice must be recorded. Scripts need to be re-executed after invalidation. +Therefore the choice record must be permanently stored somewhere. The most +natural place is in the script itself. + +In \MATITA{} disambiguation is governed by \emph{disambiguation aliases}. +They are mappings, stored in the library, from ambiguity sources +(identifiers, symbols and literal numbers at the content level) to partially +specified terms. In case of overloaded sources there exists multiple aliases +with the same source. It is possible to record \emph{disambiguation +preferences} to select one of the aliases of an overloaded source. + +Preferences can be explicitely given in the script (using the +misleading \texttt{alias} commands), but +are also implicitly added when a new concept is introduced (\emph{implicit +preferences}) or after a sucessfull disambiguation that did not require +user interaction. Explicit preferences are added automatically by \MATITA{} to +record the disambiguation choices of the user. For instance, after the +disambiguation of the command above, the script is altered as follows: \begin{grafite} alias symbol "lt" = "integer 'less than'". @@ -860,15 +833,53 @@ theorem Zlt_compat: \forall x, y, z. x < y \to y < z \to x < z. \end{grafite} -But how are disambiguation aliases used? Since they come from the parts of the -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: +The ``alias'' command in the example sets the preferred alias for the +``\texttt{lt}'' symbol. + +Implicit preferences for new concepts are set since a concept just defined is +likely to be the preferred one in the rest of the script. Implicit preferences +learned from disambiguation of previous commands grant the coherence of +the disambiguation in the rest of the script and speed up disambiguation +reducing the search space. + +Disambiguation preferences are included in the lexicon status +(see Sect.~\ref{???}) that is part of the authoring interface status. +Unlike aliases, they are not part of the library. + +When starting a new authoring session the set of disambiguation preferences +is empty. Until it contains a preference for each overloaded symbol to be +used in the script, the user can be faced with questions from the disambiguator. +To reduce the likelyhood of user interactions, we introduced +the \texttt{include} command. With \texttt{include} it is possible to import +at once in the current session the set of preferences that was in effect +at the end of the execution of a given script. + +Preferences can be changed. For instance, at the start of the development +of integer numbers the preference for the symbol ``\texttt{<}'' is likely +to be the one over natural numbers; sooner or later it will be set to the one +over integer numbers. + +Nothing forbids the set of preferences to become incoherent. For this reason +the disambiguator cannot always respect the user preferences. +For example consider: \begin{grafite} -theorem lt_mono: \forall x, y, k. x < y \to x < y + k. +theorem Zlt_mono: \forall x, y, k. x < y \to x < y + k. \end{grafite} +No refinable partially specified term corresponds to the preferences: +\OP{+} over natural numbers, \OP{<} over integer numbers. +When the disambiguator fails, disambiguation is tried again with a less +strict set of preferences. Thus disambiguation is organized in +multiple \emph{passes}. In the first pass, called \emph{mono-preferences}, +we consider only the aliases corresponding to the current preferences. +In the second pass, called \emph{multi-preferences}, +we consider every alias corresponding to a current or past preference. +For instance, in the example above disambiguation succeeds in the +multi-preference pass +TODO: CAMBIATO SOLO FINO A QUI + + and suppose that the \OP{+} operator is defined only on natural numbers. If the alias for \OP{<} points to the integer version of the operator, no refinable partially specified term matching the term could be found. @@ -1251,6 +1262,7 @@ applications. \end{center} \end{figure} +TODO: referenziarli e spostarli nella parte sulla libreria? \begin{figure}[!ht] \begin{center} \includegraphics[width=0.30\textwidth]{pics/cicbrowser-screenshot-browsing}