Go backward to 3.4 Functions as Sets Go up to 3 Sets, Relations, and Functions |
While we could extend tuples accordingly, we have a more convenient concept to model sequences of objects of arbitrary (possibly infinite) length:
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) :=A finite sequence over S is a sequence of length n over S, for some n:
such n in N: exists S: s is a sequence of length n over S.
s is a finite sequence over S : <=>An infinite sequence over S is a function from N, the natural numbers, to S:
exists n in N: s is a sequence of length n over S.
s is an infinite sequence over S : <=> s: N -> S.
Sequences appear under various names:
The i-th component s(i) of a sequence s is also denoted as
[2, 3, 4, 4, 5].The length of S is 5 and we have
S_{0} = 2, S_{1} = 3, S_{2} = 4, S_{3} = 4, S_{4} = 5.We also have
forall i in N_{5}: 0 < S_{i} < 10.Take the infinite sequence T := {<i, i^{2}>: i in N}, i.e.,
[0, 1, 4, 9, 16, 25, ...].We have
forall i in N: S_{i} = i^{2}.
The same concept may be extended to two dimensions.
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:
which is typically depicted as:
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>}
We have
1 2 3 4 5 6 7 8 9
forall i in N_{3}, j in N_{3}: 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:
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_{0} != i}.
A := new(5, 0)[3 |-> 1][2 |-> 5][4 |-> 1][2 |-> 3].Then we have length(A) = 5 and
A_{0} = 0, A_{1} =0, A_{2} = 3; A_{3}=1; A_{4}=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]).