[om] DefMP elements

[Bill Naylor]

Hi all,

I am interested in the current state of thought amongst the OpenMath
community as regards DefMP files/elements. The only documents that I could
find which mentioned these dated back to 1999, and are clearly out of date
(with regard to other aspects of OpenMath). Also, the two documents I
looked at seemed to have different ideas about how this should be done:

The one document "Development of Strong OpenMath" (Arjeh Cohen and Olga
Caprotti) suggested the DefMP has a name attribute to specify the symbol,
whilst the enclosing CDDefMPs element has a cd attribute. The major
difference (between this and the next technique I shall mention) is the
specification of the definition, that is the OMOBJ
content of the DefMP IS the object being defined (by my reading - Olga, or
                     ~~
Arjeh maybe you can correct me if I'm wrong?)

The second document "Proposal for an extension of OpenMath by Defining
Mathematical Properties" suggests that the DefMPs should be in the CD
itself and should have content which is an OMOBJ with a defining
property of the symbol being defined.

It seems to me that the second interpretation gives broader scope for
definition, as the first interpretation may be recovered simply by going:

<DefMP><OMOBJ> eq(symbol,property) </OMOBJ></DefMP>

though I would also vote for the name attribute and having these DefMP
elements in a seperate file system.

This interpretation seems to be much closer to the OMDoc definition
element, though that also has a type attribute which allows to specify the
type of the definition ("simple","inductive","recursive" etc.). I gues we
could do this via OMAttr, and having a CD to define the different possible
definition mechanisms.

thoughts / and / or pointers to relevant material gratefully accepted,

Bill
--
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