From e5d77bcbc81aa4e3f5d2f8d53ce47f029e1618a6 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 25 Nov 2005 11:19:59 +0000 Subject: [PATCH 1/1] ... --- helm/papers/matita/matita2.tex | 42 +++++++++++++++++++++++----------- 1 file changed, 29 insertions(+), 13 deletions(-) diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex index 8708e4458..76cd8aa18 100644 --- a/helm/papers/matita/matita2.tex +++ b/helm/papers/matita/matita2.tex @@ -183,7 +183,7 @@ to be used as a Web service. \MATITA{} can directly link the code of the that forwards every request to the Getter. To better understand the architecture of \MATITA{} and the role of each -library, we can focus on the rappresentation of the mathematical information. +library, 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 @@ -313,29 +313,45 @@ 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. -In \MATITA{} we provide two translations from partially refined terms +In \MATITA{} we provide two translations from partially specified terms to content level terms and the other way around. The first translation can also -be applied to fully refined terms since a fully refined term is a special case -of partially refined term where no metavariable or implicit term occurs. +be applied to fully specified terms since a fully specified term is a special +case of partially specified term where no metavariable or implicit term occurs. -The translation from partially refined terms to content level terms must +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 -proofs steps that can easily be rendered in natural language. The latters +proof steps that can easily be rendered in natural language. The latters are translated to MathML Content formulae. MathML Content is a W3C standard for the representation of content level expressions in an XML extensible format. The translation to content level is implemented in the -\texttt{acic\_to\_content} library. Its input are \emph{annotated partially -refined terms}. Annotated partially refined terms are maximally unshared -partially refined terms enriched with additional typing information for each +\texttt{acic\_content} library. Its input are \emph{annotated partially +specified terms}. Annotated partially specified terms 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 content level since it is required to generate the natural language rendering -of proofs. The \emph{cic\_to\_acic} library annotates partially refined terms. - -The translation from content level terms to partially refined terms is -also performed in \ldots ??? +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 +two different positions we need to associate different typing informations. +This association is made easier when the term is represented as a tree since +it is possible to label each node with an unique identifier and associate +the typing information using a map on the identifiers. +The \texttt{cic\_acic} library annotates partially specified terms. + +We do not provide yet a reverse translation from content level proofs to +partially specified terms. But in \texttt{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 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 +\texttt{disambiguation} library contains the implementation of 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 refined term +obtained using the interpretation is refinable. \subsection{Terms at the presentation level} -- 2.39.2