From: Andreas Strotmann <andreas.strotmann@ualberta.ca>

Date: Thu, 14 May 2009 13:29:04 -0600

Message-ID: <4A0C7100.7090602@ualberta.ca>

To: David Carlisle <davidc@nag.co.uk>

CC: www-math@w3.org

Date: Thu, 14 May 2009 13:29:04 -0600

Message-ID: <4A0C7100.7090602@ualberta.ca>

To: David Carlisle <davidc@nag.co.uk>

CC: www-math@w3.org

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, -- AndreasReceived on Thursday, 14 May 2009 19:29:54 UTC

*
This archive was generated by hypermail 2.3.1
: Tuesday, 6 January 2015 21:27:41 UTC
*