Language Extension Dictionaries

[jbs1]

migrated from Trac, where originally posted by lars_h on 24-Jul-2014 8:37pm

Submitting for Michael Kohlhase ;-)

MK proposes "a language extension mechanism for OpenMath that will allow us to introduce new language features (as have been called for by the community) while keeping the underlying core language intact so that we can maintain compatibility with MathML3 and the upcoming ISO standard."

A paper (http://ceur-ws.org/Vol-1186/paper-14.pdf) on this was presented (and at some length discussed) at OM2014 in Coimbra. MK promised to return with an updated version of that paper, which may thus get attached to this ticket.

From the paper and subsequent discussion, key features of the proposal appears to be:

1. The set of valid OM objects is not extended, but the set of XML documents that constitute valid OM objects is.

• However, some suggested applications (e.g. using a full sequences extension to encode infinite sequences and then present them in ellipsis form) would suggest that phrasebooks may parse extended OM documents into some extended OM object representation and then make use of that.
  1. Every piece of new syntax is given with a canonical translation to old syntax, and encodes the exact same OM object as its translation would. The translations will typically employ helper symbols from some content dictionary created to support the extension.
  2. Language extensions are to be defined in "Language Extension Dictionary" documents. These may contain "equalities", which are analogous to Formal Mathematical Properties, except for describing properties of the new language elements rather than properties of symbols in a CD.
  3. Phrasebooks are supposed to handle language extensions at a "language level", which apparently is more fundamental than the level at which ordinary symbols in a CD are handled.
• This could mean that phrasebooks are not expected to read LEDs at runtime, but should rather have support for some set of language extensions built in at compile-time, and reject all documents using additional extensions.

[kohlhase]

moved to OpenMath/OMSTD#14