[Om] Binder arguments

Professor James Davenport jhd at cs.bath.ac.uk
Sat Jun 13 19:24:33 CEST 2009


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



More information about the Om mailing list