[Om3] Summary of the Davenport&Kohlhase Proposal

[Michael Kohlhase]

On 23.03.2009 23:20 Uhr, David Carlisle wrote:
> 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,
>>      
No, this is _not_ the justification, it is just part of the motivation 
leading to the proposal.

The justification is that with the extension we do not have to force 
math practicioners into using lambdas all the time. Lambdas are nice for 
the enlightened, but really really scary to most mathematicians.
>
> 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)
>    )
>    
In think you are at the heart of the misunderstanding here, this is 
exactly the question Paul asked, the litmus test whether you can do 
something like this, is whether you can define the symbols 0 and vector 
independently of each other. So, if you say that these two are 
equivalent, you should be able to define the symbols for O and vector in 
the productcond case I was making.
>
>    
>> 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.
>    
There are always multiple ways of encoding an object that are 
mathematically equivalent. Even in tricial cases;: you can write the sum 
of A, B, and B as +(A,B,C), +(+(A,B),C), .... So we are not losing 
anything. There is no way that we can make unique representations for 
any part of Math. And it would be foolish to attempth this.
>> 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)
>    
And I would maintain that it needs to distinguish them, and we need to 
maintain the mathematician's freedom to write any of them, just as we 
have to maintain the mathematician's freedom to distinguish 3+5 and 8, 
even though they are mathematically equivalent. One of the stated design 
goals of OpenMath since the beginning is that it does not build in any 
kind of evaluation (i.e. equivalence transformation) except 
alpha-conversion of bound variables. Therefore we need to distinguish 
different (but mathematically equivalent representations.
> 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.
>    
I am sorry, I think you have it totally wrong. OpenMath says that the 
meaning of the XML encodings are OpenMath objects, that can already now 
in OpenMath2 distinguish many similar things, even if you pack them 
under a lambda as you are proposing. So why should be force people to 
conflate objects they consider different where the differences are of 
basically the same magnitude.

Michael

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

-- 
----------------------------------------------------------------------
  Prof. Dr. Michael Kohlhase,       Office: Research 1, Room 62
  Professor of Computer Science     Campus Ring 12,
  School of Engineering&  Science   D-28759 Bremen, Germany
  Jacobs University Bremen*         tel/fax: +49 421 200-3140/-493140
  m.kohlhase at jacobs-university.de http://kwarc.info/kohlhase
  skype: m.kohlhase   * on Sabbatical in Auckland (NZ) until VII/2009
----------------------------------------------------------------------