[Om] Tuple and list : any distinction?

Michael Kohlhase m.kohlhase at jacobs-university.de
Thu Feb 18 18:09:34 CET 2010

Dear Joe,

there are at least two possible answers to this question:


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 

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.


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,


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

More information about the Om mailing list