[om] Little question about Coq theories in OpenMath

[Olga Caprotti]

Hi Paul,

I met Claudio Sacerdoti Coen in Marseille last week and we talked
about this issue. It seems to me that both approaches have to be
allowed: the second (richer CDs) needed when one interfaces Coq with
systems that have similar formal precision, the first needed when
Coq talks to systems that basically are not type-aware or formal.
This first approach is the one I used for the Pocklington example which 
however was dealing with very simple objects to be sent to GAP.

Simpler questions have to be answered first when trying to use OpenMath
instead of Content-MML (with lots of csymbols). For instance,
Claudio asked me how to convert a function like divide which in Coq
takes 3 arguments: numerator, denominator and a proof that the 
denominator is not zero. In this case I believe it would be useful
to have such a divide symbol in OpenMath: it would even be possible to
keep the extra information in types-unaware systems e.g. using something 
like "assert" in Maple. Maybe James can comment on this further.

I guess the choice of which symbol to put in a CD is an art and not
so easy to decide. To this end, it would help to extend HELM to systems
other that COQ or even to start comparing MBase theories with Coq theories.


Olga






Paul Libbrecht wrote:
> 
> Hi OpenMathers,
> 
> 
> A while ago, we had a rather long discussion with the team of Andrea 
> Asperti in Bologna on how to export Coq content to OpenMath.
> 
> Basically, two approaches were proposed and I have to say I could not 
> really decide which is better and would like to have more precise ideas 
> on their implications for applications of OpenMath (especially 
> phrasebooks and rendering engines):
> 
> - their original approach was to say that OpenMath is a "content" 
> representation as opposed to a "semantic" (they call it so...) 
> representation that Coq has.
> That is, in their conversion to "content" they accept to loose some 
> semantics. Among others, there are about nineteen equalities in Coq 
> which they all map to the official one of OpenMath.
> Inputting an OpenMath object into Coq would then involve guessing, using 
> Coq type-checking I guess, the exact symbol attached to the generic 
> equality. Wether this task is feasible is, to me, an open question.
> 
> - the other approach is, of course, to define new content dictionaries 
> (possibly helped by a declaration framework such as OMDoc) which would 
> contain the very rich set of symbols found in the Coq classical 
> libraries thus avoid loosing the semantics in the conversion but 
> destroying interoperability as all the applications would need to be 
> extended to support these content dictionaries if they were to be used.
> 
> I think some of the members of the list had attempts with Coq.
> Can they comment on the conversion process ? Could they, for example, 
> take advantage of an OpenMath conversion to have Coq delegate 
> computational tasks to another mathematical system ??
> Did anyone try to present Coq theories aside of the HELM project ?
> 
> Thanks.
> 
> Paul
> -- 
> om at openmath.org  -  general discussion on OpenMath
> Post public announcements to om-announce at openmath.org
> Automatic list maintenance software at majordomo at openmath.org
> Mail om-owner at openmath.org for assistance with any problems
> 
> 



-- 
--
Olga Caprotti         caprotti at risc.uni-linz.ac.at
RISC-Linz, Johannes Kepler University, A-4040 Linz
--
om at openmath.org  -  general discussion on OpenMath
Post public announcements to om-announce at openmath.org
Automatic list maintenance software at majordomo at openmath.org
Mail om-owner at openmath.org for assistance with any problems