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