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

[Professor James Davenport]

On Thu, 5 Jul 2007, Michael Kohlhase wrote:
> could you explain what you have done to the CDs, I have had a short look at
I was proposing a new CD which would support some of the MathML2 uses of 
int.
> integration, which I consider the most pressing problem in the alignment. The
> situation I see is the following: MathML has a binder symbol for integration
> and OpenMath an appliccative one. (I see that you have added an indefinite
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).
> integral to the CD below to account for the two usages of <int> in MathML).
> 
> I think that the binding symbol for integrals is important to support, I mean
> a usage of the following form:
> 
> <OMBIND>
> <OMS name="int" cd="newint"/>
> <OMBVAR><OMV name="x"/></OMBVAR>
> <OMA><OMS cd="specfun1" name="sin"/><OMV name="x"/></OMA>
> </OMBIND>
Ah yes, I understand, but what would this return?
In OpenMath this would be a unary function., equivalent to -cos.
IF that's the same in MathML3 (and I don't know) then your suggestion is 
reasonable.
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>
which in itself is a convoluted way of saying
<OMA>
  <OMS name="int" cd="calculus1"/>
  <OMS cd="specfun1" name="sin"/>
</OMA>
> 
> This usage of the integral allows to view it as an operation on an expression
> with a (bound) variable and does not force one to use the \lambda (which in my
> recollection mathematicians do not like, and I do not like, as I want to be
> able to use integration in logics that do not supply a \lambda). So I think we
But if you differentiate your expression, you get, essentially, lambda x 
sin x, so I don't see this point.
> need a symbol for binding integral.
> 
> Please also see the my first e-mail  to the list
> [http://openmath.org/pipermail/om3/2007-June/000002.html], if we adopt having
> more than one role per symbol, then we could use the same symbol for the
> binding usage above and the apliccative below, and get by with one symbol.
Aha - this is a broader discussion. 
James