James Davenport – one of the originators of OpenMath is presenting the current status. (OpenMath and MathML are converging and although they are distinct I shall confalte them here).
What is the formal semantics? OM has 4 flags:
- official
- experimental
- private
- obsolete
Normally only the official and obsolete are visible on the official http://www.openmath.org site.
What if we have conflict? An exampls is systems (like Euclid) which start from 1 whereas OpenManth may start from 0. (I’m on weak ground here…). MathML has ContentDictionaries (CD) for representing each approach – but we need a mechanism for conversion.
This is very similar to the CML idea of convention attribute.
For example the British and the French have different symbolisms for integrals. They aren’t just linguistic. In CD sqrt(-1) is i, in engineering it is j.
Do we skate over inconsistencies or refuse to emit any results where there are conflicts?
“A theorem prover which emits wrong results is probably worse than useless.” [A chemistry system which emits wrong compounds? Of course. (but most of the current ones do].
Is notation independent of semantics? Apparently not. And it’s a harder problem that in looks to convert. How do we speak:
T(n) = O(n2)
Apparently no mathematician would speak “equals” – they would say “is in”. JD is suggested a “notation” approach (I see this as similar to CML’s convention). So our symbology is much deepr than we usually realise.
So OM defines a smallish set of symbols which are fundamental. This are hardcoded. (In chemistry these migh be element symbols, coordinates, etc.) Then there are those that OM uses widely but are not fundamental, and then those that the community develops – they have to be supported by OM, but are not part of it.
I’ll stop here – I hope you get the idea that OM is struggling to formalize those things which are absolute, those which are universal but not fundamental, and those which are widely used. If those words (which are mine not James’) conflict, that’s probably accurate.
He finishes:
“OM is useful, but being semantic, let’s use it carefully”. That goes for CML as well.
My message is that MLs are community processes, depend heavily on interpreting implicit semantics, and in doing so will help to formalize our understanding.
Maths has a community process. CML is much less advanced, but uses the Blue Obelisk as a clearing house. But I take from OM and communities like FOAF that CML should have flags on its components such as
- accepted
- experimental
- convention (e.g. JSpecView)
- obsolete