Based on chapter 9 in The Way of Z.

Links to more Z lectures.

This page looks best when this ` and this ``X` are
about the same size: ` 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 == |

DEPT ::= admin | manufacturing | research |

Define the Cartesian product type `EMPLOYEE`.

EMPLOYEE == ID NAME DEPT |

Declare tuples which are instances of the type.

Frank, Aki: EMPLOYEE | ||

Frank = (0019, frank, admin) | ||

Aki = (7408, aki, research) | ||

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

Employee: EMPLOYEE | ||

Employee = { | ||

(0019, frank, admin), | ||

(0308, philip, research), | ||

(7408, aki, research), | ||

... | ||

) | ||

PAIRS

*Pairs* are tuples with just two components.

(aki, 4117) |

The *maplet* arrow provides alternate syntax without
parentheses.

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

(NAME PHONE) |

or

NAME 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

phone: NAME PHONE | ||

phone = { | ||

... | ||

aki 4019, | ||

philip 4107, | ||

doug 4107, | ||

doug 4136, | ||

philip 0113, | ||

frank 0110, | ||

frank 6190, | ||

... | ||

) | ||

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 { doug, philip } = { 4107, 4136, 0113 } |

RELATIONAL CALCULUS (2)

*Restriction operators* can model database queries.

*Domain restriction* selects pairs based on their first component.

{ doug, philip } phone = |

{ philip 4107, |

doug 4107, |

doug 4136, |

philip 0113 ) |

*Range restriction* selects according to the second element.

phone (4000 .. 4999) = { |

... |

aki 4019, |

philip 4107, |

doug 4107, |

doug 4136, |

... |

) |

RELATIONAL CALCULUS (3)

*Overriding* can model database updates.

phone { heather 4026, aki 4026 } = { |

... |

aki 4026, |

philip 4107, |

doug 4107, |

doug 4136, |

philip 0113, |

frank 0110, |

frank 6190, |

heather 4026, |

... |

) |

RELATIONAL CALCULUS (4)

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

phone ^{~} = { |

... |

4019 aki, |

4107 philip, |

4107 doug, |

4136 doug, |

0013 philip, |

0110 frank, |

6190 frank, |

... |

) |

RELATIONAL CALCULUS (5)

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

dept: PHONE DEPT | ||

dept = { | ||

0000 admin, ..., 0999 admin, | ||

4000 research, ..., 4999 research, | ||

6000 manufacturing, ..., | ||

Composing the `phone` and `dept` relations:

phone dept = { |

... |

aki research, |

philip research, |

doug research, |

philip admin, |

frank admin, |

frank manufacturing, |

... |

) |

FUNCTIONS

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

phonef: NAME PHONE | ||

phonef = { | ||

... | ||

aki 4019, | ||

philip 4107, | ||

doug 4107, | ||

frank 6190, | ||

... | ||

) | ||

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

phonef { doug } = 4107 |

phonef (doug) = 4107 |

phonef doug = 4107 |

BINARY RELATIONS AND FUNCTIONS

X Y | Binary relations: many-to-many |

X Y | Partial functions: many-to-one |

Some function applications undefined | |

X Y | Total functions: |

All function applications defined | |

X Y | Partial injections: one-to-one |

Inverse is also a function | |

X Y | Total injections |

X Y | Bijections: cover entire range (onto) |

All have type ` (X 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.

child: NODE NODE | ||

child = { a b, a c, | ||

b d, b e, | ||

c f, c g, c h ) | ||

``Pointers'' are not necessary.

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

descendent = child ^{+} |

descendent = { a b, a c , a d, a e, ... } |

SEQUENCES

*Sequences* can model *arrays* and *lists*.

DAYS ::= friday | monday | saturday | sunday |

| thursday | tuesday | wednesday |

weekday: seq DAYS | ||

weekday = monday, tuesday, wednesday, | ||

thursday, friday | ||

Sequence operators include *head* and
*concatentation*, `.
`

head weekday = monday |

week == sunday weekday saturday |

Sequences are functions, and functions are sets.

weekday = { 1 monday, 2 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.

_ + _: | ||

... | ||

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

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

OPERATOR SYMBOLS AND SYNTAX

Operator symbols are defined systematically.

X R | Domain restriction |

X R | Domain anti-restriction |

R Y | Range restriction |

R Y | Range anti-restriction |

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

{ doug, philip } phone (4000 .. 4999) = |

{ philip 4107, |

doug 4107, |

doug 4136 ) |

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

FORMAL DEFINITIONS

Z operators are defined by formulas.

[X,Y] | |||

_ _, _ _ : X (X Y) X Y | |||

_ _, _ _ : (X Y) Y X Y | |||

_ ^{~} : (X Y) (Y X) | |||

_ _ : (X Y) X Y | |||

_ _ : (X Y) (X Y) (X Y) | |||

x: X; y: Y; S: X; T: Y; | |||

Q, R: X Y | |||

S R = { x: X; y: Y | x S x R y } | |||

S R = { x: X; y: Y | x S x R } | |||

R T = { x: X; y: Y | x R y y T } | |||

R T = { x: X; y: Y | x R y y T } | |||

R ^{~} = { x: X; y: Y | x R y y x } | |||

R S = { x: X; y: Y | x S x R y y } | |||

Q R = ((dom R) Q) R | |||

Back to Z lectures.

Jonathan Jacky / University of Washington / Seattle, Washington / USA

E-mail: jon@u.washington.edu