Go backward to 3.1 The Datatype Set Go up to 3 Sets, Relations, and Functions Go forward to 3.3 Predicates as Sets |
We call < x_{0}, x_{1}, ..., x_{n-1}> an n- tuple (Tupel).
<x_{0}, x_{1}, ..., x_{n-1}>_{0} = x_{0}; <x_{0}, x_{1}, ..., x_{n-1}>_{1} = x_{1}; ... <x_{0}, x_{1}, ..., x_{n-1}>_{n-1} = x_{n-1}.
Please do not confuse in above proposition a variable name x_{i} with the application of the tuple selector ._{i} to a tuple t, denoted as t_{i}. 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 (x_{0}, x_{1}, ..., x_{n-1}).
Let U:=< 2, T, {1}>. Then
T_{0} = 1; T_{1} = 2.
U_{0} = 2; U_{1} = T; U_{2} = {1}.
<x_{0}, x_{1}, ..., x_{n-1}> = <y_{0}, y_{1}, ..., y_{n-1}> <=> (x_{0} = y_{0} /\ x_{1} = y_{1} /\ ...x_{n-1} = y_{n-1}).
<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:
An n-ary tuple is then constructed from 2-tuples as
t_{0} := such x: exists y: t = <x, y>; t_{1} := such y: exists x: t = <x, y>.
<x_{0}, x_{1}, ..., x_{n-1}> := <x_{0}, < x_{1}, < ..., <x_{n-2}, x_{n-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.
S_{0} x ... x S_{n-1} := {<x_{0}, ..., x_{n-1}>: x_{0} in S_{0} /\ ... /\ x_{n-1} in S_{n-1}}.
In the Logic Evaluator, we define the binary Cartesian product as follows: