[Om3] Initializing OM3 at 2013 Process

Michael Kohlhase m.kohlhase at jacobs-university.de
Fri May 2 19:15:35 CEST 2014


Dear Jan Willem,
On 30.4.14 15:11, Jan Willem Knopper wrote:
> On 23-04-14 15:24, Michael Kohlhase wrote:
>> Dear all,
>>
>> In thinking about OpenMath3, we have problem that there are some
>> language extension proposals, but at the same time, we have the problem
>> that we have to keep MathML3 compatibility. This has been bothering me,
>> but I think I have the beginnings of a solution. I would like to submit
>> the blue note attached to the discussion of our committee.
>>
>> Please give me feedback,
> Some typos:
>
> - The formula (1) seems to be wrong.
> - The relaxng rules in listing 1 differ from those in 3.1.1
thanks.
> Some remarks:
> - is there a description/reference of the language used for the
> translation rules ?
There is a CICM 2008 paper, but I gave one in my response to Lars.
> - it is useful if the translation is machine readable, or even better if
> a conversion/translation rules can be generated.
We have an implementation of the language and (at some point had)  even
an XSLT that generated XSLT from them.
> - furthermore it would be useful if the translation is straightforward
> and if testing if two objects are equal terminates (which I assume is
> the case)
I think that this is the case for extension I showed, but in general,
the equality rules in the target CD can be undecidable (though we
probably want to somehow forbid this).
> - personally I wouldn't use constructions like <OMNTH> and <OMNATS>, but
> I can see how these would be of interest to some people
> - these extensions could previously also be used as "local encodings" of
> OpenMath (since there is a unique translation back to OpenMath). This is
> a nice way of formalizing that.
> However the real motivation seems to come from type theory, and that is
> not easy for me to comment on.
No, I to not think that the motivation comes form type theory, but from
Math, where we use argument sequences as a primitive langauge feature
all the time; unfortunately OpenMath can only partially deal with that
without a sequence extension.
> - how about namespace support ?
>
> - how about attributions ? If a different visualization is implied, than
> it might be nice to generate an attribution. This might be mentioned.
Yes but there is no change wrt. OM2.

Thanks for your comments.

Michael
>
> Best regards,
>
> Jan Willem Knopper
>
> P.S. I don't think Chris Rowley got the doodle poll, since he is not
> subscribed on the om3 list with the correct address. His old address,
> just was removed due to bounces.
>

-- 
----------------------------------------------------------------------
 Prof. Dr. Michael Kohlhase,        Office: Research 1, Room 168
 Professor of Computer Science  Campus Ring 1, 
 Jacobs University Bremen           D-28759 Bremen, Germany
 tel/fax: +49 421 200-3140/-493140  skype: m.kohlhase   
 m.kohlhase at jacobs-university.de http://kwarc.info/kohlhase 
----------------------------------------------------------------------

-------------- next part --------------
A non-text attachment was scrubbed...
Name: m_kohlhase.vcf
Type: text/x-vcard
Size: 320 bytes
Desc: not available
URL: <http://openmath.org/pipermail/om3/attachments/20140502/88148500/attachment.vcf>


More information about the Om3 mailing list