rendering, and semantic selection, i.e. the possibility to select semantically
meaningful rendering expressions, and to past the respective content into
a different text area.
-\NOTE{il widget\\ non ha sel\\ semantica}
+\NOTE{il widget non ha sel semantica}
\end{itemize}
Starting from all this, the further step of developing our own
proof assistant was too
idea, although \MATITA{} currently supports almost all functionalities of
\COQ{}, it links 60'000 lins of \OCAML{} code, against ... of \COQ{} (and
we are convinced that, starting from scratch again, we could furtherly
-reduce our code in sensible way).\NOTE{righe\\\COQ{}}
+reduce our code in sensible way).\NOTE{righe \COQ{}}
\begin{itemize}
\item scelta del sistema fondazionale
\subsection{libreria tutta visibile}
\ASSIGNEDTO{csc}
+\NOTE{assumo che si sia gia' parlato di approccio content-centrico}
+Our commitment to the content-centric view of the architecture of the system
+has important consequences on the user's experience and on the functionalities
+of several components of \MATITA. In the content-centric view the library
+of mathematical knowledge is an already existent and completely autonomous
+entity that we are allowed to exploit and augment using \MATITA. Thus, in
+principle, when the user starts to prove a new theorem she has complete
+visibility of the library and she can refer to every definition and lemma,
+also using the mathematical notation already developed. In a similar way,
+every form of automation of the system must be able to analyze and possibly
+exploit every notion in the library.
+
+The benefits of this approach highly justify the non neglectable price to pay
+in the development of several components. We analyse now a few of the causes
+of this additional complexity.
+
+\subsubsection{Ambiguity}
+A rich mathematical library includes equivalent definitions and representations
+of the same notion. Moreover, mathematical notation inside a rich library is
+surely highly overloaded. As a consequence every mathematical expression the
+user provides is highly ambiguous since all the definitions,
+representations and special notations are available at once to the user.
+
+The usual solution to the problem, as adopted for instance in Coq, is to
+restrict the user's scope to just one interpretation for each definition,
+representation or notation. In this way much of the ambiguity is removed,
+burdening the user that must someway declare what is in scope and that must
+use special syntax when she needs to refer to something not in scope.
+
+Even with this approach ambiguity cannot be completely removed since implicit
+coercions can be arbitrarily inserted by the system to ``change the type''
+of subterms that do not have the expected type. Usually implicit coercions
+are used to overcome the absence of subtyping that should mimic the subset
+relation found in set theory. For instance, the expression
+$\forall n \in nat. 2 * n * \pi \equiv_\pi 0$ is correct in set theory since
+the set of natural numbers is a subset of that of real numbers; the
+corresponding expression $\forall n:nat. 2*n*\pi \equiv_\pi 0$ is not well typed
+and requires the automatic insertion of the coercion $real_of_nat: nat \to R$
+either around both 2 and $n$ (to make both products be on real numbers) or
+around the product $2*n$. The usual approach consists in either rejecting the
+ambiguous term or arbitrarily choosing one of the interpretations. For instance,
+Coq rejects the declaration of coercions that have alternatives
+(i.e. already declared coercions with the same domain and codomain)
+or that are obtained composing other coercions in order to
+avoid making several terms highly ambiguous by choosing to insert any one of the
+alternative coercions. Coq also arbitrarily chooses how to insert coercions in
+terms to make them well typed when there is more than one possibility (as in
+the previous example).
+
+The approach we are following is radically different. It consists in dealing
+with ambiguous expressions instead of avoiding them. As a last resource,
+when the system is unable to disambiguate the input, the user is interactively
+required to provide more information that is recorded to avoid asking the
+same question again in subsequent processing of the same input.
+More details on our approach can be found in \ref{sec:disambiguation}.
+
+\subsubsection{Consistency}
+A large mathematical library is likely to be logically inconsistent.
+It may contain incompatible axioms or alternative conjectures and it may
+even use definitions in incompatible ways. To clarify this last point,
+consider two identical definitions of a set of elements of a given type
+(or of a category of objects of a given type). Let us call the two definitions
+$A-Set$ and $B-Set$ (or $A-Category$ and $B-Category$).
+It is perfectly legitimate to either form the $A-Set$ of every $B-Set$
+or the $B-Set$ of every $A-Set$ (the same for categories). This just corresponds
+to assuming that a $B-Set$ (respectively an $A-Set$) is a small set, whereas
+an $A-Set$ (respectively a $B-Set$) is a big set (possibly of small sets).
+However, if one part of the library assumes $A-Set$s to be the small ones
+and another part of the library assumes $B-Set$s to be the small ones, the
+library as a whole will be logically inconsistent.
+
+Logical inconsistency has never been a problem in the daily work of a
+mathematician. The mathematician simply imposes himself a discipline to
+restrict himself to consistent subsets of the mathematical knowledge.
+However, in doing so he doesn't choose the subset in advance by forgetting
+the rest of his knowledge.
+
+Contrarily to a mathematician, the usual tendency in the world of assisted
+automation is that of restricting in advance the part of the library that
+will be used later on, checking its consistency by construction.
\subsection{ricerca e indicizzazione}
\label{sec:metadata}
\subsubsection{Disambiguation algorithm}
-\NOTE{assumo\\
- che si sia\\
- gia' parlato\\
- di refine}
+\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
The latter is a term that lives in the context of the placeholders.
The concrete syntax is reported in table \ref{tab:pathsyn}
-\NOTE{uso nomi diversi \\dalla grammatica \\ ma che hanno + senso}
+\NOTE{uso nomi diversi dalla grammatica ma che hanno + senso}
\begin{table}
\caption{\label{tab:pathsyn} Concrete syntax of \MATITA{} patterns.\strut}
\hrule
assumption is selected. Remember that the user can be mostly
unaware of this syntax, since the system is able to write down a
$\NT{sequent\_path}$ starting from a visual selection.
- \NOTE{Questo ancora non va\\in matita}
+ \NOTE{Questo ancora non va in matita}
A $\NT{multipath}$ is a CiC term in which a special constant $\%$
is allowed.
sequent accept the pattern syntax. In particular these tactics are: simplify,
change, fold, unfold, generalize, replace and rewrite.
-\NOTE{attualmente rewrite e \\ fold non supportano \\ phase 2. per
-supportarlo\\bisogna far loro trasformare\\il pattern phase1+phase2\\
-in un pattern phase1only\\come faccio nell'ultimo esempio.\\lo si fa
+\NOTE{attualmente rewrite e fold non supportano phase 2. per
+supportarlo bisogna far loro trasformare il pattern phase1+phase2
+in un pattern phase1only come faccio nell'ultimo esempio. lo si fa
con una pattern\_of(select(pattern))}
\subsubsection{Comparison with Coq}
projects / helm.git / commitdiff