Re: on "strict" MathML

David,
thank you very much for your reply. I will take a look at the current
state of affairs - I did go through a few months of archive when I
rejoined the list a few weeks ago, but I clearly missed the reference to
the working copy -sorry. I'm glad to hear that my gravest concerns have
already been taken care of.
>   
>> 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.
>   
I couldn't agree more. It would have made my attempt some years back of
putting together a formal semantics of *all* of OpenMath (my MKM'04
paper) much easier, too - and the resulting formal semantics much
cleaner, as well.
> 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>.
>   
My idea was, of course, that bvar always means bound variable, so that
any time a bvar appears inside an apply a transformation to OM would do
the conversion to OMBIND, and there would be no need to introduce a bind
element in MathML.
> 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>
>
>   
I have long considered this kind of example - in fact, a formula quite
similar to this one combined with the one below appears in my '98 paper,
I believe (\int dx = \int_{}^x dx, I believe the example was). My
interpretation was, back then, that this is an example of how
mathematical formulas mirror principles of human language, in that
repetition of the obvious is strongly discouraged. My conclusion back
then was that a correct interpretation of mathematical formulas may
require ideas from linguistics; in this case, treating the upperbound x
as an implicit ingredient of this formula.
>
> 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.
>   
As I said, I agree with the rewrite in principle, but I don't see how
this improves the OpenMath 2 match, since the calculus1 CD appears to be
quite consistent with  a view that integration transforms functions into
functions, which in turn is completely in tune with a notion that the
bvar inside an apply with an int head is a true bound variable.
> 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
>   
I understand your point, but I believe that both are lambda terms, that
is, that cos x is simply a shorthand for the function lambda x. cos x. 
The added meaning of x as the x axis is pragmatics rather than
semantics, to be added from context - again, human language does this
all the time.
> 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)
>   
Good example. In my interpretation, differentiation is done over
function spaces, i.e., it maps lambda x. x^2 to lambda x. 2x. The fact
that these are meant to be equivalent to polynomials over x (rather than
y) is again implicit from the context. The MathML <share> concept could
be ideal for capturing this. In real life, explicit conversions may need
to be inserted, or a special differentiation operator over polynomial
rings defined.
>> 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?
>   
I hope you're right - that would be a huge relief. It was my
understanding from the time that OM2 was being defined that one of the
big changes from OM1 to OM2 implied that something like
ombind(oma(restrict,oma(lift2big,assocop),D),bvar(x),body) (with a
compund head) was no longer allowed, nor was
ombind(myassocop,bvar(x),body) (with myassocop  being a regular
function, not binder). I noticed that Michael Kohlhase responded to a
question on this mailing list fairly recently in a way that made me
suspect that this continued to be the case, saying that one would have
to use "big" operators instead of "small" ones in strict mathml because
they'd be heads of a bind construct.

But perhaps you can just map to OM2 as if it did allow arbitrary ombind
heads, if that turns out to be necessary. This would be a simple enough
change for OM3 to incorporate if necessary, after all. It would be all
that would be needed to introduce a restrict operator into OM that
properly mirrors domainofapplication, I think.

Best,
 -- Andreas

Received on Thursday, 14 May 2009 19:29:54 UTC