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

• 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 Boolean

• But 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 write

true /\ 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 relation

• The domain and range of a relation are the LHS and RHS sets that actually occur in a relation

• In 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 C

• That 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 C

• That 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