From 34dbef19bdb8726cab7af14bff72dd4573c1d365 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 23 Jan 2006 12:13:00 +0000 Subject: [PATCH] completed disambiguation part --- helm/papers/matita/matita2.tex | 35 ++++++++++++++++------------------ 1 file changed, 16 insertions(+), 19 deletions(-) diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex index 84c98b484..2a5f3fd2e 100644 --- a/helm/papers/matita/matita2.tex +++ b/helm/papers/matita/matita2.tex @@ -1041,6 +1041,16 @@ an interpretation for one instances does not constraint the choice for the others). For this reason we always attempt a fresh instances pass only after attempting a non-fresh one. +\paragraph{One-shot aliases} Disambiguation aliases as seen so far are +instance-independent. However, aliases obtained as a result of a disambiguation +pass which uses fresh instances ought to be instance-dependent, that is: to +ensure a term can be disambiguated in a batch fashion we may need to state that +an \emph{i}-th instance of a symbol should be mapped to a given partially +specified term. Instance-depend aliases are meaningful only for the term whose +disambiguation generated it. For this reason we call them \emph{one-shot +aliases} and \MATITA{} doesn't use it to disambiguate further terms down in the +script. + \subsubsection{Implicit coercions} Let's now consider a (rather hypothetical) theorem about derivation: @@ -1082,19 +1092,14 @@ attempting passes with implicit coercions. \subsubsection{Disambiguation passes} -Summarizing, we perform multiple disambiguation passes for each presentation -level term and in each of them we have 3 degree of freedom: disambiguation -aliases (mono/multi/library), operator instances (shared/fresh), and implicit -coercions (enabled/disabled). This would lead to up to 12 different -disambiguation passes with ordering to be decided upon. Our choice in \MATITA{} -is depicted in Tab.~\ref{tab:disambpasses}. - -\TODO{spiegazione della tabella} +According to the criteria described above in \MATITA{} we choose to perform the +sequence of disambiguation passes depicted in Tab.~\ref{tab:disambpasses}. In +our experience that choice implements a good trade off among disambiguation time +and admitted ambiguity in terms input by users. -\begin{table} - \caption{Disambiguation passes.\strut} +\begin{table}[ht] + \caption{Sequence of disambiguation passes used in \MATITA.\strut} \label{tab:disambpasses} - \footnotesize \begin{center} \begin{tabular}{c|c|c|c} \multicolumn{1}{p{1.5cm}|}{\centering\raisebox{-1.5ex}{\textbf{Pass}}} @@ -1113,14 +1118,6 @@ is depicted in Tab.~\ref{tab:disambpasses}. \end{center} \end{table} -\TODO{alias one shot} - - - - - - - \subsection{Patterns} serve una intro che almeno cita il widget (per i patterns) e che fa -- 2.39.2