[Om] Binder arguments

[David Carlisle]

Lars,

   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?


While there have been several suggestions to relax this rule, there
hasn't been any agreement on what such an extension should meen.
That's not to say any of the proposals individually (the most recent
been from James and Michael) are broken, just that there is no real
basis for allowing such a construct.

ombind is a slightly awkward part of openmath which is noticable in for
example the fact that a bindiing symbol can't really be described in sts
(or anything else). It might be useful to follow MathML3's example and
more formally view constructs like this as things that can be rewritten
to something else. In this case the natural thing to rewrite to is a
lambda expression (which unfortunately isn't a primitive, but one could
either use (as the rewrites in MathML3 draft do, lambda from fns1) or one
could imagine a primitive OMLAMBDA (or perhaps OMBIND with no explict
head child which would be defined to mean a lambda construuctor)
in any case, 

OMBIND
  head
  bvars
  expression-in-bvars

ought to be seen as syntactic sugar for


OMA
  head
  OMLAMBDA <!-- or <OMBIND><OMS cd="fns1 name="lambda"/> -->
    bvars
    expression-in-bvars

so the question about what an ombind with multiple children should mean
has two natural answers, the mathml3 draft (when interpretting an apply
with bound variables and multiple children) makes an application of the
head term to a set of arguments constructed by separately
lambda-abstracting  each of the original children,

see

http://www.w3.org/TR/MathML3/chapter4.html#contm.dombind-strict

An alternative meaning would be to say an ombind with multiple children
related to a lambda term with multiple children, which could, perhaps,
be made to model a system that supported multiple return values from
functions.

Your example of bounds on an integration though wouldn't want either of
these interpretations, as the scope of the bound variable does not
include the specification of the limits, so the natural encoding there
is the one OM uses, which is to view it not as a top level binding but
as an _application_ of an integrate function to two terms, one
expressing the limits of integration, and the second term being a
function, perhaps constructed with an explict lambda binder, or perhaps
not. (or perhasp more natural would have been to have three arguments,
lowlimit, highlimit and function, avoiding issues with the interval
construct that you mention)

>  binders are extremely rare among the official and contributed CDs on
>  openmath.org! 

Yes because usually (actually always) it's more convenient to delegate
all binding to lambda, and to encode the "binding operation" as an
application on the lambda term.

Even the prototypical binding operations of forall and exists would
better have been expressed not as binders but as functions mapping
a function term to a truth value. As Andreas commented recently on this
list that would have enabled MathML (for example) to give a far more
uniform translation of <domainofapplication> into openmath, where
normally it is interpreted as restricting the domain of a function, but
for forall and exists we have to give  special rules which modify the
predicate, if we want to use the binders in quant1.

> I suppose a lambdification of formulae can be an ideological choice or
> at least personal preference from core OM developers,
certainly some of us:-)

> -- except that interval1#interval doesn't construct a set (which is 
> what one would expect) but rather some sort of "formal interval", as

Yes that's a point somewhat hidden in the current Cds, there is a plan
to clarify it (and to introduce an explict "ordered_interval" symbol,
but I think that's mainly  editorial improvements to the intervall CD
rather than an indication of a real flaw in the system.

Sorry I haven't commented on the details of the binding operation that
you need for Abstract Index Notation expressions. It's late and not an
area that I'm familiar with. I'll read the reference you pointed to
before commenting.

David


________________________________________________________________________
The Numerical Algorithms Group Ltd is a company registered in England
and Wales with company number 1249803. The registered office is:
Wilkinson House, Jordan Hill Road, Oxford OX2 8DR, United Kingdom.

This e-mail has been scanned for all viruses by Star. The service is
powered by MessageLabs. 
________________________________________________________________________