Formal Foundations of Computer Science 1 -- 3.5 Sequences and Matrices

Go backward to 3.4 Functions as Sets
Go 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 N_n, the set of the first n natural numbers, to S:

s is a sequence of length n over S : <=> s: N_n -> S.

The length of a finite sequence s is that n such that s maps N_n 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

s_i;
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

S₀ = 2, S₁ = 3, S₂ = 4, S₃ = 4, S₄ = 5.

We also have

forall i in N₅: 0 < S_i < 10.

Take the infinite sequence T := {<i, i²>: i in N}, i.e.,

[0, 1, 4, 9, 16, 25, ...].

We have

forall i in N: S_i = i².

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 N_m x N_n to S:

M is a m x n-matrix over S : <=> M: N_m x N_n -> S.

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

M(i, j);
M[i, j];
M_{i, 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 N₃, j in N₃: M_i,
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 N_n}.

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: t₀ != i}.

Example Take the sequence

A := new(5, 0)[3 |-> 1][2 |-> 5][4 |-> 1][2 |-> 3].

Then we have length(A) = 5 and

A₀ = 0, A₁ =0, A₂ = 3; A₃=1; A₄=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