[Om] Binder arguments

[Professor James Davenport]

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, but there
are others, notably the view that the "standard theory" of bing only
allows one object for the binding to govern.
>    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.
>
> 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.
>
> 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.
>
> 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.

James Davenport
Visiting Full Professor, University of Waterloo
(and also at the University of Western Ontario)
Otherwise:
Hebron & Medlock Professor of Information Technology and
Chairman, Powerful Computing WP, University of Bath
OpenMath Content Dictionary Editor and Programme Chair, OpenMath 2009
IMU Committee on Electronic Information and Communication