-\documentclass{kluwer}
+\documentclass[draft]{kluwer}
\usepackage{color}
\usepackage{graphicx}
% \usepackage{amssymb,amsmath}
\definecolor{gray}{gray}{0.85} % 1 -> white; 0 -> black
\newcommand{\NT}[1]{\langle\mathit{#1}\rangle}
\newcommand{\URI}[1]{\texttt{#1}}
+\newcommand{\OP}[1]{``\texttt{#1}''}
%{\end{SaveVerbatim}\setlength{\fboxrule}{.5mm}\setlength{\fboxsep}{2mm}%
\newenvironment{grafite}{\VerbatimEnvironment
\newcommand{\NOTE}[1]{\ednote{#1}{foo}}
\newcommand{\TODO}[1]{\textbf{TODO: #1}}
+\newcounter{pass}
+\newcommand{\PASS}{\stepcounter{pass}\arabic{pass}}
+
\newsavebox{\tmpxyz}
\newcommand{\sequent}[2]{
\savebox{\tmpxyz}[0.9\linewidth]{
The origins of \MATITA{} go back to 1999. At the time we were mostly
interested to develop tools and techniques to enhance the accessibility
via Web of formal libraries of mathematics. Due to its dimension, the
-library of the \COQ{}\cite{CoqManual} proof assistant (of the order of 35'000 theorems)
+library of the \COQ~\cite{CoqManual} proof assistant (of the order of 35'000 theorems)
was choosed as a privileged test bench for our work, although experiments
have been also conducted with other systems, and notably
with \NUPRL{}\cite{nuprl-book}.
\begin{figure}[t]
\begin{center}
\includegraphics[width=0.9\textwidth]{librariesCluster.ps}
- \caption{\label{fig:libraries}\MATITA{} libraries}
+ \caption{\MATITA{} libraries}
+ \label{fig:libraries}
\end{center}
\end{figure}
implemented in the \texttt{disambiguation} library of Fig.~\ref{fig:libraries}
and presented in~\cite{disambiguation}. In this section we present how to use
such an algorithm in the context of the development of a library of formalized
-mathematics. We proceed by examples took from the \MATITA{} standard library.
+mathematics. We will see that using multiple passes of the algorithm, varying
+some of its parameters, helps in keeping the input terse without sacrificing
+expressiveness.
\subsubsection{Disambiguation aliases}
\end{grafite}
The \texttt{include} statement adds the requirement that the part of the library
-defining the notion of (Peano) natural numbers should be defined before
+defining the notion of natural numbers should be defined before
processing the following definition. 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
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
-\texttt{<} operator, and being the resulting partially specified term refinable,
+\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 Peano numbers, and that we want
+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 \texttt{<} operator):
+course overload the \OP{<} operator):
\begin{grafite}
include "Z/z.ma".
\forall x, y, z. x < y \to y < z \to x < z.
\end{grafite}
-Since integers are defined on top of Peano numbers, the part of the library
+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
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}). 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 \texttt{<} over integers
-has been choosed):
+(\emph{implicit aliases}). Aliases implicitely 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
+choosed):
\begin{grafite}
-alias symbol "lt" (instance 0) = "integer 'less than'".
+alias symbol "lt" = "integer 'less than'".
theorem Zlt_compat:
\forall x, y, z. x < y \to y < z \to x < z.
\end{grafite}
theorem lt_mono: \forall x, y, k. x < y \to x < y + k.
\end{grafite}
-and suppose that the \texttt{+} operator is defined only on Peano numbers. If
-the alias for \texttt{<} points to the integer version of the operator, no
+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.
For this reason we choosed to attempt \emph{multiple disambiguation passes}. A
first pass attempt to disambiguate using the last available disambiguation
-aliases, in case of failure the next pass try again the disambiguation
-forgetting the aliases and using the whole library to retrieve interpretation
-for ambiguous expressions. Since the latter pass may lead to too many choices we
-intertwined an additional pass among the two which use as interpretations all
-the aliases coming for included parts of the library (this is the reason why
-aliases are \emph{one-to-many} mappings instead of one-to-one). This choice
+aliases (\emph{mono aliases} pass), in case of failure the next pass try again
+the disambiguation forgetting the aliases and using the whole library to
+retrieve interpretation for ambiguous expressions (\emph{library aliases} pass).
+Since the latter pass may lead to too many choices we intertwined an additional
+pass among the two which use as interpretations all the aliases coming for
+included parts of the library (\emph{multi aliases} phase). This is the reason
+why aliases are \emph{one-to-many} mappings instead of one-to-one. This choice
turned out to be a well-balanced trade-off among performances (earlier passes
fail quickly) and degree of ambiguity supported for presentation level terms.
\subsubsection{Operator instances}
+Let's suppose now we want to define a theorem relating ordering relations on
+natural and integer numbers. The way we would like to write such a theorem (as
+we can read it in the \MATITA{} standard library) is:
+
+\begin{grafite}
+include "Z/z.ma".
+include "nat/orders.ma".
+..
+theorem lt_to_Zlt_pos_pos:
+ \forall n, m: nat. n < m \to pos n < pos m.
+\end{grafite}
+
+Unfortunately, none of the passes described above is able to disambiguate its
+type, no matter how aliases are defined. This is because the \OP{<} operator
+occurs twice in the content level term (it has two \emph{instances}) and two
+different interpretation for it have to be used in order to obtain a refinable
+partially specified term. To address this issue, we have the ability to consider
+each instance of a single symbol as a different ambiguous expression in the
+content level term, and thus we can assign a different interpretation to each of
+them. A disambiguation pass which exploit this feature is said to be using
+\emph{fresh instances}.
+
+Fresh instances lead to a non negligible performance loss (since the choice of
+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.
+
+\subsubsection{Implicit coercions}
+
+Let's now consider a (rather hypothetical) theorem about derivation:
+
+\begin{grafite}
+theorem power_deriv:
+ \forall n: nat, x: R. d x ^ n dx = n * x ^ (n - 1).
+\end{grafite}
+
+and suppose there exists a \texttt{R \TEXMACRO{to} nat \TEXMACRO{to} R}
+interpretation for \OP{\^}, and a real number interpretation for \OP{*}.
+Mathematichians would write the term that way since it is well known that the
+natural number \texttt{n} could be ``injected'' in \IR{} and considered a real
+number for the purpose of real multiplication. The refiner of \MATITA{} supports
+\emph{implicit coercions} for this reason: given as input the above content
+level term, it will return a partially specified term where in place of
+\texttt{n} the application of a coercion from \texttt{nat} to \texttt{R} appears
+(assuming it has been defined as such of course).
+
+Nonetheless coercions are not always desirable. For example, in disambiguating
+\texttt{\TEXMACRO{forall} x: nat. n < n + 1} we don't want the term which uses
+two coercions from \texttt{nat} to \texttt{R} around \OP{<} arguments to show up
+among the possible partially specified term choices. For this reason in
+\MATITA{} we always try first a disambiguation pass which require the refiner
+not to use the coercions and only in case of failure we attempt a
+coercion-enabled pass.
+
+It is interesting to observe also the relationship among operator instances and
+implicit coercions. Consider again the theorem \texttt{lt\_to\_Zlt\_pos\_pos},
+which \MATITA{} disambiguated using fresh instances. In case there exists a
+coercion from natural numbers to (positive) integers (which indeed does, it is
+the \texttt{pos} constructor itself), the theorem can be disambiguated using
+twice that coercion on the left hand side of the implication. The obtained
+partially specified term however would not probably be the expected one, being a
+theorem which prove a trivial implication. For this reason we choose to always
+prefer fresh instances over implicit coercion, i.e. we always attempt
+disambiguation passes with fresh instances before attempting passes with
+implicit coercions.
+
+\subsubsection{Disambiguation passes}
+
+\TODO{spiegazione della tabella}
+
+\begin{center}
+ \begin{tabular}{c|c|c|c}
+ \multicolumn{1}{p{1.5cm}|}{\centering\raisebox{-1.5ex}{\textbf{Pass}}}
+ & \multicolumn{1}{p{2.5cm}|}{\centering\textbf{Operator instances}}
+ & \multicolumn{1}{p{3.1cm}|}{\centering\textbf{Disambiguation aliases}}
+ & \multicolumn{1}{p{2.5cm}}{\centering\textbf{Implicit coercions}} \\
+ \hline
+ \PASS & Normal & Mono & Disabled \\
+ \PASS & Normal & Multi & Disabled \\
+ \PASS & Fresh & Mono & Disabled \\
+ \PASS & Fresh & Multi & Disabled \\
+ \PASS & Fresh & Mono & Enabled \\
+ \PASS & Fresh & Multi & Enabled \\
+ \PASS & Fresh & Library & Enabled
+ \end{tabular}
+\end{center}
+
+\TODO{alias one shot}
+
\acknowledgements
We would like to thank all the students that during the past
five years collaborated in the \HELM{} project and contributed to
projects / helm.git / blobdiff