[Om3] Summary of the Davenport&Kohlhase Proposal

[David Carlisle]

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. 
________________________________________________________________________