previous up next
Go backward to 3.3 Predicates as Sets
Go up to 3 Sets, Relations, and Functions
Go forward to 3.5 Sequences and Matrices
RISC-Linz logo

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: (<x, y0> in f /\  <x, y1> 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: <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 -> 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: The following are not functions:

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):

All of this is to be interpreted as
f: A -> B /\  forall x in A: f(x) = T
or, equivalently, as
f = {<x, T>: 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/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: <x, y> in (f o g).

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

previous up next