previous up next
Go backward to 3.1 The Datatype Set
Go up to 3 Sets, Relations, and Functions
Go forward to 3.3 Predicates as Sets
 RISC-Linz logo

3.2 Tuples

The elements in a set do not have a particular order, i.e., there is no "first", "second", or "last" set element. The concept of containers that preserve a particular order among their components needs some additional mechanisms.

Proposition 27 (Tuple) For every n, there is an n-ary function < > (the  tuple constructor) and n unary functions .0, .1, ..., .n-1 (the  tuple selectors or  projections) such that for all x0, x1, ..., xn-1 we have
<x0, x1, ..., xn-1>0 = x0;
<x0, x1, ..., xn-1>1 = x1;
...
<x0, x1, ..., xn-1>n-1 = xn-1.
We call < x0, x1, ..., xn-1> an n- tuple (Tupel).

Please do not confuse in above proposition a variable name xi with the application of the tuple selector .i to a tuple t, denoted as ti. Please also note that we use the same symbol < > for the tuple constructors of all arities and the same function symbol .i for the selection of the i-th component of every n-tuple with i<n. Frequently, tuple construction is just denoted by (x0, x1, ..., xn-1).

Example  Let T:=< 1, 2>. Then
T0 = 1;
T1 = 2.
Let U:=< 2, T, {1}>. Then
U0 = 2;
U1 = T;
U2 = {1}.

Proposition 28 (Equality of Tuples) Two n-tuples are equal if and only if their components are equal, i.e., for every n and all x0, x1, ..., xn-1 and all y0, y1, ..., yn-1, we have
<x0, x1, ..., xn-1> = <y0, y1, ..., yn-1> <=>
(x0 = y0 /\  x1 = y1 /\  ...xn-1 = yn-1).
Example 
<1, 2> != <2, 1>;
<1, 2> != <1, 2, 2>.

Construction from Sets  Tuples are not a basic concept: they can be built from sets as follows. First, we define the constructor for 2-tuples as

<x, y> := {{x}, {y, x}}.
If x=y, then t has a single element {x} that determines both x and y. If x != y, then t contains two elements {x} and {x, y}. The 1-element set determines x and its complement in the 2-element set determines y. Thus the selectors can be uniquely defined as:
t0 := such x: exists y: t = <x, y>;
t1 := such y: exists x: t = <x, y>.
An n-ary tuple is then constructed from 2-tuples as
<x0, x1, ..., xn-1> := <x0, < x1, < ..., <xn-2, xn-1>>>>
with the selectors being defined accordingly.

Logic Evaluator  The constructor < > is represented by the function tuple with selector .i being represented as (prefix) .i; the predicate = can be also applied to tuples. The unary predicate Tuple returns true for tuples only.

Definition 23 (Cartesian Product) The  Cartesian Product (Kartesisches Produkt) of n sets S0, ..., Sn-1 is the set of all n-tuples whose i-th component is in Si:
S0 x ... x Sn-1 := {<x0, ..., xn-1>: x0 in S0 /\  ... /\  xn-1 in Sn-1}.

In the Logic Evaluator, we define the binary Cartesian product as follows:

Author: Wolfgang Schreiner
Last Modification: October 4, 1999
previous up next