## Sets, Functions and Relations

# Relations, Functions and Z

Bart Massey

# Sets

Review:

Collections of things

Unordered

No duplicates

Can be typed (= all members of same superset = sorted)

# Z Set Constructor

```
{ variables | conditions @ element }
```

e.g.

```
{ z in Z | z mod 2 = 0 @ z }
```

Awkward compared to casual math practice, but precise.

# Tuples

Specifically pairs:

Match up two things

Can be built form sets with funny constructions, e.g.

`(a, b) == {{1, a}, {2, b}}`

But usually treated as primitive.

Z notations:

`(a, b) a |-> b`

Often left and right have different type

# More About Tuples

Tuple projection

Cartesian Product

`A x B = {a in A, b in B @ (a, b)}`

Cartesian Product usually used as a tuple type

`f : N x N -> N`

f (a, b) = a + b

# Relations

A relation is just a set of tuples of a given Cartesian Product type.

E.g.

`{(3, 2), (3, 4), (2, 5), (3, 5)}`

"Relates" the thing on the left to the thing on the right.

E.g.

`<=`

`(<=) = {... (1,1), (1,2) ... (2, 3) ... (2, 99) ...}`

A relation exists ("holds") between two values if their tuple is part of the relation's set of tuples.

We write

`x R y`

as equivalent to`(x, y) in R`

# Relations Aren't Booleans

Note that in programming we think of

`<=`

as being a sort of function that takes two numeric arguments and returns a BooleanBut this is not what's going on here. We don't even have any Boolean type yet

The

*theory of Z*says that a relational expression is true or false inasmuch as the tuple is or isn't in the relation.But the Booleans are stuck in the theory, and don't escape into the language we are allowed to use right now. We

*must not*writetrue /\ a < b

# Domain and Range Of A Relation

The

*formal domain*and*formal range*of a relation are the sets that are declared for the LHS and RHS of the relationThe

*domain*and*range*of a relation are the LHS and RHS sets that actually occur in a relationIn Z we use the

`dom R`

and`ran R`

functions to get these sets

# Relational Image

Note that the same LHS can occur multiple times in a general relation, so the function notion of "apply a function to an argument yielding a result" doesn't quite work.

The Z Relational Image operator lets us collect

*the set of results*we get by applying a relation to a given*set of arguments*`R subset A x B`

R (| {a1, a2} |) = { b in B | (a1, b) in R \/ (a2, b) in R @ b }

# Domain and Range Restriction

Peculiar to Z: allow limiting the domain or range of a relation to a particular set ("restricting" the relation).

`{x} <| R = { (x, b) in R @ (x, b) } R |> = { (x, b) in R @ (x, b) }`

Also antirestriction operators that restrict the relation to things

*outside*the set.Consider relational image:

R (| S |) = ran (S <| R)

# Relational Override

Peculiar to Z: makes a new relation by replacing elements in a relation:

`R (+) R' = (dom R' <~| R) union R'`

"Keeps R except where R' holds"

# Properties Of Relations

A relation is

*reflexive*if every pair with identical LHS and RHS appears in it, i.e.`(dom R x dom R) subset R`

A relation is

*commutative*if every pair in R also occurs reversed, i.e.`a R b iff b R a`

A relation is

*transitive*if it is "ordered", i.e.x R y and y R z => x R z

# Functions Are Relations

We say a relation is a

*function*if each element in the domain appears on the left in exactly one tuple.A function is a

*total function*if every element in the formal domain of the function is in its domain. A function is a*partial function*otherwise.e.g.

`isqrt : N -> N`

is total`isqrt : Z -|-> Z`

is partial`isqrt : C -> C`

is total (but no C in Standard Z)

# Properties Of Functions

A function is

*surjective*(*"onto"*) if its formal range is the same as its range: that is, for every element in the formal range there is a tuple with that RHS.A function is

*injective*(*"invertible"*) if every element in its range is the RHS of exactly one tuple. In Z, we write the inverse of a relation as`~`

, and in general the inverse of a relation is another relation: for an injective function, the inverse relation is also a function.A function is

*bijective*(*"total invertible"*) if it is total and injective and surjective. If the formal domain and formal range are the same set, then such a function is a*permutation*function.

# Higher-Order Functions: Curried

We can think of

`f : A -> B -> C`

as a relation from elements of A to relations from B to CThat is:

`f subset A x (B x C)`

So

`(+) : N -> N -> N`

has elements in it like(2, (3, 5)) (2, (7, 9))

# Tupled Functions

We can think of

`f : A x B -> C`

as a relation from (relations of A to B) to CThat is:

`f subset (A x B) x C`

So

`(+) : (N x N) -> N`

has elements in it like`((2, 3), 5)) ((2, 7), 9))`

This is the default Z view of standard functions