Based on appendix D in The Way of Z.

Links to more Z examples.

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

The Z mathematical tool-kit is a collection of types and operators somewhat like a standard library of types and functions in a programming language.

The definitions in the tool-kit build up all the Z operators from a few fundamental constructs in logic and set theory.

The tool-kit uses generic definitions very heavily: `X`, `Y`, and `Z`
stand for any type, `S` and `T` are sets of any type, and `Q` and `R`
are binary relations between any two types. The toolkit also makes
extensive use of patterns in abbreviation definitions, for example it
defines the binary relation symbol ` by ``X Y == (X Y)`.

In a few places I've used English paraphrases for predicates, where the formal definition uses constructs or concepts not defined here.

These selections from the tool-kit are based on the Reference Manual, which defines additional types and operators.

Sets

Pairs and binary relations I

Pairs and binary relations II

Pairs and binary relations III

Numbers and arithmetic

Functions

Sequences

## Sets

Glossary

- Empty set: a set that has no elements x S- Non-membership: xis not an element ofSS T- Subset: all elements of Sbelong toTS T- Proper subset: Sis a subset ofTandSis not equal toTS T- Union: the set of elements in either SorTS T- Intersection: the set of elements in both SandTS \ T- Set difference: the set of elements in Sthat are not inTDefinitions

[X] == { x: X | false }

[X] _ _ : X X _ _, _ _ : X X _ _ , _ _, _ \ _: X X X x: X; S, T: X x S (x X) (S T ( x: X x S x T)) (S T S T S T) S T = { x: X | x S X T } S T = { x: X | x S X T } S \ T = { x: X | x S X T }

## Pairs and binary relations I

Glossary

(x,y)- The pair x,yx y- Maplet: xmaps toy, same as(x,y)first p- First element of pair psecond p- Second element of pair pidX- Identity relation X Y- Binary relation domR- Domain: the set of first elements of all pairs in RranR- Range: the set of second elements of all pairs in RDefinitions

X Y == (X Y) idX == { x: X x x }

[X,Y] first: X Y X second: X Y Y _ _ : X Y X Y dom: (X Y) Xran: (X Y) Yx: X; y: Y; R: X Y first(x,y) = x second(x,y) = y x y = (x,y) domR = { x: X; y: Y | xRy x }ranR = { x: X; y: Y | xRy y }

## Pairs and binary relations II

Glossary

S R- Domain restriction: the pairs in Rwhose first element is inSR T- Range restriction: the pairs in Rwhose second element is inTS R- Domain antirestriction: the pairs in Rwhose first element is not inSR T- Range antirestriction: the pairs in Rwhose second element is not inTR^{~}- Relational inverse: the pairs in R,but with first and second elements exchanged R S- Relational image: the second elements of pairs in Rwhose first element is inS.R Q- Overriding: all pairs in RorQ,except pairs in Rwhose first element is also inQ.R^{+}- Transitive closure of RDefinitions

[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) (X X)x: X; y: Y; S: X; T: Y; Q, R: X Y S R = { x: X; y: Y | x S x Ry x y }S R = { x: X; y: Y | x S x Ry x y }R T = { x: X; y: Y | x Ry y T x y }R T = { x: X; y: Y | x Ry y T x y }R ^{~}= { x: X; y: Y | xRy y x }R S = { x: X; y: Y | x S x Ry y }Q R = (( domR) Q) R... predicate for _omitted ...^{+}

## Pairs and binary relations III

Glossary

Q R- Relational composition: Qcomposed withRR Q- Backward relational composition, same as Q RDefinitions

[X,Y,Z] _ _ : (X Y) (Y Z) (X Z) _ _ : (Y Z) (X Y) (X Z) Q: X Y; R: Y Z Q R = R Q = { x: X; y: Y; z: Z | x Qy yRz x z }

## Numbers and arithmetic

Glossary

- The set of integers - The set of natural numbers, starting with zero _{1}- The set of strictly positive numbers, starting with one +,-,*- Arithmetic operators: addition, subtraction, multiplication div,mod- Arithmetic operators: integer division and remainder (modulus) <,- Comparison: less than, less than or equal >,- Comparison: greater than, greater than or equal i .. j- Number range: the set of numbers starting with iup throughjmin S- Mininum: the smallest element in S, if anymax S- Maximum: the largest element in S, if any# S- Size: the number of elements in S_{1}- Non-empty sets - Finite sets Definitions

[] == { n: | n 0 } _{1}== \ { 0 }_{1}X == { S: X | S }X == { S: X | ... Sis finite ... }

_ + _, _ - _, _* _ : _ div_, _mod_ : ( \ { 0 })_ - : _ < _, _ _, _ _, _ > _ : _ .. _ : #: X min, max: _{1}a,b: a .. b = { i: | a i b } ... predicates for other operators omitted ...

## Functions

Glossary

X Y- Partial function: some members of Xare paired with a member ofYX Y- Total function: every member of Xis paired with a member ofYX Y- Partial injection: some members of Xare paired with different members ofYX Y- Total injection: every member of Xis paired with a different member ofYX Y- Bijection: every member of Xis paired with a different member ofY,covering all Y'sDefinitions

X Y == { f: X Y | Each member of Xappears no more than once. }X Y == { f: X Y | domf = X }X Y == { f: X Y | Each member of Xis paired with a different member ofY. }X Y == (X Y) (X Y) X Y == ... definition omitted ...

## Sequences

Glossary

seq X- Sequence: the set of all sequences of X'sseq_{1}X- Non-empty sequence: the set of all sequences of X'swith at least one element iseq X- Injective sequence: the set of all sequences of X'swhere each element of Xappears only onces t- Concatenation: sequence swith sequencetappendedhead s- Head: the first element of sequence slast s- Last: the last element of sequence sfront s- Front: all but the last element of sequence stail s- Tail: all but the first element of sequence ssint- Segment relation: the sequence sappears in sequencetDefinitions

seq X == { f: X | domf = 1 .. # f }seq _{1}X == { f: seq X | # f > 0 }iseq X == seq X ( X)

[X] head, last : seq _{1}X Xtail, front : seq _{1}X seq X_ _ : seq X seq X seq X _ in_ : seq X seq Xs: seq _{1}X; u,v: seq Xhead(s) = s(1) last(s) = s(# s) u v = u { i: domv i + #u v(i) }u inv ( s,t: seq X s u t = v)... predicates for other operators omitted ...

Z examples in web pages.

**Z2HTML** tool for translating
LaTeX documents with Z markup to HTML web pages.

Z home page with FAQ and links to publications, tools, and meetings.

Back to top

Jonathan Jacky / Department of Radiation Oncology Box 356043

University of Washington / Seattle, Washington 98195-6043 / USA

Tel (206) 598-4117 / Fax (206) 598-6218

E-mail: jon@u.washington.edu