Go backward to 3.3 Predicates as SetsGo up to 3 Sets, Relations, and FunctionsGo 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

fis a function : <=>fis a binary relation /\forallx,y_{0},y_{1}: (<x,y_{0}> inf/\ <x,y_{1}> inf) =>y_{0}=y_{1}.

A

f:A->^{partial}B: <=>fis a function /\fsubsetAxB.

f:A->B: <=>f:A->^{partial}B/\forallxinA:existsyinB: <x,y> inf.

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

maps a tuple <f:AxB->C

**0**;- {<0, 0>, <1, 0>, <2, 1>, <3, 2>};
- {<
`x`,`x`^2>:`x`in**N**}; - {<
`x`,`x`^{2}>:`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**}.

- {<0, 0>, <0, 1>};
- {<
`x`,`x`^{2}>:`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.

f(x) :=suchyin range(f): <x,y> inf.

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

with the understanding thatforally:existsf:forallx:f(x)=y

forally:existsf:forallx: <x,y> inf.

Instead of writing `f`(<`x`_{0}, ...,
`x`_{n-1}>), we usually simply write `f`(`x`_{0},
..., `x`_{n-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/\forallxinA:f(x) =T

f= {<x,T>:xinA} /\forallxinA:TinB.

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

to denote

f:A_{0}x ... xA_{n-1}->Bf(x_{0}, ...,x_{n-1}) :=T

f:A_{0}x ... xA_{n-1}->Bf(t) :=letx_{0}=t_{0}, ...,x_{n-1}=t_{n-1}:T.

should be read as

div: NxN->Qdiv( x,y) :=x/y;

div := {<< x,y>,x/y>:xinN,yinN} /\forallxinN,yinN: div(x,y) inQ.

**Function Inversion**
While the inverse of a function is well defined, it is not necessarily a
function.

is a binary relation but not a function, because it contains <0, 0> and <0, 1>.f^{-1}= {<0, 0>, <0, 1>, <1, 2>}

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.

fog:A->C.

(1) ( fog):A->^{partial}C;(2) forallxinA:existsyinC: <x,y> in (fog).

- We prove (1), i.e., by definition of ->
^{partial}, that

We know (3) from the definition of o ; we still have to show (4). Take arbitrary(3) ( `f`o`g`) subset`A`×`C`;(4) **forall**x,`y`_{0},`y`_{1}: (<`x`,`y`_{0}> in (`f`o`g`) /\ <`x`,`y`_{1}> in (`f`o`g`)) =>`y`_{0}=`y`_{1}.`x`,`y`_{0},`y`_{1}and assume

We have to show(5) < `x`,`y`_{0}> in (`f`o`g`);(6) < `x`,`y`_{1}> in (`f`o`g`).`y`_{0}=`y`_{1}.From (5), (6), and the definition of o , we know

`y`_{0}in`C`,`y`_{1}in`C`, and

By (7), we have some(7) **exists**`b`in`B`: <`x`,`b`> in`f`/\ <`b`,`y`_{0}> in`g`;(8) **exists**`b`in`B`: <`x`,`b`> in`f`/\ <`b`,`y`_{1}> in`g`.`b`_{0}in`B`such that <`x`,`b`_{0}> in`f`/\ <`b`_{0},`y`_{0}> in`g`; by (8), we have some`b`_{1}in`B`such that <`x`,`b`_{1}> in`f`/\ <`b`_{1},`y`_{0}> in`g`. From <`x`,`b`_{0}> in`f`, <`x`,`b`_{1}> in`f`and the fact that`f`is a function, we know that`b`_{0}=`b`_{1}. From this and from <`b`_{0},`y`_{0}> in`g`, <`b`_{1},`y`_{1}> in`g`, and the fact that`g`is a function, we know that`y`_{0}=`y`_{1}. - We prove (2). Take arbitrary (3)
`x`in`A`. We have to show(4)

From (3) and**exists**`y`in`C`: <`x`,`y`> in (`f`o`g`).`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)(12) `x`in`A`/\`y`in`C`;(13) **exists**`b`: <`x`,`b`> in`f`/\ <`b`,`y`> in`g`.`b`:=`f`(`x`) and have to show:

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.

forallxin A: (fog)(x) =g(f(x)).

We then have the following result:

forallA,B,C,D,f:A->B,g:B->C,h:C->D:fo (goh)=(fog) oh

Take arbitraryforallxinA: (fo (goh))(x) = ((fog) oh)(x).

( fo (goh))(x)= ( goh)(f(x))= h(g(f(x)))= h((fog)(x))= (( fog) oh)(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

says that

Author: Wolfgang Schreiner

Last Modification: October 4, 1999