[Om3] CD issues from MathML3 cn discussion

[Michael Kohlhase]

Dear all,

yesterday at the MathML3 F2F in Cannes, we discussed the alignment of
number constructs between MathML and OpenMath and a couple of things
came up that still need to be discussed for alignment, mostly during a
teleconference with Stephen Watt, who has worked

Here is the background (I have attached the newest version of MathML3
chapter 4 for reference).
We have split the representation of numbers in content MathML into a
strict part  (isomorphic to OpenMath; see 4.2.3) and a pragmatic part
(that gets its meaning via a translation to stric; see 4.3.1).

The main idea is to interpret those number representations that cannot
simply be represented by a single string as constructed from strict
numbers that can (see 4.3.1). Now there are two important decisions to take:

   1. where to draw the line between strict: the current proposal is to
      go by representability and have types integer, double, and real in
      strict. The first two directly correspond to OMI and OMF in
      OpenMath and <cn type="real"> can be translated to OM via
      bigfloat1. Stephen objects to this proposal on the grounds that
      the type hierarchy integer<rational<real is  punctuated by 
      rationals being in pragmatic while integer and real being in strict.

   2. what are the exact symbols that are used as constructors: the
      current proposal follows the old OM/MathML alignment/translation
      guide and uses the CDs complex1, bigfloat1, num1. Stephen objected
      to this zoo of number constructors and called for re-parceling the
      CDs involved into a new CD called number_constructors or something
      speaking like this.

A remaining problem of the proposal is that round-tripping between
strict content  MathML (and thus OM) and pragmatic content MathML is no
longer possible: In the current proposal, a pragmatic <cn> would be
translated to an <apply> construction in strict MathML that does not
show that it actually represents an atomic number. We currently see
three ways of solving this:

   1. upgrading the role system in OM2 and MathML3 with a role of
      number-constructor, which would signal that an application of this
      symbol constructs corresponds to a <cn>
   2. doing the same via STS
   3. using a "number_constructors" CD, so that the signal is a
      constructor from this CD.

We should discuss which measures we want to take here.

There are a couple of problems remaining that have to do with infinities
and NaNs from IEEE floats and how to represent these, but I must say
that I do not understand these issues well enough to represent them
here. David has taken the action item to come up with something sensible.

OK, I hope that this sums up the discussion so far.

I would ask you to give your opinions on this matter soon, since the
Math WG has to prepare a Working Draft with code freeze on November 6.
And the more of the issues we have resolved the better the draft will be.

Michael



-- 
----------------------------------------------------------------------
 Prof. Dr. Michael Kohlhase,       Office: Research 1, Room 62 
 Professor of Computer Science     Campus Ring 12, 
 School of Engineering & Science   D-28759 Bremen, Germany
 Jacobs University Bremen*         tel/fax: +49 421 200-3140/-493140
 m.kohlhase at jacobs-university.de http://kwarc.info/kohlhase 
 skype: m.kohlhase   * International University Bremen until Feb. 2007
----------------------------------------------------------------------

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://openmath.org/pipermail/om3/attachments/20081025/5960435d/attachment-0001.html