[Om] Binder arguments

[Lars Hellström]

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