[Om] Binder arguments
Lars Hellström
Lars.Hellstrom at residenset.net
Thu Jun 18 12:21:48 CEST 2009
David Carlisle skrev:
> 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.
Yes, you should; it seems you've made some presumptions about the
nature of variables in mathematical notation that AIN provides a
counterexample to.
But in order to see this, you may need something more worked out than
the wikipedia page (I intended it mostly to serve as a disambiguation,
as it is not uncommon that different mathematical communities have
different names for the same thing, or use the same name for very
different things). At
http://abel.math.umu.se/~lars/diamond/AIN.pdf
you may find an excerpt that rigorously establishes the notation,
although within a framework slightly different from that of the
wikipedia page, namely that of a general PROducts-and-Permutations
category (PROP). The corresponding excerpt introducing and defining
these is at
http://abel.math.umu.se/~lars/diamond/PROP.pdf
-- you'll find that some ordinary notations used in AIN.pdf are defined
in PROP.pdf.
[rewind]
> 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.
You mean, they haven't been approved yet? I don't see any technical or
logical problems with the idea, so if you do, you'd need to spell them out.
> 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).
What are you requiring here?
One obvious approach for sts-typing binders would be to simply
disregard the OMBVAR child, and type-declare the rest as for an
application. A (possibly multiple) definite integral with condition
could then be something like
<OMA>
<OMS cd="sts" name="bindermapsto"/>
<OMS cd="sts" name="BooleanValue"/>
<OMS cd="sts" name="NumericalValue"/>
<OMS cd="sts" name="NumericalValue"/>
</OMA>
i.e., when the first child of OMBIND has this type, then the third
child must be a BooleanValue, fourth (=final) child must be a
NumericalValue, and the OMBIND element as a whole counts as a
NumericalValue. The only binder-ish piece of mathematical notation that
I can think of that would be less than fully cared for by this is
fns1#lambda, but that's rather special.
One might also want to go further: associating types to bound
variables, as those might be related to types of the binder as a whole;
but that is orthogonal to the issue of multiple binder arguments.
> 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)
The problem with a drive to extend the syntactic role of fns1#lambda is
that it reduces the semantic content of the symbol. Using it for all
binding tasks in K-14 math might be consistent with its semantic as
constructing a function -- something mapping values to values -- but it
wouldn't work for AIN, as the abstract index variables there don't have
values.
> or one
> could imagine a primitive OMLAMBDA (or perhaps OMBIND with no explict
> head child which would be defined to mean a lambda construuctor)
That would be preferable, but it's still just a dumber version of OMBIND.
> 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
While it may be eminently appropriate for a phrasebook to make this
kind of identification, I find it deeply disturbing that a standard
purporting to care for all of mathematics should make it, as it would
cover up distinctions that may well be of interest.
> 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.
Yet another meaning (which to me seems far more plausible than the
multiple return values one) is that the different children can have
different roles in specifying the resulting function... but then we've
better add a head symbol to specify which roles the various children
have, don't you think? Oops, that brings us back to OMBIND with
multiple arguments! ;-)
> Your example of bounds on an integration
[Sigh!] Why is it, that every time I present an elementary example on
this list just to suggest where I'm going, someone jumps at it as if it
was _all_ that I'm interested in?
As it seems I'll have to get down into the technical details, I've put
a more genuine example at
http://abel.math.umu.se/~lars/diamond/symocat-example.xml. The outline
of it is
<OMA>
<OMS cd="relation1" name="eq"/>
<OMBIND>
<OMS cd="symocat1" name="fuse"/>
<OMBVAR>
<OMV name="a"/><OMV name="b"/><OMV name="c"/>
<OMV name="d"/><OMV name="e"/><OMV name="f"/>
<OMV name="g"/><OMV name="h"/><OMV name="i"/>
<OMV name="j"/><OMV name="k"/>
</OMBVAR>
<OMA>
<OMS cd="list1" name="list"/>
<OMV name="j"/>
<OMV name="a"/>
</OMA>
<OMA>
<OMS cd="arith1" name="times"/>
<OMA>
<OMS cd="symocat1" name="label"/>
<OMS cd="Hopf-algebra" name="mult"/>
<OMA>
<OMS cd="list1" name="list"/>
<OMV name="a"/>
</OMA>
<OMA>
<OMS cd="list1" name="list"/>
<OMV name="b"/>
<OMV name="c"/>
</OMA>
</OMA>
[... 6 more factors have been elided ...]
</OMA>
<OMA>
<OMS cd="list1" name="list"/>
<OMV name="d"/>
<OMV name="h"/>
</OMA>
</OMBIND>
<OMBIND>
<OMS cd="symocat1" name="fuse"/>
<OMBVAR>
<OMV name="a"/><OMV name="h"/>
</OMBVAR>
<OMA>
<OMS cd="list1" name="list"/>
<OMV name="h"/>
<OMV name="a"/>
</OMA>
<OMS cd="alg1" name="one"/>
<OMA>
<OMS cd="list1" name="list"/>
<OMV name="a"/>
<OMV name="h"/>
</OMA>
</OMBIND>
</OMA>
> though wouldn't want either of
> these interpretations, as the scope of the bound variable does not
> include the specification of the limits,
I had already observed that, but our mails probably crossed paths.
> 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,
It's a _possible_ encoding, but that doesn't make it natural; at least
not for the community at large. In e.g. Maple, you've long had the
choice between
int(x^3,x=a..b)
and
int(x->x^3,a..b),
but even though the language favours the latter (due to scoping
problems brought on by not actually binding x in the former), people
generally tend to use the former, presumably because they find it more
natural.
> 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.
I strongly disagree!
> 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.
Is that even possible for foundational work?!? Forall is a primitive in
first-order logic, whereas /lambdas/ are at best syntactic sugar.
Sure, other foundations may have lambda as primitive, but it is not up
to OM or MathML to single one out as the preferred foundation for
mathematics!
> 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.
Taken in the context of e.g. ZF or NBG set theory, this would be
entirely due to DWIM'iness on the part of MathML.
>> -- 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.
That there is only one defint symbol which gets thrown (and therefore
is supposed to interpret) all sorts of domains may well be a problem --
there's ambiguities concerning Lebesgue vs. improper Riemann integral,
for one, and then there's the whole range of choices for limits in the
latter, so it would definitely be preferable to have several integral
symbols whose expectations for the domain specifications were clearly
documented -- but this is indeed an issue at CD content level rather
than standard content level, though I would maintain that the problem
lies more with calculus1 than with intervall. And it is of course
orthogonal to the issue of whether there ought to be binder integrals.
Lars Hellström
More information about the Om
mailing list