[Trac] [OpenMath] #31: containers are used as binding symbols in MathML2

[OpenMath]

#31: containers are used as binding symbols in MathML2
----------------------------+-----------------------------------------------
     Reporter:  kohlhase    |          Owner:  jhd             
         Type:  proposal    |         Status:  new             
     Priority:  major       |      Milestone:  MathML3CD Draft1
    Component:  MathML CDs  |        Version:                  
   Resolution:              |       Keywords:                  
Include_gantt:  0           |   Dependencies:                  
   Due_assign:  YYYY/MM/DD  |      Due_close:  YYYY/MM/DD      
----------------------------+-----------------------------------------------
Comment (by david):

 Replying to [comment:3 jhd]:

 > Ye Gods. I have no idea what this means in ordinary mathematics.

 I'm with you James:-)

 Surely these examples are confused aren't they? (certainly their readers
 are confused:-)

 mathml2 (1st edn) was explicit that the bvar version of set could only be
 used with condition, to form the set of x satisfying some condition.

 mathml 2 (2nd edition) generally expanded the notion of qualifier,
 although for set it seems slightly broken as it refers to 4.2.3.2
 Operators taking Qualifiers
 which lists which operators take which qualifiers, but it fails to list
 set.
 That could be fixed in mathml3, but surely if interval is used as a
 qualifier then its sense is [a,b] means the condition a <= x and x <= b,
 for a bound variable x, as specified by the bvar element. So you can't use
 the bound variable as the end point of the interval can you? what set is
 meant by "the collection of all intervals from 0 to x." is x a free
 variable here?

 I don't think that there's really a problem here for openmath, we need two
 symbols, one nary one that constructs a set from an explicit list,
 modelling {1,2,3}
 and one constructing a set from a predicate {x| x in [a,b]} the fact that
 they both map to the pragmatic <set> element with or without a bvar child
 is just general
 notation mangling isn't it? This of course is more or less exactly what
 the original entry says, so no objection to that, but the examples seem
 strange to me.


 David

-- 
Ticket URL: <https://trac.kwarc.info/OM3/ticket/31#comment:4>
OpenMath <http://www.openmath.org>
The development of the OpenMath Standard and Content Dictionaries.