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

[James Davenport]

On Fri, 6 Jul 2007, Michael Kohlhase wrote:
> James Davenport wrote:
> > On Fri, 6 Jul 2007, Michael Kohlhase wrote:
> > > Professor James Davenport wrote:
> > > > On Thu, 5 Jul 2007, Michael Kohlhase wrote:

> > > > 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).
> > Wha worries me is that it begins <apply> but ends </bind>, so I have no
> > idea what was intended.
> Ahh, that was what you were complaining about (and you are right). That is
> just a typo, and I am not sure what I meant either, but since there is no
> <bvar> element I guess it should end in an apply.
And if it were to be evalualted, be sin(b)-sin(a). So this is a
straight-forward application, rather than a binding (nothing is bound).
> > > 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?
>
> I think not (at the language level at least). eta-conversion is tied to
lambda
> (other binding symbols do not have it, e.g. forall or int). So having
> eta-conversion at the OM objects level would not work. But we should
specify
> it in the content dictionary that declares lambda.
True indeed - we culd, and probably should. Looks like a major version
number change, but probably worth it.
> > 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.
>
> why not, they are subject to alpha renaming, which is the litmus test for
> binding.
I don't think they do:
int(sin(x),x) is not the case as int(sin(y),y): one would be -cos(x) and
the other -cos(y).

James