\newcommand{\LOCATE}{\textsc{Locate}}
\newcommand{\MATCH}{\textsc{Match}}
\newcommand{\MATITA}{Matita}
+\newcommand{\MATITAC}{\texttt{matitac}}
+\newcommand{\MATITADEP}{\texttt{matitadep}}
\newcommand{\METAHEADING}{Symbol & Position \\ \hline\hline}
\newcommand{\MOWGLI}{MoWGLI}
\newcommand{\NAT}{\ensuremath{\mathit{nat}}}
\end{opening}
+\tableofcontents
\section{Introduction}
\label{sec:intro}
overall management of the library, integrating everything into a
single system. \MATITA{} is the result of this effort.
-\subsection{The System}
-DESCRIZIONE DEL SISTEMA DAL PUNTO DI VISTA ``UTENTE''
-
-\begin{itemize}
- \item scelta del sistema fondazionale
- \item sistema indipendente (da \COQ)
- \item compatibilit\`a con sistemi legacy
-\end{itemize}
-
\subsection{Relationship with \COQ{}}
At first sight, \MATITA{} looks as (and partly is) a \COQ{} clone. This is
%be able to contribute to \COQ{}'s code is quite steep and requires direct
%and frequent interactions with \COQ{} developers.
+\subsection{The system}
+
+DESCRIZIONE DEL SISTEMA DAL PUNTO DI VISTA ``UTENTE''\\
+ROBA CHE MANCA:
+\begin{itemize}
+ \item scelta del sistema fondazionale
+ \item sistema indipendente (da \COQ)
+ \item compatibilit\`a con sistemi legacy
+\end{itemize}
+
\begin{figure}[t]
+ \begin{center}
+% \includegraphics[width=0.9\textwidth]{a.eps}
+ \caption{\MATITA{} screenshot}
+ \label{fig:screenshot}
+ \end{center}
+\end{figure}
+
+\MATITA{} has a script based user interface. As can be seen in Fig.~... it is
+split in two main windows: on the left a textual widget is used to edit the
+script, on the right the list of open goal is shown using a MathML rendering
+widget. A distinguished part of the script (shaded in the screenshot) represent
+the commands already executed and can't be edited without undoing them. The
+remaining part can be freely edited and commands from that part can be executed
+moving down the execution point. An additional window --- the ``cicBrowser'' ---
+can be used to browse the library, including the proof being developed, and
+enable content based search on it. In the cicBrowser proofs are rendered in
+natural language, automatically generated from the low-level $\lambda$-terms
+using techniques inspired by \cite{natural,YANNTHESIS}.
+
+In the \MATITA{} philosophy the script is not relevant \emph{per se}, but is
+only seen as a convenient way to create mathematical objects. The universe of
+all these objects makes up the \HELM{} library, which is always completely
+visible to the user. The mathematical library is thus conceived as a global
+hypertext, where objects may freely reference each other. It is a duty of
+the system to guide the user through the relevant parts of the library.
+
+This methodological assumption has many important consequences
+which will be discussed in the next section.
+
+%on one side
+%it requires functionalities for the overall management of the library,
+%%%%%comprising efficient indexing techniques to retrieve and filter the
+%information;
+%on the other it introduces overloading in the use of
+%identifiers and mathematical notation, requiring sophisticated disambiguation
+%techniques for interpreting the user inputs.
+%In the next two sections we shall separately discuss the two previous
+%points.
+
+%In order to maximize accessibility mathematical objects are encoded in XML. (As%discussed in the introduction,) the modular architecture of \MATITA{} is
+%organized in components which work on data in this format. For instance the
+%rendering engine, which transform $\lambda$-terms encoded as XML document to
+%MathML Presentation documents, can be used apart from \MATITA{} to print ...
+%FINIRE
+
+A final section is devoted to some innovative aspects
+of the authoring system, such as a step by step tactical execution,
+content selection and copy-paste.
+
+\section{Architecture}
+\label{architettura}
+
+\begin{figure}[ht]
\begin{center}
\includegraphics[width=0.9\textwidth]{librariesCluster.ps}
\caption{\MATITA{} libraries}
\end{center}
\end{figure}
-\section{Architecture}
-\label{architettura}
Fig.~\ref{fig:libraries} shows the architecture of the \emph{\components}
(circle nodes) and \emph{applications} (squared nodes) developed in the HELM
project.
\component, we can focus on the representation of the mathematical information.
\MATITA{} is based on (a variant of) the Calculus of (Co)Inductive
Constructions (CIC). In CIC terms are used to represent mathematical
-expressions, types and proofs. \MATITA{} is able to handle terms at
+formulae, types and proofs. \MATITA{} is able to handle terms at
four different levels of specification. On each level it is possible to provide
a different set of functionalities. The four different levels are:
fully specified terms; partially specified terms;
We use metadata and a sort of crawler to index the mathematical notions
in the distributed library. We are interested in retrieving a notion
by matching, instantiation or generalization of a user or system provided
- mathematical expression. Thus we need to collect metadata over the fully
+ mathematical formula. Thus we need to collect metadata over the fully
specified terms and to store the metadata in some kind of (relational)
database for later usage. The \texttt{hmysql} \component{} provides
a simplified
given by the conclusion of the sequent. The term must be closed in the
context that is given by the ordered list of hypotheses of the sequent.
The explicit substitution instantiates every hypothesis with an actual
-value for the term bound by the hypothesis.
+value for the variable bound by the hypothesis.
Partially specified terms are not required to be well-typed. However a
partially specified term should be \emph{refinable}. A \emph{refiner} is
a type-inference procedure that can instantiate implicit terms and
metavariables and that can introduce \emph{implicit coercions} to make a
-partially specified term be well-typed. The refiner of \MATITA{} is implemented
+partially specified term well-typed. The refiner of \MATITA{} is implemented
in the \texttt{cic\_unification} \component. As the type checker is based on
the conversion check, the refiner is based on \emph{unification} that is
a procedure that makes two partially specified term convertible by instantiating
and lemmas. The \texttt{grafite\_engine} \component{} is the core of \MATITA{}.
It implements the semantics of each command in the grafite AST as a function
from status to status. It implements also an undo function to go back to
-previous statuses. \TODO{parlare di disambiguazione lazy \& co?}
+previous statuses.
As fully specified terms, partially specified terms are not well suited
for user consumption since their syntax is not extendible and it is not
\subsection{Content level terms}
\label{sec:contentintro}
-The language used to communicate proofs and expecially expressions with the
+The language used to communicate proofs and expecially formulae with the
user does not only needs to be extendible and accomodate the usual mathematical
notation. It must also reflect the comfortable degree of imprecision and
ambiguity that the mathematical language provides.
to communicate formulae with the user and with external tools, it seems good
practice to stick to the usual imprecise mathematical ontology. In the
Mathematical Knowledge Management community this imprecise language is called
-the \emph{content level} representation of expressions.
+the \emph{content level} representation of formulae.
In \MATITA{} we provide two translations: from partially specified terms
to content level terms and the other way around. The first translation can also
The translation from partially specified terms to content level terms must
discriminate between terms used to represent proofs and terms used to represent
-expressions. The firsts are translated to a content level representation of
-proof steps that can easily be rendered in natural language. The latters
-are translated to MathML Content formulae. MathML Content~\cite{mathml} is a W3C
-standard
-for the representation of content level expressions in an XML extensible format.
+formulae. The firsts are translated to a content level representation of
+proof steps that can easily be rendered in natural language. The representation
+adopted has greatly influenced the OMDoc~\cite{omdoc} proof format that is now
+isomorphic to it. Terms that represent formulae are translated to MathML
+Content formulae. MathML Content~\cite{mathml} is a W3C standard
+for the representation of content level formulae in an XML extensible format.
The translation to content level is implemented in the
\texttt{acic\_content} \component. Its input are \emph{annotated partially
specified terms}, that are maximally unshared
partially specified terms enriched with additional typing information for each
subterm. This information is used to discriminate between terms that represent
-proofs and terms that represent expressions. Part of it is also stored at the
+proofs and terms that represent formulae. Part of it is also stored at the
content level since it is required to generate the natural language rendering
of proofs. The terms need to be maximally unshared (i.e. they must be a tree
and not a DAG). The reason is that to the occurrences of a subterm in
We do not provide yet a reverse translation from content level proofs to
partially specified terms. But in \texttt{cic\_disambiguation} we do provide
-the reverse translation for expressions. The mapping from
-content level expressions to partially specified terms is not unique due to
+the reverse translation for formulae. The mapping from
+content level formulae to partially specified terms is not unique due to
the ambiguity of the content level. As a consequence the translation
is guided by an \emph{interpretation}, that is a function that chooses for
-every ambiguous expression one partially specified term. The
+every ambiguous formula one partially specified term. The
\texttt{cic\_disambiguation} \component{} implements the
disambiguation algorithm we presented in~\cite{disambiguation} that is
responsible of building in an efficicent way the set of all ``correct''
interpretations. An interpretation is correct if the partially specified term
obtained using the interpretation is refinable.
+In the last section we have described the semantics of a command as a
+function from status to status. We also suggested that the formulae in a
+command are encoded as partially specified terms. However, consider the
+command ``\texttt{replace} $x$ \texttt{with} $y^2$''. Until the occurrence
+of $x$ to be replaced is located, its context is unknown. Since $y^2$ must
+replace $x$ in that context, its encoding as a term cannot be computed
+until $x$ is located. In other words, $y^2$ must be disambiguated in the
+context of the occurrence $x$ it must replace.
+
+The elegant solution we have implemented consists in representing terms
+in a command as function from a context to a partially refined term. The
+function is obtained by partially applying our disambiguation function to
+the content term to be disambiguated. Our solution should be compared with
+the one adopted in the Coq system (where ambiguity is only relative to
+DeBrujin indexes). In Coq variables can be bound either by name or by
+position. This makes more complex every operation over terms (i.e. according
+to our architecture every module that depends on \texttt{cic}). Moreover,
+this solution cannot cope with other forms of ambiguity (as the meaning
+of the $~^2$ exponent in the previous example that depends on the context).
+
\subsection{Presentation level terms}
Content level terms are a sort of abstract syntax trees for mathematical
-expressions and proofs. The concrete syntax given to these abstract trees
+formulae and proofs. The concrete syntax given to these abstract trees
is called \emph{presentation level}.
The main important difference between the content level language and the
semantics of these commands. It also implements undoing of the semantic
actions. Among the commands there are hints to the
disambiguation algorithm that are used to control and speed up disambiguation.
-These mechanisms will be further discussed in Sect.~\ref{disambiguazione}.
+These mechanisms will be further discussed in Sect.~\ref{sec:disambiguation}.
Finally, the \texttt{grafite\_parser} \component{} implements a parser for
the concrete syntax of the commands of \MATITA. The parser process a stream
\texttt{logger}, \texttt{registry} and \texttt{utf8\_macros}) are
minor \components{} that provide a core of useful functions and basic
services missing from the standard library of the programming language.
-In particular, the \texttt{xml} \component{} is used
-to easily represent, parse and pretty-print XML files.
-
-\section{Using \MATITA (boh \ldots cambiare titolo)}
-
-\begin{figure}[t]
- \begin{center}
-% \includegraphics[width=0.9\textwidth]{a.eps}
- \caption{\MATITA{} screenshot}
- \label{fig:screenshot}
- \end{center}
-\end{figure}
-
-\MATITA{} has a script based user interface. As can be seen in Fig.~... it is
-split in two main windows: on the left a textual widget is used to edit the
-script, on the right the list of open goal is shown using a MathML rendering
-widget. A distinguished part of the script (shaded in the screenshot) represent
-the commands already executed and can't be edited without undoing them. The
-remaining part can be freely edited and commands from that part can be executed
-moving down the execution point. An additional window --- the ``cicBrowser'' ---
-can be used to browse the library, including the proof being developed, and
-enable content based search on it. In the cicBrowser proofs are rendered in
-natural language, automatically generated from the low-level $\lambda$-terms
-using techniques inspired by \cite{natural,YANNTHESIS}.
-
-In the \MATITA{} philosophy the script is not relevant \emph{per se}, but is
-only seen as a convenient way to create mathematical objects. The universe of
-all these objects makes up the \HELM{} library, which is always completely
-visible to the user. The mathematical library is thus conceived as a global
-hypertext, where objects may freely reference each other. It is a duty of
-the system to guide the user through the relevant parts of the library.
-
-This methodological assumption has many important consequences
-which will be discussed in the next section.
-
-%on one side
-%it requires functionalities for the overall management of the library,
-%%%%%comprising efficient indexing techniques to retrieve and filter the
-%information;
-%on the other it introduces overloading in the use of
-%identifiers and mathematical notation, requiring sophisticated disambiguation
-%techniques for interpreting the user inputs.
-%In the next two sections we shall separately discuss the two previous
-%points.
-
-%In order to maximize accessibility mathematical objects are encoded in XML. (As%discussed in the introduction,) the modular architecture of \MATITA{} is
-%organized in components which work on data in this format. For instance the
-%rendering engine, which transform $\lambda$-terms encoded as XML document to
-%MathML Presentation documents, can be used apart from \MATITA{} to print ...
-%FINIRE
-
-A final section is devoted to some innovative aspects
-of the authoring system, such as a step by step tactical execution,
-content selection and copy-paste.
+%In particular, the \texttt{xml} \component{} is used to easily represent,
+%parse and pretty-print XML files.
\section{Library Management}
\subsection{Indexing and searching}
-\subsection{Compilation and decompilation}
+\subsection{Compilation and cleaning}
\label{sec:libmanagement}
-The aim of this section is to describe the way matita
+%
+%goals: consentire sviluppo di una librearia mantenendo integrita' referenziale e usando le teconologie nostre (quindi con metadati, XML, libreria visibile)
+%\subsubsection{Composition}
+%scripts.ma, .moo, XML, metadata
+%\subsubsection{Compilation}
+%analogie con compilazione classica dso.\\
+%granularita' differenti per uso interattivo e non
+%\paragraph{Batch}
+%- granularita' .ma/buri \\
+%-- motivazioni\\
+%- come si calcolano le dipendenze\\
+%- quando la si usa\\
+%- metodi (cc e clean)\\
+%- garanzie
+%\paragraph{Interactive}
+%- granularita' fine\\
+%-- motivazioni
+%\label{sec:libmanagement}
+%consistenza: integrita' referenziale
+%Goals: mantenere consistente la rappresentazione della libreria su
+%memoria persistente consentendo di compilare e pulire le compilation
+%unit (.ma).\\
+%Vincoli: dipendenze oggetti-oggetti e metadati-oggetti\\
+%Due livelli di gestione libreria, uno e' solo in fase interattiva dove la compilazione e' passo passo: \\
+%--- granularita' oggetto per matita interactive\\
+%--- granularita' baseuri (compilation unit) per la libreria\\
+%In entrmbi i casi ora:\\
+%--- matitaSync: add, remove, timetravel(facility-macro tra 2 stati)[obj]\\
+%--- matitaCleanLib: clean\_baseuri (che poi usa matitaSync a sua volta)[comp1]\\
+%Vincoli di add: typecheck ( ==$>$ tutto quello che usa sta in lib)\\
+%Vincoli di remove: \\
+%--- la remove di mSync non li controlla (ma sa cosa cancellare per ogni uri)\\
+%--- la clean\_baseuri calcola le dipendenze con i metadati (o anche i moo direi) e li rispetta\\
+%Undo di matita garantisce la consistenza a patto che l'history che tiene sia ok\\
+%Undo della lib (mClean) garantisce la consistenza (usando moo o Db).\\
+
+The aim of this section is to describe the way \MATITA{}
preserves the consistency and the availability of the library
-trough the \WHELP{} technology, in response to the user addition or
-deletion of mathematical objects.
+using the \WHELP{} technology, in response to the user addition or
+removal of mathematical objects.
As already sketched in \ref{fully-spec} the output of the
compilation of a script is split among two storage media, a
store the XML encoding of the objects defined in the script, the
disambiguation aliases and the interpretation and notational convention defined,
while the latter is used to store all the metadata needed by
-\WHELP{}. In addition the \GETTER component
-should be updated with the the new mapping between the logical URI
-and the physical path of objects.
+\WHELP{}.
-While this kind of consistency has nothing to do with the nature of
-the content of the library and is thus of poor interest (but really
-tedious to implement and keep bug-free), there is a more deep
+While the consistency of the data store in the two media has
+nothing to do with the nature of
+the content of the library and is thus uninteresting (but really
+tedious to implement and keep bug-free), there is a deeper
notion of mathematical consistency we need to provide. Each object
must reference only defined object (i.e. each proof must use only
already proved theorems).
-We will focus on how matita ensures the interesting kind
+We will focus on how \MATITA{} ensures the interesting kind
of consistency during the formalization of a mathematical theory,
-giving the user the freedom of adding, deleting, modifying objects
+giving the user the freedom of adding, removing, modifying objects
without loosing the feeling of an always visible and browsable
library.
\subsubsection{Compilation}
+
The typechecker component guarantees that if an object is well typed
-it depends only on well defined objects available in the library,
+it depends only on well typed objects available in the library,
that is exactly what we need to be sure that the logic consistency of
-the library is preserved. We have only find the right order of
+the library is preserved. We have only to find the right order of
compilation of the scripts that compose the user development.
-For this purpose we developed a low level tool called \emph{matitadep}
+For this purpose we provide a tool called \MATITADEP{}
that takes in input the list of files that compose the development and
-outputs their dependencies in a format suitable for the make utility.
-The user is not asked to run \emph{matitadep} nor make by hand, but
-simply to tell matita the root directory of his development (where all
-script files can be found) and matita will handle all the compilation
-tasks.\\
-To calculate dependencies it is enough to look at the script file for
-its inclusions of other parts of the development or for explicit
+outputs their dependencies in a format suitable for the GNU \texttt{make} tool.
+The user is not asked to run \MATITADEP{} by hand, but
+simply to tell \MATITA{} the root directory of his development (where all
+script files can be found) and \MATITA{} will handle all the compilation
+related tasks, including dependencies calculation.
+To compute dependencies it is enough to look at the script files for
+inclusions of other parts of the development or for explicit
references to other objects (i.e. with explicit aliases, see
-\ref{aliases}).
+\ref{sec:disambaliases}).
The output of the compilation is immediately available to the user
trough the \WHELP{} technology, since all metadata are stored in a
user-specific area of the database where the search engine has read
access, and all the automated tactics that operates on the whole
-library, like auto, have full visibility of the newly defined objects.
+library, like \AUTO, have full visibility of the newly defined objects.
Compilation is rather simple, and the only tricky case is when we want
-to compile again the same script, maybe after the deletion of a
-theorem. Here the policy is simple: decompile it before recompiling.
-As we will see in the next section decompilation will ensure that
+to compile again the same script, maybe after the removal of a
+theorem. Here the policy is simple: clean the output before recompiling.
+As we will see in the next section cleaning will ensure that
there will be no theorems in the development that depends on the
-removed item.
+removed items.
+
+\subsubsection{Cleaning}
-\subsubsection{Decompilation}
-Decompiling an object involves,
-recursively, the decompilation of all the objects that depend on it.
+With the term ``cleaning'' we mean the process of removing all the
+results of an object compilation. In order to keep the consistency of
+the library, cleaning an object requires the (recursive) cleaning
+of all the objects that depend on it (\emph{reverse dependencies}).
The calculation of the reverse dependencies can be computed in two
ways, using the relational database or using a simpler set of metadata
-that matita saves in the filesystem as a result of compilation. The
+that \MATITA{} saves in the filesystem as a result of compilation. The
former technique is the same used by the \emph{Dependency Analyzer}
described in \cite{zack-master} and really depends on a relational
-database.\\
-The latter is a fall-back in case the database is not available. Due to
-the complex deployment of a complex peace of software like a database,
-it is a common usage for the \HELM{} team to use a single and remote
-database, that may result unavailable if the user workstation lacks
-connectivity. This facility has to be intended only as a fall-back,
-since the whole \WHELP{} technology depends on the database.
-
-Decompilation guarantees that if an object is removed there are no
-dandling references to it, and that the part of the library still
-compiled is logically consistent. Since decompilation involves the
-deletion of all the outputs of the compilation, metadata included, the
-library browsable trough the \WHELP{} technology is always up to date.
-
-\subsubsection{Interactive and batch (de)compilation}
-\MATITA{} includes an interactive graphical interface and a batch
-compiler. Only the former is intended to be used directly by the
-user, the latter is automatically invoked when a not yet compiled
-part of the user development is required.
-
-While they share the same engine for compilation and decompilation,
-they provide different granularity. The batch compiler is only able to
-compile a whole script file and reciprocally it can decompile only a whole
-script, and consequently all the other scripts that rely on an object
-defined in it. The interactive interface is able to execute single steps
-of compilation, that may include the definition of an object, and
-symmetrically to undo single steps, thus removing single objects.
+database.
-%
-%goals: consentire sviluppo di una librearia mantenendo integrita' referenziale e usando le teconologie nostre (quindi con metadati, XML, libreria visibile)
-%\subsubsection{Composition}
-%scripts.ma, .moo, XML, metadata
-%\subsubsection{Compilation}
-%analogie con compilazione classica dso.\\
-%granularita' differenti per uso interattivo e non
-%\paragraph{Batch}
-%- granularita' .ma/buri \\
-%-- motivazioni\\
-%- come si calcolano le dipendenze\\
-%- quando la si usa\\
-%- metodi (cc e clean)\\
-%- garanzie
-%\paragraph{Interactive}
-%- granularita' fine\\
-%-- motivazioni
-%\label{sec:libmanagement}
-%consistenza: integrita' referenziale
-%Goals: mantenere consistente la rappresentazione della libreria su memoria persistente consentendo di compilare e decompilare le compilation unit (.ma).\\
-%Vincoli: dipendenze oggetti-oggetti e metadati-oggetti\\
-%Due livelli di gestione libreria, uno e' solo in fase interattiva dove la compilazione e' passo passo: \\
-%--- granularita' oggetto per matita interactive\\
-%--- granularita' baseuri (compilation unit) per la libreria\\
-%In entrmbi i casi ora:\\
-%--- matitaSync: add, remove, timetravel(facility-macro tra 2 stati)[obj]\\
-%--- matitaCleanLib: clean\_baseuri (che poi usa matitaSync a sua volta)[comp1]\\
-%Vincoli di add: typecheck ( ==$>$ tutto quello che usa sta in lib)\\
-%Vincoli di remove: \\
-%--- la remove di mSync non li controlla (ma sa cosa cancellare per ogni uri)\\
-%--- la clean\_baseuri calcola le dipendenze con i metadati (o anche i moo direi) e li rispetta\\
-%Undo di matita garantisce la consistenza a patto che l'history che tiene sia ok\\
-%Undo della lib (mClean) garantisce la consistenza (usando moo o Db).\\
+The latter is a fall-back in case the database is not
+available.\footnote{Due to the complex deployment of a large piece of
+software like a database, it is a common practice for the \HELM{} team
+to use a shared remote database, that may be unavailable if the user
+workstation lacks network connectivity.} This facility has to be
+intended only as a fall-back, since the queries of the \WHELP{}
+technology depend require a working database.
+
+Cleaning guarantees that if an object is removed there are no dandling
+references to it, and that the part of the library still compiled is
+consistent. Since cleaning involves the removal of all the results of
+the compilation, metadata included, the library browsable trough the
+\WHELP{} technology is always kept up to date.
+
+\subsubsection{Batch vs Interactive}
+
+\MATITA{} includes an interactive graphical interface and a batch
+compiler (\MATITAC). Only the former is intended to be used directly by the
+user, the latter is automatically invoked when a
+part of the user development is required (for example issuing an
+\texttt{include} command) but not yet compiled.
+
+While they share the same engine for compilation and cleaning, they
+provide different granularity. The batch compiler is only able to
+compile a whole script and similarly to clean only a whole script
+(together with all the other scripts that rely on an object defined in
+it). The interactive interface is able to execute single steps of
+compilation, that may include the definition of an object, and
+similarly to undo single steps. Note that in the latter case there is
+no risk of introducing dangling references since the \MATITA{} user
+interface inhibit undoing a step which is not the last executed.
\subsection{Automation}
-\subsection{\MATITA's naming convention}
+\subsection{Naming convention}
A minor but not entirely negligible aspect of \MATITA{} is that of
adopting a (semi)-rigid naming convention for identifiers, derived by
our studies about metadata for statements.
expression and the suffix \verb+_to_Prop+. In the above example,
\verb+eqb_to_Prop+ is accepted.
-\section{The \MATITA{} user interface}
-
-
+\section{User interface}
\subsection{Disambiguation}
+\label{sec:disambiguation}
Software applications that involve input of mathematical content should strive
to require the user as less drift from informal mathematics as possible. We
expressiveness.
\subsubsection{Disambiguation aliases}
-\label{aliases}
+\label{sec:disambaliases}
Let's start with the definition of the ``strictly greater then'' notion over
(Peano) natural numbers.
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:
\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}.
+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.
-\TODO{spiegazione della tabella}
-
-\begin{table}
- \caption{\label{tab:disambpasses} Disambiguation passes.\strut}
- \footnotesize
+\begin{table}[ht]
+ \caption{Sequence of disambiguation passes used in \MATITA.\strut}
+ \label{tab:disambpasses}
\begin{center}
\begin{tabular}{c|c|c|c}
\multicolumn{1}{p{1.5cm}|}{\centering\raisebox{-1.5ex}{\textbf{Pass}}}
\end{center}
\end{table}
-\TODO{alias one shot}
-
-
-
-
-
-
-
\subsection{Patterns}
serve una intro che almeno cita il widget (per i patterns) e che fa
\MATITA{} tacticals syntax is reported in table \ref{tab:tacsyn}.
While one would expect to find structured constructs like
$\verb+do+~n~\NT{tactic}$ the syntax allows pieces of tacticals to be written.
-This is essential for base idea behind matita tacticals: step-by-step execution.
+This is essential for base idea behind \MATITA{} tacticals: step-by-step
+execution.
The low-level tacticals implementation of \MATITA{} allows a step-by-step
execution of a tactical, that substantially means that a $\NT{block\_kind}$ is
goal) gives you the feeling of what is going on.
\end{description}
-\section{The \MATITA{} library}
+\section{Standard library}
\MATITA{} is \COQ{} compatible, in the sense that every theorem of \COQ{}
can be read, checked and referenced in further developments.
projects / helm.git / blobdiff