### STRUCTURE

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)

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