[Trac] [OpenMath] #23: sort out symbols for associative binary operators, e.g. union

[OpenMath]

#23: sort out symbols for associative binary operators, e.g. union
----------------------------+-----------------------------------------------
     Reporter:  kohlhase    |          Owner:  jhd       
         Type:  proposal    |         Status:  new       
     Priority:  blocker     |      Milestone:  CD3 Draft1
    Component:  MathML CDs  |        Version:            
   Resolution:              |       Keywords:            
Include_gantt:  0           |   Dependencies:            
   Due_assign:  YYYY/MM/DD  |      Due_close:  YYYY/MM/DD
----------------------------+-----------------------------------------------
Old description:

> MathML allowed big operators for associative operators like union. We
> need a general template how to deal with these symbols.
>
> In the phone call today, we distinguished three symbols that we will
> probably need. They are the same from the deep semantics but different on
> a representational level.
>
> For set union, we have
>
> union       =    union at set1   (the nary-associative union operator)
> union-coll  =    big_union at set3 (from the Eindhoven CDs).
> union-expr  =    union at MathML (the binding operator over expression with
> a bvar).
>
> all of these names are just for the local discussion. The first two have
> the natural role "application" the latter role "binding".
>
> For union-expr, the MathML WG tentatively suggested the name
> big_union at set1.
>
> We need to decide what good names for these symbols should be, and into
> which content dictionaries they should go.

New description:

 MathML allowed big operators for associative operators like union. We need
 a general template how to deal with these symbols.

 In the phone call today, we distinguished three symbols that we will
 probably need. They are the same from the deep semantics but different on
 a representational level.

 For set union, we have

 union       =    union at set1   (the nary-associative union operator)

 union-coll  =    big_union at set3 (from the Eindhoven CDs).

 union-expr  =    union at MathML (the binding operator over expression with a
 bvar).

 all of these names are just for the local discussion. The first two have
 the natural role "application" the latter role "binding".

 For union-expr, the MathML WG tentatively suggested the name
 big_union at set1.

 We need to decide what good names for these symbols should be, and into
 which content dictionaries they should go.

Comment (by kohlhase):

 Replying to [ticket:23 kohlhase]:

 > We need to decide what good names for these symbols should be, and into
 which content dictionaries they should go.

 I think they should all go into set1, we should not have more than one CD
 per topic in the MathML set.

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