\end{center}}
\newcounter{example}
-\newenvironment{example}{\stepcounter{example}\emph{Example} \arabic{example}.}
+\newenvironment{example}{\stepcounter{example}\vspace{0.5em}\noindent\emph{Example} \arabic{example}.}
{}
\newcommand{\ASSIGNEDTO}[1]{\textbf{Assigned to:} #1}
\newcommand{\FILE}[1]{\texttt{#1}}
\subsubsection{Disambiguation algorithm}
-\NOTE{assumo che si sia gia' parlato di refine}
-
A \emph{disambiguation algorithm} takes as input a content level term and return
a fully determined CIC term. The key observation on which a disambiguation
algorithm is based is that given a content level term with more than one sources
CIC term. In the term of Ex.~\ref{ex:disambiguation} for instance the
interpretation of \texttt{ln} as a function from \IR to \IR and the
interpretation of \texttt{1} as the Peano number $1$ can't coexists. The notion
-of ``can't coexists'' in the disambiguation of \MATITA{} is inherited from the
-refiner described in Sect.~\ref{sec:metavariables}: as long as
-$\mathit{refine}(c)\neq\epsilon$, the combination of interpretation which led to
-$c$
-can coexists.
+of ``can't coexists'' in the disambiguation of \MATITA{} is defined on top of
+the \emph{refiner} for CIC terms described in~\cite{csc-phd}.
-The \emph{naive disambiguation algorithm} takes as input a content level term
-$t$ and proceeds as follows:
+Briefly, a refiner is a function whose input is an \emph{incomplete CIC term}
+$t_1$ --- i.e. a term where metavariables occur (Sect.~\ref{sec:metavariables}
+--- and whose output is either:\NOTE{descrizione sommaria del refiner, pu\'o
+essere spostata altrove}
\begin{enumerate}
+
+ \item an incomplete CIC term $t_2$ where $t_2$ is a well-typed term obtained
+ assigning a type to each metavariable in $t_1$ (in case of dependent types,
+ instantiation of some of the metavariable occurring in $t_1$ may occur as
+ well);
- \item Create disambiguation domains $\{D_i | i\in\mathit{Dom}(t)\}$, where
- $\mathit{Dom}(t)$ is the set of ambiguity sources of $t$. Each $D_i$ is a set
- of CIC terms and can be built as described above.
-
- \item Let $\Phi = \{\phi_i | {i\in\mathit{Dom}(t)},\phi_i\in D_i\}$ be an
- interpretation for $t$. Given $t$ and an interpretation $\Phi$, a CIC term is
- fully determined. Iterate over all possible interpretations of $t$ and refine
- the corresponding CIC terms, keep only interpretations which lead to CIC terms
- $c$ s.t. $\mathit{refine}(c)\neq\epsilon$ (i.e. interpretations that determine
- typable terms).
+ \item $\epsilon$, meaning that no well-typed term could be obtained via
+ assignment of type to metavariable in $t_1$ and their instantiation;
- \item Let $n$ be the number of interpretations who survived step 2. If $n=0$
- signal a type error. If $n=1$ we have found exactly one CIC term corresponding
- to $t$, returns it as output of the disambiguation phase. If $n>1$ we have
- found many different CIC terms which can correspond to the content level term,
- let the user choose one of the $n$ interpretations and returns the
- corresponding term.
+ \item $\bot$, meaning that the refiner is unable to decide whether of the two
+ cases above apply (refinement is semi-decidable).
\end{enumerate}
-The above algorithm is highly inefficient since the number of possible
-interpretations $\Phi$ grows exponentially with the number of ambiguity sources.
-The actual algorithm used in \MATITA{} is far more efficient being, in the
-average case, linear in the number of ambiguity sources.
-
-The efficient algorithm --- thoroughly described along with an analysis of its
-complexity in~\cite{disambiguation} --- exploit the refiner and the metavariable
-extension (Sect.~\ref{sec:metavariables}) of the calculus used in \MATITA.
-
-\TODO{FINQUI}
-
-The efficient algorithm can be applied if the logic can be extended with
-metavariables and a refiner can be implemented. This is the case for CIC and
-several other logics.
-\emph{Metavariables}~\cite{munoz} are typed, non linear placeholders that can
-occur in terms; $?_i$ usually denotes the $i$-th metavariable, while $?$ denotes
-a freshly created metavariable. A \emph{refiner}~\cite{McBride} is a
-function whose input is a term with placeholders and whose output is either a
-new term obtained instantiating some placeholder or $\epsilon$, meaning that no
-well typed instantiation could be found for the placeholders occurring in
-the term (type error).
-
-The efficient algorithm starts with an interpretation $\Phi_0 = \{\phi_i |
-\phi_i = ?, i\in\mathit{Dom}(t)\}$,
-which associates a fresh metavariable to each
-source of ambiguity. Then it iterates refining the current CIC term (i.e. the
-term obtained interpreting $t$ with $\Phi_i$). If the refinement succeeds the
-next interpretation $\Phi_{i+1}$ will be created \emph{making a choice}, that is
-replacing a placeholder with one of the possible choice from the corresponding
-disambiguation domain. The placeholder to be replaced is chosen following a
-preorder visit of the ambiguous term. If the refinement fails the current set of
-choices cannot lead to a well-typed term and backtracking is attempted.
-Once an unambiguous correct interpretation is found (i.e. $\Phi_i$ does no
-longer contain any placeholder), backtracking is attempted
-anyway to find the other correct interpretations.
-
-The intuition which explain why this algorithm is more efficient is that as soon
-as a term containing placeholders is not typable, no further instantiation of
-its placeholders could lead to a typable term. For example, during the
-disambiguation of user input \texttt{\TEXMACRO{forall} x. x*0 = 0}, an
-interpretation $\Phi_i$ is encountered which associates $?$ to the instance
-of \texttt{0} on the right, the real number $0$ to the instance of \texttt{0} on
-the left, and the multiplication over natural numbers (\texttt{mult} for short)
-to \texttt{*}. The refiner will fail, since \texttt{mult} require a natural
-argument, and no further instantiation of the placeholder will be tried.
-
-If, at the end of the disambiguation, more than one possible interpretations are
-possible, the user will be asked to choose the intended one (see
-Fig.~\ref{fig:disambiguation}).
-
-\begin{figure}[htb]
-% \centerline{\includegraphics[width=0.9\textwidth]{disambiguation-1}}
- \caption{\label{fig:disambiguation} Disambiguation: interpretation choice}
-\end{figure}
+On top of a CIC refiner \MATITA{} implement an efficient disambiguation
+algorithm, which is outlined below. It takes as input a content level term $c$
+and proceeds as follows:
+
+\begin{enumerate}
+
+ \item Create disambiguation domains $\{D_i | i\in\mathit{Dom}(c)\}$, where
+ $\mathit{Dom}(c)$ is the set of ambiguity sources of $c$. Each $D_i$ is a set
+ of CIC terms and can be built as described above.
-Details of the disambiguation algorithm of \WHELP{} can
-be found in~\cite{disambiguation}, where an equivalent algorithm
-that avoids backtracking is also presented.
+ \item An \emph{interpretation} $\Phi$ for $c$ is a map associating an
+ incomplete CIC term to each ambiguity source of $c$. Given $c$ and one of its
+ interpretations an incomplete CIC term is fully determined replacing each
+ ambiguity source of $c$ with its mapping in the interpretation and injecting
+ the remaining structure of the content level in the CIC level (e.g. replacing
+ the application of the content level with the application of the CIC level).
+ This operation is informally called ``interpreting $c$ with $\Phi$''.
+
+ Create an initial interpretation $\Phi_0 = \{\phi_i | \phi_i = \_,
+ i\in\mathit{Dom}(c)\}$, which associates a fresh metavariable to each source
+ of ambiguity of $c$. During this step, implicit terms are expanded to fresh
+ metavariables as well.
+
+ \item Refine the current incomplete CIC term (i.e. the term obtained
+ interpreting $t$ with $\Phi_i$).
+
+ If the refinement succeeds or is undetermined the next interpretation
+ $\Phi_{i+1}$ will be created \emph{making a choice}, that is replacing in the
+ current interpretation one of the metavariable appearing in $\Phi_i$ with one
+ of the possible choice from the corresponding disambiguation domain. The
+ metavariable to be replaced is chosen following a preorder visit of the
+ ambiguous term. Then, step 3 is attempted again with the new interpretation.
+
+ If the refinement fails the current set of choices cannot lead to a well-typed
+ term and backtracking of the current interpretation is attempted.
+
+ \item Once an unambiguous correct interpretation is found (i.e. $\Phi_i$ does
+ no longer contain any placeholder), backtracking is attempted anyway to find
+ the other correct interpretations.
+
+ \item Let $n$ be the number of interpretations who survived step 4. If $n=0$
+ signal a type error. If $n=1$ we have found exactly one (incomplete) CIC term
+ corresponding to the content level term $c$, returns it as output of the
+ disambiguation phase. If $n>1$ we have found many different (incomplete) CIC
+ terms which can correspond to the content level term, let the user choose one
+ of the $n$ interpretations and returns the corresponding term.
+
+\end{enumerate}
+The efficiency of this algorithm resides in the fact that as soon as an
+incomplete CIC term is not typable, no further instantiation of the
+metavariables of the corresponding interpretation is attemped.
+% For example, during the disambiguation of the user input
+% \texttt{\TEXMACRO{forall} x. x*0 = 0}, an interpretation $\Phi_i$ is
+% encountered which associates $?$ to the instance of \texttt{0} on the right,
+% the real number $0$ to the instance of \texttt{0} on the left, and the
+% multiplication over natural numbers (\texttt{mult} for short) to \texttt{*}.
+% The refiner will fail, since \texttt{mult} require a natural argument, and no
+% further instantiation of the placeholder will be tried.
+
+Details of the disambiguation algorithm along with an analysis of its complexity
+can be found in~\cite{disambiguation}, where a formulation without backtracking
+(corresponding to the actual \MATITA{} implementation) is also presented.
+
+\subsubsection{Disambiguation stages}
\subsection{notazione}
\label{sec:notation}
projects / helm.git / blobdiff