[om] Little question about Coq theories in OpenMath

[Paul Libbrecht]

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