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 [email protected] http://kwarc.info/kohlhase ----------------------------------------------------------------------
<<attachment: m_kohlhase.vcf>>
_______________________________________________ Om3 mailing list [email protected] http://openmath.org/mailman/listinfo/om3
