From f59550b5a9cdddbb348697201fae7d736d6b96c5 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 24 Nov 2005 14:02:27 +0000 Subject: [PATCH] ... --- helm/papers/matita/matita2.tex | 48 ++++++++++++++++++++++++++++++++++ 1 file changed, 48 insertions(+) diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex index 7cfdde2e9..be3cc61bf 100644 --- a/helm/papers/matita/matita2.tex +++ b/helm/papers/matita/matita2.tex @@ -288,6 +288,54 @@ an improvement over fully specified terms since they allow to omit redundant information that can be inferred by the refiner. \subsection{Terms at the content level} +The language used to communicate proofs and expecially expressions 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. + +For instance, it is common practice in mathematics to speak of a generic +equality that can be used to compare any two terms. However, it is well known +that several equalities can be identified as soon as we care for decidability +or for their computational properties. For instance equality over real +numbers is well known to be undecidable, whereas it is decidable over +rational numbers. + +Similarly, we usually speak of natural numbers and their operations and +properties without caring about their representation. However the computational +properties of addition over the binary representation are very different from +those of addition over the unary representation. And addition over two natural +numbers is definitely different from addition over two real numbers. + +Formal mathematics cannot hide these differences and obliges the user to be +very precise on the types he is using and their representation. However, +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. + +In \MATITA{} we provide two translations from partially refined 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. + +The translation from partially refined 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 +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 +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 ??? \subsection{Terms at the presentation level} -- 2.39.2