Sets, Functions and Relations

Relations, Functions and Z

Bart Massey



  • Collections of things

  • Unordered

  • No duplicates

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

Z Set Constructor

    { variables | conditions @ element }


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

Awkward compared to casual math practice, but precise.


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


  • 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

Last modified: Monday, 18 January 2016, 10:07 PM