[om] Little question about Coq theories in OpenMath

[Professor James Davenport]

On Fri, 28 Jun 2002, Paul Libbrecht wrote:
> 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.
I wish I'd been involved in those, but one can't be everywhere.
> 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.
Well, the'official one' need not be the only one in OpenMath. There are 
certainly several equalities. Indeed, I have been working on a ternary 
equality "x = y in D", or, for example
<OMA>
  <OMS name="eq" cd="relation2"/>
  <OMI> 2 </OMI>
  <OMI> 5 </OMI>
  <OMA>
    <OMS name="GFp" cd="setname2"/>
    <OMI> 3 </OMI>
  </OMA>
</OMA>
I have a paper on equalities, but I certainly can't count to 19, and one 
might hope that the above suggestion would handle several of them.
> 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.
Possibly augmented with hints.
> - 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.
Several new CDs are certainly needed, and I don't think they would destroy 
all inter-operability. 
> 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 ?
James
--
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