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

[Michael Kohlhase]

Professor James Davenport wrote:
> 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).
>   
James, please keep in mind that the content MathML spec was written with 
OpenMath alignment in mind, and I was experimenting with the notion of 
interval there. This is just an (experimental) translation of the 
OpenMath 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.
>> 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.
>   
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 :-). 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 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.
> 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 :-)).
>> 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.
>   
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
>> 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. 
>   
Yes, what do you think?

Michael
> James
>   

-- 
----------------------------------------------------------------------
 Prof. Dr. Michael Kohlhase,       Office: Research 1, Room 62 
 Professor of Computer Science     Campus Ring 12, 
 School of Engineering & Science   D-28759 Bremen, Germany
 Jacobs University Bremen*         tel/fax: +49 421 200-3140/-493140
 m.kohlhase at jacobs-university.de http://kwarc.info/kohlhase 
 skype: m.kohlhase   * International University Bremen until Feb. 2007
----------------------------------------------------------------------