[Om3] Language Dictionaries (Was: Re: Initializing OM3 at 2013 Process)

[Lars Hellström]

Michael Kohlhase skrev 2014-05-02 19.09:
> Dear Lars,
>
>
> On 30.4.14 09:23, Lars Hellström wrote:
[snip]
>>>   <schemaext>
>>>     OMNATS = element OMNATS {omel}
>>>     OMNTH = element OMNTH {omel,omel}
>>>     omel |= OMNTH | OMNATS
>>>   </schemaext>
>>
>> Mixing XML and non-XML syntax for something that actually has an XML
>> syntax??
> technically that is no problem, the content is just a text node

Sure, but it's murder on machine-readability.

>> It certainly enhances readability, but no, that's just wrong.
> I am very open here, RNC and RNG are intercompilable.
[snip]
>> (An additional quirk is that this latter type of equality probably
>> isn't the colloquial relation1#eq, but an absolute "there should be
>> absolutely no way within the formal system to tell the difference
>> between these two" invariance under substitution equality.)
> Indeed, nice idea. So you are proposing a meta-level equality symbol for
> these (but not for the inter-language equalities); I have to think about
> this some more.

I guess it could be formalised as a symbol, but I was mostly thinking about 
it in the sense that "rewriting using the translation rules does not change 
the satisfaction status of a formula".

>> I understand EdNote2 as saying that this particular FMP is
>> superfluous, as it would anyway be implied by a similar FMP in the
>> argseq CD. I tend to agree, but note that
there
>> could well be properties of
>> new notation that isn't as natural to state for ordinary symbols.
> yes, that was what I was wondering as well. I guess we need more examples.
>>
>>>   <translation cd="argseq">
[snip]
> In principle we could also use XSLT here, but that is much more
> expressive and would open a great can of worms.

If the main use-case is to preserve some interoperability with MathML3, then 
I suspect XSLT would figure anyway.

>>
>>>     <rule>
>>>       <OMNTH>
>>>         <expr name="n"/>
>>>         <exprlist name="seq">  <expr name="elt"/>  </exprlist>
>>>       </OMNTH>
>>>       <OMA>
>>>         <OMS cd="seqs" name="nth"/>
>>
>> Does that cd="argseq" attribute on the translation element even mean
>> anything? It appears that the symbols that the rules are generating
>> rather reside in the seqs CD.
> Right, I wanted to put the information somewhere which CDs are needed to
> interpret the rule bodies.

OK, so that is essentially the same as the (deprecated!) CDUses element for 
a content dictionary. ;-)

[snip]
>> What would be a more interesting example is a set of translations that
>> cover the whole sequences proposal. Inventing translations for OMNTH
>> and OMNATS is one thing, but OMSEQ and OMSV are much tougher customers
>> (at least if one wants to achieve the intended semantics; it may be
>> that the above already gets it wrong with OMNATS).

To elaborate, I'm pretty sure

<OMA>
   <OMS cd="list3" name="length"/>
   <OMA>
     <OMS cd="list1" name="list"/>
     <OMNATS><OMI>3</OMI></OMNATS>
   </OMA>
</OMA>

is supposed to be 3, but I'd argue that its supposed translation

<OMA>
   <OMS cd="list3" name="length"/>
   <OMA>
     <OMS cd="list1" name="list"/>
     <OMA>
       <OMS cd="seqs" name="nats"/>
       <OMI>3</OMI>
     </OMA>
   </OMA>
</OMA>

will be 1.

>> It is not at all
>> obvious that you would succeed. And is there a proposed standard
>> extension other than the sequences one for which this OMLangExt
>> mechanism would even apply?

I may have answered this positively myself earlier today. On the other hand, 
I'm less sure about syntax relaxations such as the n-ary OMBIND 
(https://trac.mathweb.org/OM3/ticket/136).

>> I don't recall any example of any other
>> introducing new XML elements, so how does one deal with other language
>> extensions?
> Another language extension I would really like to see is record
> structures. That proposal has been made a long time ago, but never
> really pushed. I think we need them for such things as: "Let
> $(R,+,*,0,1,-)$ be a ring." I would like to represent this as "Let
> [base=R,addop=+,mulop=*,addneut=0,mulneut=1,addinv=-] be a ring".

A value of record type? I'd say that is trivially
<OMATTR>
   <OMATP>
     <OMS cd="foo" name="base"/>
     R
     <OMS cd="foo" name="addop"/>
     +
     ...
     <OMS cd="foo" name="addinv"/>
     -
   </OMATP>
   <OMS name="algstruct" cd="foo"/>
</OMATTR>
with base, addop, etc. being semantic-annotations. No language extension needed.

> So
> that we have accessor symbols base, addop, mulop, addneut, mulneut,
> addinv which have natural counterparts in mathematical language. Note
> that I am not necessarily advocating this 5-record over the record
> [addstruct=[base=R,op=+,neut=0,inv=-],mulstruct=[base=R,op=*,neut=1]],

(A framework for this should of course allow both simultaneously, and 
require neither. A specific application of such a framework may of course 
require one or both of them. This is a matter that I've spent quite some 
time thinking about.)

> I
> think we need records and accessors in both cases.

Accessors are just application symbols.

> I know (in principle) how a OMLangExt for this could be written, but
> have not developed one yet.
[snip]
> I guess the question I really want feedback on is whether we should go
> for a OMLangExt-like scheme of extending OpenMath to OM3, which would
> allow us to keep OM2  as a base (and thus be MathML-compatible) while
> extending to (a set of) OM3 languages we can experiment with in the next
> years. Then we can (in a couple of years) see which language extensions
> can be standardized further.

Well, it is certainly a connection that we may seek to establish, but being 
able to establish it should not be a requirement for a proposed extension. 
Either way, there should indeed be a period of some years of 
experimentation. But let's not forget that there is also the intermediate 
goal of cleaning up the OM2.0 standard.

Lars Hellström