B5. FUNCTIONS AND SEQUENCES
1. Pairs and Functions
The distinguishing feature of ordered pairs, or simply "pairs", is
that they have a first and a second element.
(forall (p) (1)
(if (pair p)
(exists (x y) (and (first x p)(second y p)))))
We could define pairs in the traditional way in set theoretic terms.
The pair is defined as the set {x, {y}}. This is certainly a
model of the axioms involving "pair", but it would be pedantic to call
this the definition.
Two pairs are equal exactly when their first elements are equal and
their second elements are equal.
(forall (p1 p2) (2)
(if (or (pair p1)(pair p2))
(iff (equal p1 p2)
(and (pair p1)(pair p2)
(forall (x1 y1 x2 y2)
(if (and (first x1 p1)(second y1 p1)
(first x2 p2)(second y2 p2))
(and (equal x1 x2)(equal y1 y2))))))))
That is, if either p1 or p2 is a pair, then they are equal if and only
if they are both pairs, their first elements are equal, and their
second elements are equal.
The first and second elements of a pair are unique.
(forall (p x1 x2) (3)
(if (and (pair p)(first x1 p)(first x2 p))
(equal x1 x2)))
(forall (p y1 y2) (4)
(if (and (pair p)(second y1 p)(second y2 p))
(equal y1 y2)))
A function f from a set s1 to a set s2 is a set of pairs where each
element of s1 occurs exactly once as the first element in a pair, and
every element of s2 occurs as a second element of at least one pair.
We will call this predicate "function0" because in Chapter B7 we will
extend it to functions from scales to scales as well.
(forall (f s1 s2) (5)
(iff (function0 f s1 s2)
(and (set s1)(set s2)
(forall (p)
(if (member p f)
(and (pair p)
(forall (x y)
(if (and (first x p)(second y p))
(and (member x s1)
(member y s2)))))))
(forall (x)
(if (member x s1)
(exists (p)
(and (member p f)(first x p)))))
(forall (p1 p2 x)
(if (and (first x p1)(first x p2)
(member p1 f)(member p2 f))
(equal p1 p2)))
(forall (y)
(if (member y s2)
(exists (p)
(and (member p f)(second y p))))))))
Lines 4-10 of this definition say that a function is a set of pairs,
the first elements of which come from s1 and the second elements of
which come from s2. Lines 11-14 say that there is a value of the
function for every element of s1. Lines 15-18 say that that value is
unique. Lines 19-22 say that every element of s2 is a value of some
member of s1 under the function f.
We won't use these terms formally, but we can call s1 the domain of
the function and s2 the range.
(forall (f s1 s2) (if (function0 f s1 s2)(domain s1 f))) (6)
(forall (f s1 s2) (if (function0 f s1 s2)(range s2 f))) (7)
If f is a function from s1 to s2, we will say that f maps an element x
of s1 into an element y of s2 when the pair is a member of f.
(forall (f x y) (8)
(iff (map f x y)
(exists (s1 s2 p)
(and (function0 f s1 s2)(member p f)
(first x p)(second y p)))))
That is, "(map f x y)" means "f(x)=y".
As an aside, we note that when we have a Skolem function, or a
functional dependency, we have a corresponding function.
(forall (y1 y x1 x e s1 s2) (9)
(if (and (skfct y1 y x1 x e)(typelt x s1)(rangeFd s2 y x e))
(exists (f)
(and (function0 f s1 s2)
(forall (p)
(iff (and (pair p)(first x1 p)(second y1 p))
(member p f)))))))
2. Sequences
Here we will assume we have the positive integers, as described in
Chapter B9. The expression "(posInteger n)" says that n is a positive
integer.
The expression "(ints s n1 n2)" says that s is the set of all positive
integers from n1 to n2, including n1 and n2.
(forall (s n1 n2) (10)
(iff (ints s n1 n2)
(and (posInteger n1)(posInteger n2)(set s)
(forall (n)
(iff (member n s)
(and (posInteger n)(leq n1 n)(leq n n2)))))))
A sequence of length n is a function whose domain is the first n
positive integers.
(forall (s) (11)
(iff (sequence s)
(exists (s1 s2 n)
(and (function0 s s1 s2)(ints s1 1 n))))))
We define "length" as follows:
(forall (n s) (12)
(if (sequence s)
(iff (length n s)
(exists (s1 s2)
(and (function0 s s1 s2)(ints s1 1 n))))))
The nth element in a sequence is the entity in the range of the
function that n is mapped into.
(forall (s n y) (13)
(if (sequence s)
(iff (nth y n s)(map s n y))))
The first element of a sequence is the nth element where n is 1.
(forall (s y) (14)
(if (sequence s)
(iff (first y s)(nth y 1 s))))
Note that "first" is the same predicate we used for the first element
of a pair. Formally, there is no confusion because all axioms
involving the predicate "first" are conditioned on its second argument
being either a pair or a sequence. Intuitively, any confusion is
harmless, because the set of pairs is isomorphic to the set of
sequences of length two.
The rest of a sequence is the sequence that remains after the first
element is removed.
(forall (s1 s) (15)
(iff (rest s1 s)
(and (sequence s)(sequence s1)
(forall (i x)
(iff (map s1 i x)
(exists (j)
(and (gt j 1)(successor j i)
(map s j x))))))))
The expression "(rest s1 s)" says that s1 is the rest of s (after the
first is removed). For example, the sequence viewed as a
function maps 2 to b. Then the sequence ** maps 1 to b.
The last element of a sequence is the nth element where n is the
length of the sequence.
(forall (s y m) (16)
(if (and (sequence s)(length n s))
(iff (last y s)(nth y n s))))
An entity is in a sequence if it is the nth element of the sequence
for some n.
(forall (x s) (17)
(iff (inSeq x s)
(exists (n) (nth x n s))))
If one element's n is less than another's, it is before the other in
the sequence.
(forall (x y s) (18)
(iff (beforeInSeq x y s)
(exists (n1 n2)
(and (sequence s)(nth x n1 s)(nth y n2 s)
(lt n1 n2)))))
We won't need infinite sequences.
Predicates Introduced in this Chapter
(pair p): p is an ordered pair.
(first x p): x is the first element of a pair or sequence.
(second y p): y is the second element of a pair.
(function0 f s1 s2): f is a function from s1 to s2.
(domain s1 f): s1 is the domain of function f.
(range s2 f): s2 is the range of function f.
(map f x y): The function f maps x to y; f(x)=y.
(ints s n1 n2): s is the set of positive integers from n1 to
n2, including n1 and n2.
(sequence s): s is a sequence.
(length n s): n is the length of the sequence s.
(nth y i s): y is the ith element of sequence s.
(rest s1 s): s1 is the rest of the sequence s after the
first element of s.
(last y s): y is the last element of sequence s.
(inSeq y s): y is an element of the sequence s.
(beforeInSeq x y s): x comes before y in the sequence s.
In addition, the following predicates will be explicated in Chapter
B9.
(posInteger n): n is a positive integer.
(leq n1 n2): n1 is less than or equal to n2.
(successor n1 n): n1 is the successor of n; n1=n+1.
(lt n1 n2): n1 is less than n2.
The constant 1 will also be explicated there.
**