Re: on "strict" MathML

Andreas, Thanks for your comments.

I think one problem is that you are looking at the November draft of
MathML 3. This had a very rough first cut at refactoring Content MathML
with the "Strict" subset aligned with OpenMath. As a working group we've
done a lot of work on it since then, in fact the principle reason for
the delay in getting out another official draft is that work on chapter
4 is still progressing.

However as previously mentioned on this list, it's possible to follow
the current state of play at 

http://monet.nag.co.uk/~dpc/draft-spec/

which is a CVS checkout of from the source control, so that draft
changes without notice (watch the automated date in the red flash on the
front cover, which is the cvs check-in date)


The rules mapping from MathML to its strict subset have been completely
reworked since November and in particular the principle that
condition,interval,lowlimit,uplimit qualifiers are syntactic variants
of domainofapplication is, I hope, now correctly maintained.


One other general constraint that you need to be aware of is that for
assorted organisational reasons the mapping has to be a mapping to
OpenMath2. So while it is possible to envision improvements to OpenMath
to make OpenMath3, and those improvements could filter to some future
mapping from MathML 3.x to a Strict Content MathML 3.x subset, the
Subset defined in mathML3 has to align with what we have in OpenMath
today.

Of course if we think there are possible or probable changes in OpenMath
and a mapping to current OpenMath can be designed in such a way that any
future changes cause minimum impact that would be a good thing. So while
it's not entirely out of scope to discuss changes to OM (and of course
entirely in scope for the original context of your paper as a submission
to OM2009) the amount to which such changes can affect MathML3 is
severely limited.

> Principle 2. The pattern apply(operator, bvar(vars), body) is semantically
> equivalent to the pattern apply(operator, lambda(bvar(vars), body)).

This is more or less the case in the current draft see

http://monet.nag.co.uk/~dpc/draft-spec/chapter4.html#contm.dombind-strict

which expresses this.

__personally__ I think things would have been a lot better if OM2 had not
introduced OMBIND and just had OMLambda (and what's currently encoded
in OpenMath as
OMBIND 
  head
  bvars
  body

would have been encoded as

OMA
  head
  OMLambda
    bvars
    body

which would have made OM2 simpler and made the mapping from MathML3
easier as well, but OM2 is what it is so I think we have to support
OMBind usage, and existing symbols (like forall and exists) which are
specified in the OM2 CDs as doing their own binding using OMBind rather
than being a symbol which you apply to a function term.

This causes a couple of extra "special case" rules in the mapping
but isn't I think a mjor complication and is just the price you pay for
having a history rather than the freedom of doing version 1 of a
language:-)

So given that OM has OMBind and an explicit aim of this refactoring
is to align with OpenMath I think that it is inevitable that we add
<bind> rather than suggesting everything is rewritten in terms of the
(existing) <lambda>.

One of the "problems" that the current rewrites try to address is that
MathML2 did not consistently use apply/bvar in a way consistent with
principle 2.

For example x is free not bound in

<apply>
  <int/>
  <bvar><ci>x</ci></bvar>
  <apply><times/><ci>x</ci><ci>x</ci></apply>
</apply>



bvar is used to specify the "variable of integration" even though it's
not bound in that form, only in the case of definite integration.

this is why in the current editors draft there is an explicit rewrite

http://monet.nag.co.uk/~dpc/draft-spec/chapter4.html#contm.p2s.int

which first binds x, does the integration and then makes x free again,
ie saying the above is syntactic shorthand for

<apply>
<apply>
  <int/>
  <lambda>
  <bvar><ci>x</ci></bvar>
  <apply><times/><ci>x</ci><ci>x</ci></apply>
  </lambda>
</apply>
<ci>x</ci>
</apply>

Similar "special cases" apply to diff and partialdiff, and other
symbols.


In other words, I don't agree with your final example in section 3

The following are equivalent:
{ apply(int,bvar(x),apply(sin,x))
{ apply(int,lambda(bvar(x), apply(sin,x)))

as the first is, I believe the expression cos x, in which x is free, and
the second is  the function term cos or equivalently lambda x. cos x

If we took the view that bvar always implied binding the variable, then
MathML would have no way to say that if you differentiate the polynomial
x^2 wrt x you get 2x (as opposed to the different polynomial 2y)

> OpenMath 2 does have the equivalents of MathML 2's apply and of its
> apply with a bvar qualifier. The latter, however, severely restricts the type of
> heads it accepts (although it did not do so in OpenMath 1),

I'm confused by this remark, OMBIND in both the text description of
OpenMath Objects, and in the schema for the XMl encoding, accepts an
arbitrary OpenMath term as head, could you clarify?


> Note that fns1:domainofapplication does not at this point have a precise deni-
> tion;

You are being polite there:-) As far as I can see the definition is
completely nonsensical (and probably my error) the only description
given for domainofapplication is mathml alignment but its STS signature
is that of domain (probably cut and paste error) so rather than restrict
the domain of a function, it (presumably) is a synonym for domain()
which, given a function returns its domain.

In

http://monet.nag.co.uk/~dpc/draft-spec/chapter4.html#contm.strict-doa

we've suggested using a new symbol from an (extended) fns1 CD that
does mirror what you need for mathml's domainofapplication.

provisionally it's called fns1:restriction (with
fns1:domainofapplication being deprectaed)

http://monet.nag.co.uk/~dpc/cdfiles2/cd/fns1.xhtml#restriction

these updated CDs will be presented formally at the OM meeting, I hope.


You make a lot of other good points and we should work through your
principles and see how far the current rewrites adhere to them,
so I won't respond in detail to all your points here but I wanted to make
an initial response just to thank you for the review  and to confirm
we'd got it, and also to encourage you to watch the editors draft as
chapter 4 is being worked on at present.


So further comments will no doubt follow. Also these are personal
comments not a WG view (although we have a teleconference this
afternoon, when this will no doubt be discussed)

Thanks again,

David

________________________________________________________________________
The Numerical Algorithms Group Ltd is a company registered in England
and Wales with company number 1249803. The registered office is:
Wilkinson House, Jordan Hill Road, Oxford OX2 8DR, United Kingdom.

This e-mail has been scanned for all viruses by Star. The service is
powered by MessageLabs. 
________________________________________________________________________

Received on Thursday, 14 May 2009 09:49:09 UTC