STRUCTURE

Based on chapter 9 in The Way of Z.

Links to more Z lectures.

This page looks best when this \power and this X are about the same size: \power X. See these viewing tips.

Objects from discrete mathematics can model data structures.

Tuples (records)

Relations (tables, linked data structures)

Functions (lookup tables, trees and lists)

Sequences (lists, arrays)

Mathematics also provides precise meanings for operators.

TUPLES

Tuples can resemble C structures or Pascal records.

Tuples are instances of Cartesian product types.

First declare types for each component.

[NAME]
ID == \nat
DEPT ::= admin | manufacturing | research

Define the Cartesian product type EMPLOYEE.

EMPLOYEE == ID \cross NAME \cross DEPT

Declare tuples which are instances of the type.

\begin{axdef}
Frank, Aki: EMPLOYEE
\where
Frank = (0019, frank, admin)
Aki = (7408, aki, research)
\end{axdef}

RELATIONS

Relations are sets of tuples. They can resemble tables or databases.

ID NAME DEPT
0019 Frank Admin
0308 Philip Research
7408 Aki Research
... ... ...

In Z this can be expressed

\begin{axdef}
Employee: \power EMPLOYEE
\where
Employee = {
(0019, frank, admin),
(0308, philip, research),
(7408, aki, research),
...
)
\end{axdef}

PAIRS

Pairs are tuples with just two components.

(aki, 4117)

The maplet arrow provides alternate syntax without parentheses.

aki \mapsto 4117

The projection operators first and second extract the components of a pair.

first(aki,4117) = aki
second(aki, 4117) = 4117

BINARY RELATIONS (1)

Binary relations are sets of pairs.

\power (NAME \cross PHONE)

or

NAME \rel PHONE

Binary relations can model lookup tables.

NAME PHONE
Aki 4019
Philip 4107
Doug 4107
Doug 4136
Philip 0113
Frank 0110
Frank 6190
... ...

BINARY RELATIONS (2)

In Z this can be expressed

\begin{axdef}
phone: NAME \rel PHONE
\where
phone = {
...
aki \mapsto 4019,
philip \mapsto 4107,
doug \mapsto 4107,
doug \mapsto 4136,
philip \mapsto 0113,
frank \mapsto 0110,
frank \mapsto 6190,
...
)
\end{axdef}

RELATIONAL CALCULUS (1)

The tool-kit provides many operators for binary relations.

Domain and range are the sets of first and second components, respectively.

dom phone = { ..., aki, philip, doug, frank, ... }
ran phone = { ..., 4019, 4107, 4136, 0113, ... }

Relational image can model table lookup.

phone \limg { doug, philip } \rimg = { 4107, 4136, 0113 }

RELATIONAL CALCULUS (2)

Restriction operators can model database queries.

Domain restriction selects pairs based on their first component.

{ doug, philip } \dres phone =
{ philip \mapsto 4107,
doug \mapsto 4107,
doug \mapsto 4136,
philip \mapsto 0113 )

Range restriction selects according to the second element.

phone \rres (4000 .. 4999) = {
...
aki \mapsto 4019,
philip \mapsto 4107,
doug \mapsto 4107,
doug \mapsto 4136,
...
)

RELATIONAL CALCULUS (3)

Overriding can model database updates.

phone \oplus { heather \mapsto 4026, aki \mapsto 4026 } = {
...
aki \mapsto 4026,
philip \mapsto 4107,
doug \mapsto 4107,
doug \mapsto 4136,
philip \mapsto 0113,
frank \mapsto 0110,
frank \mapsto 6190,
heather \mapsto 4026,
...
)

RELATIONAL CALCULUS (4)

Inverse reverses domain and range by exchanging the components of each pair.

phone ~ = {
...
4019 \mapsto aki,
4107 \mapsto philip,
4107 \mapsto doug,
4136 \mapsto doug,
0013 \mapsto philip,
0110 \mapsto frank,
6190 \mapsto frank,
...
)

RELATIONAL CALCULUS (5)

Composition merges two relations by combining pairs that share a matching component.

\begin{axdef}
dept: PHONE \rel DEPT
\where
dept = {
0000 \mapsto admin, ..., 0999 \mapsto admin,
4000 \mapsto research, ..., 4999 \mapsto research,
6000 \mapsto manufacturing, ...,
\end{axdef}

Composing the phone and dept relations:

phone \comp dept = {
...
aki \mapsto research,
philip \mapsto research,
doug \mapsto research,
philip \mapsto admin,
frank \mapsto admin,
frank \mapsto manufacturing,
...
)

FUNCTIONS

Functions are binary relations where each element in the domain appears just once. Each domain element is a unique key.

\begin{axdef}
phonef: NAME \pfun PHONE
\where
phonef = {
...
aki \mapsto 4019,
philip \mapsto 4107,
doug \mapsto 4107,
frank \mapsto 6190,
...
)
\end{axdef}

Function application is a special case of relational image. It associates a domain element with its unique range element.

phonef \limg { doug } \rimg = 4107
phonef (doug) = 4107
phonef doug = 4107

BINARY RELATIONS AND FUNCTIONS

X \rel Y     Binary relations: many-to-many
X \pfun Y     Partial functions: many-to-one
    Some function applications undefined
X \fun Y     Total functions:
    All function applications defined
X \pinj Y     Partial injections: one-to-one
    Inverse is also a function
X \inj Y     Total injections
X \bij Y     Bijections: cover entire range (onto)

All have type \power (X \cross Y)

LINKED DATA STRUCTURES

Binary relations can model linked data structures such as lists, graphs and trees.

Each arc can be modelled by a pair of nodes.

For example a tree can be modelled by its child function.

\begin{axdef}
child: NODE \pfun NODE
child = { a \mapsto b, a \mapsto c,
b \mapsto d, b \mapsto e,
c \mapsto f, c \mapsto g, c \mapsto h )
\end{axdef}

``Pointers'' are not necessary.

The transitive closure operator builds the descendent relation from the child relation.

descendent = child +
descendent = { a \mapsto b, a \mapsto c , a \mapsto d, a \mapsto e, ... }

SEQUENCES

Sequences can model arrays and lists.

DAYS ::= friday | monday | saturday | sunday
| thursday | tuesday | wednesday

\begin{axdef}
weekday: seq DAYS
\where
weekday = \langle monday, tuesday, wednesday,
thursday, friday \rangle
\end{axdef}

Sequence operators include head and concatentation, \cat.

head weekday = monday
week == \langle sunday \rangle \cat weekday \cat \langle saturday \rangle

Sequences are functions, and functions are sets.

weekday = { 1 \mapsto monday, 2 \mapsto tuesday, ... }
weekday 3 = wednesday
# week = 7

OPERATORS

Most operators are just functions with infix syntax. For example

2 + 3 = 5

is a function application that can also be written

(_ + _) (2,3) = 5

This function could be defined like any other.

\begin{axdef}
_ + _: \num \cross \num \fun \num
\where
...
\end{axdef}

In Z the familiar plus sign ``+'' is actually the name of a set.

(_ + _) = {  ..., (1,1) \mapsto 2, (1,2) \mapsto 3, ... }

OPERATOR SYMBOLS AND SYNTAX

Operator symbols are defined systematically.

X \dres R     Domain restriction
X \ndres R     Domain anti-restriction
R \rres Y     Range restriction
R \nrres Y     Range anti-restriction

Pictorial symbols and infix syntax remind us of operand order and make expressions easy to parse by eye.

{ doug, philip } \dres phone \rres (4000 .. 4999) =
{ philip \mapsto 4107,
doug \mapsto 4107,
doug \mapsto 4136 )

Compare to rres(dres(phone, (doug, philip)), upto(4000,4999)))

FORMAL DEFINITIONS

Z operators are defined by formulas.

\begin{gendef} [X,Y]

_ \dres _, _ \ndres _ : \power X \cross (X \rel Y) \fun X \rel Y
_ \rres _, _ \nrres _ : (X \rel Y) \cross \power Y \fun X \rel Y
_ ~ : (X \rel Y) \fun (Y \rel X)
_ \limg _ \rimg : (X \rel Y) \cross \power X \fun \power Y
_ \oplus _ : (X \rel Y) \cross (X \rel Y) \fun (X \rel Y)
\where
\forall x: X; y: Y; S: \power X; T: \power Y;
Q, R: X \rel Y @
S \dres R = {  x: X; y: Y | x \in S \land x R y  } \land
S \ndres R = {  x: X; y: Y | x \notin S \land x R  } \land
R \rres T = {  x: X; y: Y | x R y \land y \in T  } \land
R \nrres T = {  x: X; y: Y | x R y \land y \notin T  } \land
R ~ = {  x: X; y: Y | x R y @ y \mapsto x  } \land
R \limg S \rimg = {  x: X; y: Y | x \in S \land x R y @ y  } \land
Q \oplus R = ((dom R) \ndres Q) \cup R
\end{gendef}

Back to Z lectures.

Jonathan Jacky / University of Washington / Seattle, Washington / USA
E-mail: jon@u.washington.edu