From: Stefano Zacchiroli Date: Wed, 16 Nov 2005 16:38:42 +0000 (+0000) Subject: snapshot X-Git-Tag: V_0_7_2_3~61 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=03ba06211a6e1edb8472e785d2024a26992f2c0e;p=helm.git snapshot --- diff --git a/helm/papers/matita/matita.tex b/helm/papers/matita/matita.tex index 4a74110b4..7b849c928 100644 --- a/helm/papers/matita/matita.tex +++ b/helm/papers/matita/matita.tex @@ -49,6 +49,7 @@ \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}} @@ -212,6 +213,7 @@ reduce our code in sensible way).\NOTE{righe\\\COQ{}} \ASSIGNEDTO{zack} \subsection{metavariabili} +\label{sec:metavariables} \ASSIGNEDTO{csc} \subsection{pattern} @@ -225,7 +227,8 @@ reduce our code in sensible way).\NOTE{righe\\\COQ{}} \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@{}} @@ -234,7 +237,7 @@ reduce our code in sensible way).\NOTE{righe\\\COQ{}} & | & 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} \\ @@ -323,6 +326,7 @@ because some nodes of the content encoding admit more that one CIC encoding, 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 @@ -397,57 +401,84 @@ disambiguation domain may refer to different constants like the addition over 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.