[Om] Tuple and list : any distinction?

[Michael Kohlhase]

Dear Joe,

On 18.02.10 18:56, Joe Collins wrote:
> Dear Michael,
>
> Most of what you write is roughly consistent with what I have understood, and
> helps a little more with the OpenMath flavor.
> I was a little thrown by "Semantics of OpenMath and MathML3", Kohlhase&  Rabe,
> where:
>
> Definition 3 (OM Context). An OM context C is an n-tuple of variables
> which we will write as<x1 , . . . , xn>. We will use + for tuple
> concatenation and $\in$ for tuple membership.
>
> implies tuple concatenation is normal.
>    
Ha, nice answer,
> (Sorry, I didn't mean to knock you for inconsistency).
>    
this definition was actually written by my (formalist) co-author, who 
was aware of the same isomorphism you were enquiring about. Indeed we 
were talking about argument sequences there where lists and tuples are 
equally far from the "real intuition", therefore I went along with this.

BTW, I consider the representation of argument sequences as one of the 
remaining problems of OpenMath, as we do not have a real means to 
represent equations like f(a,x_1,...,x_n) = g(x_1,...x_n)-a. Mathematica 
has a good way of doing this which OM lacks.
> Let me, however, get straight to my real concern.
> I want to represent a coordinate variable tuple like (X, Y, Z) or
> (r, theta, phi). I do NOT consider these "vectors" in general.
> I was considering using tuple to construct them, but then needed a
> means of indexing them. Either adding a "tuple_selector" symbol or using the
> existing list symbols seemed to be the two best options, with my preference
> towards the "tuple_selector" symbol.
> After this feedback on the OpenMath flavor of things, my preference has
> increased in that direction.
>
> If you ask "Why not 'vectors'?", I'll ask
> "What does it mean to add
> (r1, theata1, phi1) + (r2, theata2, phi2)  ?".
>
> (Things aren't sufficiently interesting if you stay in Cartesian coordinates!)
>    
I think that in this case you really are nearer to "vectors". But you 
can always make your own tuples CD that does what you want. I am pretty 
sure that you do not want to use ECC, since with the tuple constructor 
you would "buy" all the rest of a (very complex) lambda calculus that 
most people would probably consider a Meta-Logic.

I encourage you to make a CD and contribute it to OM.

Michael
>
> Regards,
> Joe
>
> Michael Kohlhase wrote:
>    
>> Dear Joe,
>>
>> there are at least two possible answers to this question:
>>
>> Mathematical:
>>
>> generally spoken, tuples and lists are isomorphic as data raw
>> structures, but support conceptually different operations. Tuples are
>> usually thought of as having fixed length and operations are between
>> tuples of same length. Operations are mostly from linear algebra. In the
>> ecc CD we have dependent tuples that are mostly used for defining
>> functions.
>>
>> Lists are thought of as of variable length, and the operations are
>> mostly constructing lists from the empty list by prepending, appending
>> lists, mapping functions over lists,.... Moreover, lists typically only
>> have members of the same "type".
>>
>> So, even though everything you do with tuples,  the mathematical,
>> operational  intuitions are quite different.
>>
>> Formally:
>>
>> The levels of formality in the descirption of ecc and list1/2 are vastly
>> different. ECC (Extended Calculus of Construction) is a logical system,
>> where tupling has a very well-defined role. list1/2 is a (intendedly)
>> vague description of a vocabulary of lists without going into too much
>> detail, so that it can be universally used.
>>
>> hope this helps,
>>
>> Michael
>>
>> On 17.02.10 14:51, Joe Collins wrote:
>>      
>>> The OpenMath ecc CD defines Tuple and the list1 CD defines list.
>>>
>>> Is there any essential distinction between Tuple and list?
>>> If so, what?
>>>
>>> Some of the definitions in list1, list2 suggest (to me) that the order
>>> of the
>>> list elements are arbitrary. Is this actually the case?
>>>
>>> Joe
>>>
>>>        
>>      
>    

-- 
----------------------------------------------------------------------
  Prof. Dr. Michael Kohlhase,        Office: Research 1, Room 62
  Professor of Computer Science  Campus Ring 1,
  Jacobs University Bremen           D-28759 Bremen, Germany
  tel/fax: +49 421 200-3140/-493140  skype: m.kohlhase
  m.kohlhase at jacobs-university.de http://kwarc.info/kohlhase
----------------------------------------------------------------------