Go backward to 3.3 Predicates as Sets
Go up to 3 Sets, Relations, and Functions
Go forward to 3.5 Sequences and Matrices
|
Go backward to 3.3 Predicates as Sets Go up to 3 Sets, Relations, and Functions Go forward to 3.5 Sequences and Matrices |
|
Like relations provide a set theoretic substitute for predicates, we can also model functions by sets. In fact, functions are just considered as special relations.
A partial function (partielle Funktion/Abbildung) from A to B is a function that is a relation between A and B:
f is a function : <=> f is a binary relation /\ forall x, y0, y1: (<x, y0> in f /\ <x, y1> in f) => y0=y1.
A (total) function (totale Funktion/Abbildung) from A to B is a partial function from A to B where every element of A is in relation to some element of B:
f: A ->partial B : <=> f is a function /\ f subset A x B.
f: A -> B : <=> f: A ->partial B /\ forall x in A: exists y in B: <x, y> in f.
Since a function is a relation, the notions domain, range, inverse, and composition also apply to functions (but see the comments on function inversion below).
While above definition only introduces unary functions, the case of n-ary functions (for every n) is reduced to the unary case by taking a Cartesian product as the function domain: e.g. a function
f: A x B -> Cmaps a tuple <a, b> with a in A and b in B to some value c in C.
Logic Evaluator We define the corresponding predicates
Function(f) (i.e., f is a function),
isPartialFunction(f, A, B) (i.e., f:
A ->partial B) and
isFunction(f, A, B) (i.e., f:
A -> B)
as follows:
The result of a function application is determined by "looking up" the set that represents the function.
f(x) := such y in range(f): <x, y> in f.
Since f is a function, above statement indeed defines a unique y in range(f) for every x in domain(f).
Please note that this definition introduces a binary function `()' ("apply") that takes two arguments f and x. This syntax is convenient to hide the distinction between set-theoretic functions and function constants. We are now able to quantify over functions as in
forall y: exists f: forall x: f(x)=ywith the understanding that f denotes a particular set and above formula has to be interpreted as
forall y: exists f: forall x: <x, y> in f.
Instead of writing f(<x0, ..., xn-1>), we usually simply write f(x0, ..., xn-1).
Logic Evaluator We can define the binary function
apply(f, x) (i.e., f(x)) as follows:
Notation Functions are usually defined in one of the following formats (where x is a variable and T is a term):
f: A -> B x |-> T
f: A -> B f(x) := T
f: A -> B f := lambda x. T
f(x: A): B = T
or, equivalently, as
f: A -> B /\ forall x in A: f(x) = T
f = {<x, T>: x in A} /\ forall x in A: T in B.
If the function domain is a Cartesian product, we usually write
to denote
f: A0 x ... x An-1 -> B f(x0, ..., xn-1) := T
f: A0 x ... x An-1 -> B f(t) := let x0 = t0, ..., xn-1 = tn-1: T.
should be read as
div: N x N -> Q div(x, y) := x/y;
div := {<<x, y>, x/y>: x in N, y in N} /\ forall x in N, y in N: div(x, y) in Q.
Function Inversion While the inverse of a function is well defined, it is not necessarily a function.
f-1 = {<0, 0>, <0, 1>, <1, 2>}is a binary relation but not a function, because it contains <0, 0> and <0, 1>.
We will learn in Proposition Inverse of a Function under which condition the inverse of a function is indeed a function.
On the other hand, we have the following result.
f o g: A -> C.
(1) (f o g): A ->partial C; (2) forall x in A: exists y in C: <x, y> in (f o g).
We know (3) from the definition of o ; we still have to show (4). Take arbitrary x, y0, y1 and assume
(3) (f o g) subset A ×C; (4) forall x, y0, y1: (<x, y0> in (f o g) /\ <x, y1> in (f o g)) => y0=y1.
We have to show y0 = y1.
(5) <x, y0> in (f o g); (6) <x, y1> in (f o g).
From (5), (6), and the definition of o , we know y0 in C, y1 in C, and
By (7), we have some b0 in B such that <x, b0> in f /\ <b0, y0> in g; by (8), we have some b1 in B such that <x, b1> in f /\ <b1, y0> in g. From <x, b0> in f, <x, b1> in f and the fact that f is a function, we know that b0 = b1. From this and from <b0, y0> in g, <b1, y1> in g, and the fact that g is a function, we know that y0 = y1.
(7) exists b in B: <x, b> in f /\ <b, y0> in g; (8) exists b in B: <x, b> in f /\ <b, y1> in g.
(4) exists y in C: <x, y> in (f o g).From (3) and f: A -> B, we know (5) <x, f(x)> in f and (6) f(x) in B. From (6) and g: B -> C, we know (7) <f(x), g(f(x))> in g and (8) g(f(x)) in C.
To show (4), we take (9) y := g(f(x)) and show
We know (10) from (8) and (9). To show (11), we have to show, by definition of o , that
(10) y in C; (11) <x, y> in (f o g).
We know (12) from (3), (8), and (9). To show (13), we take (14) b := f(x) and have to show:
(12) x in A /\ y in C; (13) exists b: <x, b> in f /\ <b, y> in g.
We know (15) from (5) and (14). We know (16) from (7), (9), and (14).
(15) <x, b> in f; (16) <b, y> in g.
As a consequence, we have the following "direct" characterization of function composition.
forall x in A: (f o g)(x) = g(f(x)).
We then have the following result:
forall A, B, C, D, f: A -> B, g: B -> C, h: C -> D: f o (g o h)=(f o g) o h
forall x in A: (f o (g o h))(x) = ((f o g) o h)(x).Take arbitrary x in A. Then we have by Proposition Function Composition
(f o (g o h))(x) = (g o h)(f(x)) = h(g(f(x))) = h((f o g)(x)) = ((f o g) o h)(x).
Commutative Diagrams Relationships between functions and composite functions are often stated by a diagram where the nodes represent sets and an arrow f between nodes A and B indicates that f is a function from A to B. A path from one node to another represents the composition of all the functions represented by the individual arcs on the graph. The diagram is said to commute if any two paths with same initial node and same terminal node represent the same function, e.g., the diagram
asserts that h = f o g for f: A -> B and g: B -> C and h: A -> C. The diagram
says that f o g = h o k, for f: A -> B, g: B -> D, h: A -> C, k: C -> D. Proposition Associativity of Function Composition is asserted by the following diagram:
