[Om3] Summary of the Davenport&Kohlhase Proposal

[Florian Rabe]

Hi everybody,

Being among those who initially suggested to have conditions on bound variables, I thought I should join this discussion.

I agree with many of David's objections. However, I think this is because Michael picked the wrong example to sell his suggestion: The justification of conditions is much stronger for binders binding multiple variables.

If there's only a single variable, I can already add a condition like this:

  OMBIND(sum, OMBVAR(OMATTR(OMATP(type,nat), OMATP(condition, prime(x)), OMV(x))), f(x))

(This assumes that bound variables may occur in their own attributions, an issue about which OpenMath 2 is somewhat vague.)

But a problem arises with formulas like this

  \sum_{i,j\in N, i \neq j} f(i,j)

In the following I compare the solutions I know of. To simplify, I put

  ijN := OMBVAR(OMATTR(OMATP(type,N), OMV(i)), OMATTR(OMATP(type,N), OMV(j)))


1) Bind a single variable of product type and use projections whenever a bound variable is used:

  OMBIND(sum, OMBVAR(OMATTR(OMATP(type,{(m,n) \in N\times N | m \neq n}), OMV(x))), f(pi_1(x), pi_2(x)))

pro: works in OpenMath 2
con: it's awful (Even the variable names are lost.)

2) Add an explicit condition child of OMBIND:
  OMBIND(sum, ijN, i \neq j, f(i,j))

pro: nice encoding
con: disruptive language change
     conditions would be marked up more prominently than types, even though they are less important

3) Permit multiple scopes in binders (Kohlhase & Davenport proposal):
  OMBIND(condsum, ijN, i \neq j, f(i,j))

pro: nice encoding
     solves other problems, too: tuples of mutually recursive functions can be represented nicely
con: disruptive language change
     possibly addtional complicated symbols (e.g., condsum) necessary
       (unless the binder's definintion makes the condition arguments optional)
     multiple scopes of binders contrary to mathematical practice/intuition

4) Variant of 4, which wraps the multiple scopes into a tuple:

  OMBIND(condsum, ijN, OMA(vector, i \neq j, f(i,j)))

pro: works in OpenMath 2
con: definitely special symbols like condsum necessary
     no structural correspondence between OpenMath object and representation in, e.g., presentation MathML

5) Variant of 4, which uses a new symbol instead of vector:

  OMBIND(sum, ijN, OMA(conditioned_scope, i \neq j, f(i,j)))

pro: works in OpenMath 2
con: a weird special symbol necessary (Which cd would it be in?)
     a part of the variable declaration occurs as a subterm of the scope

6) Permit attributions to OMBVAR element:

  OMBIND(sum, OMATTR(OMATP(condition, i\neq j), ijN), f(i,j))

pro: very nice encoding
     conceptually a small change
     language gets easier: exclusion of attributions to OMBVAR seems arbitrary anyway
     conditions and types are treated equally, in particular conditions are only optional
con: disruptive language change


My preferences (best first): 6, 3, 2, 5, 4, 1.

Cheers,
Florian

> I'm strongly opposed to this. I'm opposed to the change to OpenMath and
> if we should as a group decide to change OpenMath in this way, I'd still
> argue that MathML would be best advised not to use the new features in
> any mapping to its "strict" subset.
>
> This is a breaking change to OpenMath, with a rather thin
> justification, which is, in total
>
>> James and I don't like that this has two binds and two unrelated dummy
>> variables,
>
> That is, it is introducing a breaking change for purely cosmetic
> reasons.
>
> It wouldn't be impossible to consider change if the change was actually
> an improvement but I don't think it is, for several reasons.
>
> A binding symbol is currently typeable by viewing
>
> ombind
>   head
>   bvar x
>   f(x)
>
> as syntactic sugar for
>
> apply
>   head
>   lambda x. f(x)
>
>
> A binder with multiple children, as proposed here, can thus be seen as
> essentially mapping to the cartesian product of the domains of each of
> the children, but uniquely for openmath the vector construct symbol is
> being omitted. If it is made explict then no extension is needed, and
> only a single child of ombind is needed.
>
> Michael's proposed
>
>   bind(O,v_1,...,v_n,A_1,...A_n)
>
> is just a custom syntax for
>
>
>
>
> bind(O,v_1,...,v_n,
>    apply
>     vector
>      (A_1,...A_n)
>   )
>
>
>> So we are proposing a liberalization of OpenMath objects: all OpenMath2
>> objects are extended Objects and retain their original meanings. But can
>> now define more mathematical symbols and represent more objects.
>
> No, actually you can only represent the same set of objects, with the extra
> complication that there are more ways to do it, so need extra FMP saying
> that they are equivalent, and the extra complication that the new way
> breaks all existing OM applications.
>
>
>> with a new symbol productcond.
>
> Irrespective of whether we extend OMbind, I don't think we should
> explode the number of symbols required by introducing symbols like
> this.
>
> The example Michael happened to pick on had both a domain [0,k] and a
> condition (i !=- j) specified, and the proposed rewrite to a prodcond
> symbol that _requires_ both a domain and a condition (as they are given
> positionally).
>
> It's not particularly common (and never necessary) to specifiy both a
> domain and a condition, so this prodcond symbol would almost always
> require dummy conditions being specified (such as ("true" or default
> domains being specified, to fill in the relevant slots. Or you have yet
> more additional symbols, for product(withdomain) and
> product(justwithcondiition)/
>
>
> In all cases the choice of whether to specify a constraint on a bound
> variable as a domain constraint or a condition is entirely arbitrary.
>
> Saying that a bound variable has domain R is the same as saying it is
> subject to a condition (x in R) and these two formulations should have
> the same openmath encoding, but this proposal arbitrarily distinguishes
> them as
>
>
> ombind
>   prodcond
>   bvar x
>   R
>   true
>   f(x)
>
> and
>
> ombind
>   prodcond
>   bvar x
>   some-superset-of-R
>   apply in x R
>   f(x)
>
>
> In general for a more complicated domain you may, at the authors whim,
> choose to express part of the constraint as a domain and part as a
> condition, so Michael's example
>
> domain:    [0,k]
> condition: i!=j
>
> could just as easily be expressed as
>
> domain:       R
> condition:    i in [0,k] and i!=j
>
> or
>
> domain:     [0,k] \ {j}
> condition:   true
>
>
> or any other alternative, the distinction between domain and condition
> is entirely arbitrary and it's a feature not of problem of OpenMath that
> these are not distinguished.
>
>
> 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.
> ________________________________________________________________________
> _______________________________________________
> Om3 mailing list
> Om3 at openmath.org
> http://openmath.org/mailman/listinfo/om3