\end{center}}
\newcommand{\ASSIGNEDTO}[1]{\textbf{Assigned to:} #1}
+\newcommand{\FILE}[1]{\texttt{#1}}
\newcommand{\NOTE}[1]{\marginpar{\scriptsize #1}}
\newcommand{\TODO}[1]{\textbf{TODO: #1}}
\ASSIGNEDTO{zack}
\subsection{metavariabili}
+\label{sec:metavariables}
\ASSIGNEDTO{csc}
\subsection{pattern}
\ASSIGNEDTO{zack}
\begin{table}
- \caption{\label{tab:termsyn} Concrete syntax of CIC terms: built-in notation\strut}
+ \caption{\label{tab:termsyn} Concrete syntax of CIC terms: built-in
+ notation\strut}
\hrule
\[
\begin{array}{@{}rcll@{}}
& | & n & \mbox{(number)} \\
& | & s & \mbox{(symbol)} \\
& | & \mathrm{URI} & \mbox{(URI)} \\
- & | & \verb+?+ & \mbox{(implicit)} \\
+ & | & \verb+_+ & \mbox{(implicit)}\TODO{sync} \\
& | & \verb+?+n~[\verb+[+~\{\NT{subst}\}~\verb+]+] & \mbox{(meta)} \\
& | & \verb+let+~\NT{ptname}~\verb+\def+~\NT{term}~\verb+in+~\NT{term} \\
& | & \verb+let+~\NT{kind}~\NT{defs}~\verb+in+~\NT{term} \\
invalidating requirement (2).
\begin{example}
+ \label{ex:disambiguation}
Consider the term at the concrete syntax level \texttt{\TEXMACRO{forall} x. x +
ln 1 = x} of Fig.~\ref{fig:inputphase}(a), it can be the type of a lemma the
natural numbers \URI{cic:/matita/nat/plus/plus.con} or that over real numbers of
the \COQ{} standard library \URI{cic:/Coq/Reals/Rdefinitions/Rplus.con}.
-For each possible way of mapping a symbol application to a CIC term, \MATITA{}
-knows a \emph{symbol interpretation function} which, when applied to a symbol
-and its arguments, returns a CIC term. The disambiguation domain for a given
-operator is built applying to the symbol and its arguments all available symbol
-interpretation functions in turn.
+For each possible way of mapping an operator application to a CIC term,
+\MATITA{} knows an \emph{operator interpretation function} which, when applied
+to an operator and its arguments, returns a CIC term. The disambiguation domain
+for a given operator is built applying to the operator and its arguments all
+available operator interpretation functions in turn.
+
+Operator interpretation functions could be added using the
+\texttt{interpretation} statement. For example, among the first line of the
+script \FILE{matita/library/logic/equality.ma} from the \MATITA{} standard
+library we read:
\begin{grafite}
- foo
- bar
- baz
+interpretation "leibnitz's equality"
+ 'eq x y =
+ (cic:/matita/logic/equality/eq.ind#xpointer(1/1) _ x y).
\end{grafite}
-\TODO{FINQUI, il resto \`e copy and paste dal Whelp paper \dots}
-
-Note that given a content level term with more than one sources of ambiguity,
-not all possible disambiguation choices are valid: for example, given the input
-\texttt{1+1} we must choose an interpretation of \texttt{+} which is typable in
-CIC according to the chosen interpretation for \texttt{1}; choosing as
-\texttt{+} the addition over natural numbers and as \texttt{1} the real number
-$1$ will lead to a type error.
-
-A \emph{disambiguation algorithm} takes as input an ambiguous term and return a
-fully determined CIC term. The \emph{naive disambiguation algorithm} takes as
-input an ambiguous term $t$ and proceeds as follows:
+Evaluating it in \MATITA{} will add an operator interpretation function for the
+binary operator \texttt{eq} which expands to the CIC term on the right hand side
+of the statement. That CIC term can be written using only built-in concrete
+syntax, can contain no ambiguity source; still, it can refer to operator
+arguments bound on the left hand side and can contain implicit terms (denoted
+with \texttt{\_}) which will be expanded to fresh metavariables. The latter
+feature is used in the example above for the first argument of Leibniz's
+polymorhpic equality.
+
+\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
+of ambiguity, not all possible combination of interpretation lead to a typable
+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\bot$, the combination of interpretation which led to $c$
+can coexists.
+
+The \emph{naive disambiguation algorithm} takes as input a content level term
+$t$ and proceeds as follows:
\begin{enumerate}
\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.
+ 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\}$
-% such that $\forall i\in\mathit{Dom}(t),\exists\phi_j\in\Phi,i=j$
- 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
- type-check them, keep only typable interpretations (i.e. interpretations that
- determine typable terms).
+ \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\bot$ (i.e. interpretations that determine
+ typable terms).
\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$ let the user choose one of the $n$ interpretations and returns the
+ 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.
\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 \WHELP{} is far more efficient being, in the
+The actual algorithm used in \MATITA{} is far more efficient being, in the
average case, linear in the number of ambiguity sources.
+\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.
projects / helm.git / commitdiff