From: Claudio Sacerdoti Coen Date: Thu, 17 Nov 2005 15:10:46 +0000 (+0000) Subject: Inizio stesura parte su "libreria tutta visibile". X-Git-Tag: V_0_7_2_3~54 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=8684c6f92b368b567fa401b1054bcdefa8fa72ae Inizio stesura parte su "libreria tutta visibile". --- diff --git a/helm/papers/matita/matita.tex b/helm/papers/matita/matita.tex index ddcc9e6ce..23244b138 100644 --- a/helm/papers/matita/matita.tex +++ b/helm/papers/matita/matita.tex @@ -205,7 +205,7 @@ language; 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 @@ -227,7 +227,7 @@ look like if entirely rewritten from scratch: just to give an 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 @@ -243,6 +243,86 @@ reduce our code in sensible way).\NOTE{righe\\\COQ{}} \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} @@ -423,10 +503,7 @@ polymorhpic equality. \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 @@ -557,7 +634,7 @@ selecting the interesting parts with the placeholder $\%$. 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 @@ -595,7 +672,7 @@ conclusion. 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. @@ -689,9 +766,9 @@ In \MATITA{} all the tactics that can be restricted to subterm of the working 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}