   Go backward to 3.4 Functions as SetsGo up to 3 Sets, Relations, and Functions ## 3.5 Sequences and Matrices

Tuples are intended to model sequences of objects of a fixed length; for every n-tuple, there are n unary functions to select each component of the tuple but there is no binary function that takes a tuple t and an arbitrary index i and returns the i-th component of t.

While we could extend tuples accordingly, we have a more convenient concept to model sequences of objects of arbitrary (possibly infinite) length:

Definition 30 (Sequence) A  sequence (Folge) of length n over S is a function from Nn, the set of the first n natural numbers, to S:
s is a sequence of length n over S : <=> s: Nn -> S.
The  length of a finite sequence s is that n such that s maps Nn to some S:
length(s) :=
such n in N: exists S: s is a sequence of length n over S.
A  finite sequence over S is a sequence of length n over S, for some n:
s is a finite sequence over S : <=>
exists n in N: s is a sequence of length n over S.
An  infinite sequence over S is a function from N, the natural numbers, to S:
s is an infinite sequence over S : <=> s: N -> S.

Sequences appear under various names:

• tables,
• arrays,
• vectors,
• lists.

The i-th component s(i) of a sequence s is also denoted as

• si;
• s[i];
• s.i.

Example  Take the sequence S := {<0, 2>, <1, 3>, <2, 4>, <3, 4>, <4, 5>} typically written as
[2, 3, 4, 4, 5].
The length of S is 5 and we have
S0 = 2, S1 = 3, S2 = 4, S3 = 4, S4 = 5.
We also have
forall i in N5: 0 < Si < 10.
Take the infinite sequence T := {<i, i2>: i in N}, i.e.,
[0, 1, 4, 9, 16, 25, ...].
We have
forall i in N: Si = i2.

The same concept may be extended to two dimensions.

Definition 31 (Matrix) A  matrix (Matrix) with m rows and n columns over S is a function from Nm x Nn to S:
M is a m x n-matrix over S : <=> M: Nm x Nn -> S.

A matrix component M(<i, j>) is often denoted as:

• M(i, j);
• M[i, j];
• Mi, j.

Example  Take the matrix
 M := { <<0, 0>, 1>, <<0, 1>, 2>, <<0, 2>, 3>, <<1, 0>, 4>, <<1, 1>, 5>, <<1, 2>, 6>, <<2, 0>, 7>, <<2, 1>, 8>, <<2, 2>, 9>}
which is typically depicted as:
 1 2 3 4 5 6 7 8 9
We have
forall i in N3, j in N3: Mi, j = 3i+j+1.

The matrix concept can be extended to an arbitrary number of dimensions in an alogous way.

When constructing sequences or matrices by iterative updates, the following notations come handy:

Definition 32 (Sequence Updates) The n-element a-sequence is the sequence of length n that maps every index to a:
new(n, a) := {<i, a>: i in Nn}.
The sequence constructed from s by setting i to a is the same as s with the exception that i is mapped to a:
s[i |-> a] := {<i, a>} union {t in s: t0 != i}.

Example  Take the sequence
A := new(5, 0)[3 |-> 1][2 |-> 5][4 |-> 1][2 |-> 3].
Then we have length(A) = 5 and
A0 = 0, A1 =0, A2 = 3; A3=1; A4=2.

Logic Evaluator  We can only represent finite sequences; we define the sequence functions `len`(s) (based on the function `#`(s) that gives the number of elements in a set s), `new`(n, a) and `[]`(s, i, a) (i.e, s[i |-> a]).

Author: Wolfgang Schreiner
Last Modification: October 4, 1999   