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