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

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.

Definition 28 (Function) A  function (Funktion) is a binary relation where every element of the domain is in relation to at most one element of the range:
 f is a function : <=> f is a binary relation /\ forall x, y0, y1: ( in f /\  in f) => y0=y1.
A  partial function (partielle Funktion/Abbildung) from A to B is a function that is a relation between A and B:
 f: A ->partial B : <=> f is a function /\ f subset A x B.
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 -> B : <=> f: A ->partial B /\ forall x in A: exists y in B: 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 -> C
maps a tuple <a, b> with a in A and b in B to some value c in C.

Example  The following are functions:
• 0;
• {<0, 0>, <1, 0>, <2, 1>, <3, 2>};
• {<x, x^2>: x in N};
• {<x, x2>: x in N /\  x is even} union {<x, 0>: x in N /\  x is odd};
• {<x, y>: x in N /\  y in N /\  x+y = 100};
• {<<x, y>, x+y>: x in N /\  y in N}.
The following are not functions:
• {<0, 0>, <0, 1>};
• {<x, x2>: x in N /\  x is prime} union {<x, 0>: x in N /\  x is odd};
• {<x, y>: x in N /\  y in N /\  x+y <= 100};

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.

Definition 29 (Function Application) Let f be a function and let x in  domain(f). The  value (Wert) of f at x is the y such that <x, y> in f:
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)=y
with 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
All of this is to be interpreted as
 f: A -> B /\  forall x in A: f(x) = T
or, equivalently, as
 f = {: x in A} /\  forall x in A: T in B.

If the function domain is a Cartesian product, we usually write

 f: A0 x ... x An-1 -> B f(x0, ..., xn-1) := T
to denote
 f: A0 x ... x An-1 -> B f(t) := let x0 = t0, ..., xn-1 = tn-1: T.

Example  The statement
 div: N x N -> Q div(x, y) := x/y;
should be read as
 div := {<, 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.

Example  Take function f = {<0, 0>, <1, 0>, <2, 1>}. Then
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.

Proposition 32 (Function Composition) The composition of two functions is also a function, i.e., for all A, B, and C, and all f: A -> B and g: B -> C, we have:
f o g: A -> C.

Proof  Take arbitrary A, B, C, f: A -> B, and g: B -> C. We have to prove f o g: A -> C, i.e., by definition of o , that
 (1) (f o g): A ->partial C; (2) forall x in A: exists y in C: in (f o g).
• We prove (1), i.e., by definition of ->partial , that
 (3) (f o g) subset A ×C; (4) forall x, y0, y1: ( in (f o g) /\  in (f o g)) => y0=y1.
We know (3) from the definition of o ; we still have to show (4). Take arbitrary x, y0, y1 and assume
 (5) in (f o g); (6) in (f o g).
We have to show y0 = y1.

From (5), (6), and the definition of o , we know y0 in C, y1 in C, and

 (7) exists b in B: in f /\  in g; (8) exists b in B: in f /\  in g.
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.
• We prove (2). Take arbitrary (3) x in A. We have to show
(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

 (10) y in C; (11) in (f o g).
We know (10) from (8) and (9). To show (11), we have to show, by definition of o , that
 (12) x in A /\  y in C; (13) exists b: in f /\  in g.
We know (12) from (3), (8), and (9). To show (13), we take (14) b := f(x) and have to show:
 (15)  in f; (16)  in g.
We know (15) from (5) and (14). We know (16) from (7), (9), and (14).

As a consequence, we have the following "direct" characterization of function composition.

Proposition 34 (Function Composition) For all A, B, and C, and all f: A -> B and g: B -> C, we have:
forall x in A: (f o g)(x) = g(f(x)).

We then have the following result:

Proposition 35 (Associativity of Function Composition) The composition of two functions is associative, i.e.,
 forall A, B, C, D, f: A -> B, g: B -> C, h: C -> D: f o (g o h)=(f o g) o h

Proof  Take arbitrary A, B, C, D, f: A -> B, g: B -> C, and h: C -> D. We have to show
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: Author: Wolfgang Schreiner
Last Modification: October 4, 1999   