[Om] Binder arguments
David Carlisle
davidc at nag.co.uk
Mon Jun 15 02:01:09 CEST 2009
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.
________________________________________________________________________
More information about the Om
mailing list