[Om3] Binding Integral symbols (was [Fwd: MathML CDs])

[James Davenport]

On Fri, 6 Jul 2007, Michael Kohlhase wrote:
> Professor James Davenport wrote:
> > On Thu, 5 Jul 2007, Michael Kohlhase wrote:
> > I was proposing a new CD which would support some of the MathML2 uses
of
> > int.
> > I had not seen the 'binder' form in MathML 3. Now I do. I must say
that i
> > don't understand it, though. Incidentally, can any-one explain the
> > following:
> > <apply><Int/> <interval><ci>a</ci><ci>b</ci></interval> <cos/> </bind>
> > (from C.3).
> >
> James, please keep in mind that the content MathML spec was written with
I was actually not aware of this - thanks for telling me.
> OpenMath alignment in mind, and I was experimenting with the notion of
> interval there. This is just an (experimental) translation of the
OpenMath
Whay worries me is that it begins <apply> but ends </bind>, so I have no
idea what was intended.
> practice into MathML syntax. It was met with some resistance. The
existence of
> this in the draft does not mean that we don't need the binding form.
What worries me is that I understand the binding form for definite
integration. The variable is not free in the result. But it is indefinite
that I do not understand
> > >
> > Ah yes, I understand, but what would this return?
> > In OpenMath this would be a unary function., equivalent to -cos.
> >
> Well, as you know in OpenMath we always pride ourselves that we do not
> necessarily have evaluation in mind, so your question is somewhat
meaningless
True indeed. By return, I mean 'be considered as'.
> :-). But this aside, you are right, for the indefinite integral to be
> evaluated, one would have to have some function constructor to represent
the
> result. So maybe the indefinite integral should not have a binding role,
> because it can be done with a lambda as in the OM tradition.
> > IF that's the same in MathML3 (and I don't know) then your suggestion
is
> > reasonable.
> >
> I would think it is, and it would be our duty to specify that, if we
allowed a
> binding role for the indefinite integral.
> > It is, of course, only a variant on <OMA>
> > <OMS name="int" cd="calculus1"/>
> > <OMBIND>
> > <OMBVAR><OMV name="x"/></OMBVAR>
> > <OMA><OMS cd="specfun1" name="sin"/><OMV name="x"/></OMA>
> >  </OMBIND>
> > </OMA>
> >
> I assume that you only forgot a <OMS cd="fns1" name="lambda"/> in as the
first
Ouch - I did indeed.
> child of the OMBIND. I would actually put this as an FMP into the CD, if
we
> allow a binding role for the indefinite integral.
If this is 'roughly' what we mean, then it indeed ought to be precisely
what we mean, which I think it what you are saying.
> > which in itself is a convoluted way of saying
> > <OMA>
> > <OMS name="int" cd="calculus1"/>
> > <OMS cd="specfun1" name="sin"/>
> > </OMA>
> >
> I would agree mathematically, but not OpenMathematically (we do not build
> evaluation into OpenMath Objects remember :-)).
No but do we (this is, as far as I can tell open, and I don't remember
any discussion of it) allow eta-conversion?
> > But if you differentiate your expression, you get, essentially, lambda
x
> > sin x, so I don't see this point.
> >
> No, the differentiation operator is also a binding operator in MathML (and
> many Mathematicians also view it as such as I recall). So we will have to
> provide a binding differentiation operator as well
No - you will laos have to remove the non-binding operator, which I would
be unhappy with. I am actually unhappy with a binding differentiation for
the same reasons as I am a binding indefinite integration: I don't think
they BIND the variables.
> > Aha - this is a broader discussion.
> >
> Yes, what do you think?
I would need to think harder, and look again.
James