[Om] Binder arguments

[Lars Hellström]

Professor James Davenport skrev:
> On Sat, June 13, 2009 4:28 pm, Lars Hellström wrote:
>> Here's another question I've encountered while examining how my needs
>> might be dressed in OM symbols. I think I know the answer already, but
>> it's still a good starting point for a discussion:
> This is indeed a good question: see Davenport/Kohlhase in MKM 2009 (early
> version at http://opus.bath.ac.uk/13079 for one point of view,

Ah, that seems to reach the same conclusion as I did: The restriction 
ought to be lifted. Nice!

> but there
> are others, notably the view that the "standard theory" of bing only
> allows one object for the binding to govern.

Is that www.bing.com?

>>    Why can binders only take one argument (last child of OMBIND,
>>    which is specified to have exactly three children), when an
>>    application is allowed any number of arguments?
>>
>> An elementary case where one might want to do this is that of the
>> ordinary definite integral
>>
>>    \int_a^b f(x) \,dx
>>
>> which one might expect to encode as something like
>>
>> <OMBIND>
>>    <OMS name="naive_integral"/>  <!-- role: binder -->
>>    <OMBVAR> <OMV name="x"/> </OMBVAR>
>>    <OMV name="a"/>
>>    <OMV name="b"/>
>>    <OMA> <OMV name="f"/> <OMV name="x"/> </OMA>
>> </OMBIND>
>>
>> were it not for said fact that a binder can (in OM2) only have one
>> argument, not the three of a, b, and f(x) as needed here.

It occurs to me that /for this example/, the technique (shown in the 
above Davenport--Kohlhase) of using a composite object as binder --

<OMBIND>
   <OMA>
     <OMS name=integralfromto"/>
     <OMV name="a"/>
     <OMV name="b"/>
   </OMA>
   <OMBVAR> <OMV name="x"/> </OMBVAR>
   <OMA> <OMV name="f"/> <OMV name="x"/> </OMA>
</OMBIND>

-- might actually be preferable since this would allow (even if it can 
be considered poor style) writing things like F(x) = \int_0^x f(x) dx 
without getting the inner and outer x's mixed up, thanks to the fine 
print about the variable not being bound in the first child of an 
OMBIND. This doesn't solve my problem, as there the extra arguments 
would all contain bound variables, but it might be helpful for others.


>> There seems to be no technical reason for this restriction, as neither
>> the XML nor the binary OM encoding need invoke arity to parse a
> This is correct. Unfortunately (from my pont of view) the abstract
> description does : see 2.1.3(iv) on page 14.

Yes, that's what I thought of when I wrote "prefix notation"... It 
doesn't look all that formalised, though -- maybe changing

   binding(B,v_1,...,v_n,C)
to
   binding(B;v_1,...,v_n;C)

would do the trick (as far as the needs in the specification are 
concerned)?


>> If memory serves, relaxations of OMBIND is one (the only?) change to
>> OM3 that is considered as needed to bring it in line with
>> Content-MathML3, but I don't know where I might have read that. Perhaps
>> someone else could elaborate on the current status of that issue?
> I can't speak on behalf on MathML.

No, but it's the only change *to OM* considered, is it not? Or do you 
mean there could be people on the MathML side who want additional 
changes in OM?

>> Now, since previously my informal examples were misunderstood by some,
>> I suppose I'd better give you my real example this time. My reason to
>> consider defining a binder in the first place is that I want to encode
>> Abstract Index Notation expressions
>> (http://en.wikipedia.org/wiki/Abstract_index_notation), which is an
>> abstraction of the Einstein notation for tensors -- e.g.
> I'd better look at this is in more detail before shooting from the hip.

Yes, it's quite a lot to wrap one's head around. Originally the 
variables were thought to range over elements of a basis for the 
underlying space, but the choice of basis is irrelevant, and the 
notation works even when the underlying space doesn't have a basis 
(e.g. is a non-free module), so one ends up with variables that are 
just labels...

I might add that there is a "higher order" alternative -- where the 
primitives are morhpism composition, tensor product, and actions of 
permutations -- to the "first order" abstract index notation. The roles 
are reversed in the sense that it is the higher order notation that is 
canon, whereas the first order notation is often regarded as somewhat 
of a curiousity, but those that do calculations tend to go for the 
first order notation.


Lars Hellström