## Z Mathematical Tool-kit

Based on appendix D in The Way of Z.

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

Glossary

 - Empty set: a set that has no elements x S - Non-membership: x is not an element of S S T - Subset: all elements of S belong to T S T - Proper subset: S is a subset of T and S is not equal to T S T - Union: the set of elements in either S or T S T - Intersection: the set of elements in both S and T S \ T - Set difference: the set of elements in S that are not in T

Definitions

 [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,y x y - Maplet: x maps to y, same as (x,y) first p - First element of pair p second p - Second element of pair p id X - Identity relation X Y - Binary relation dom R - Domain: the set of first elements of all pairs in R ran R - Range: the set of second elements of all pairs in R

Definitions

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

 [X,Y] first: X Y X second: X Y Y _ _ : X Y X Y dom: (X Y) X ran: (X Y) Y x: X; y: Y; R: X Y first(x,y) = x second(x,y) = y x y = (x,y) dom R = {  x: X; y: Y | x R y x  } ran R = {  x: X; y: Y | x R y y  }

#### Pairs and binary relations II

Glossary

 S R - Domain restriction: the pairs in R whose first element is in S R T - Range restriction: the pairs in R whose second element is in T S R - Domain antirestriction: the pairs in R whose first element is not in S R T - Range antirestriction: the pairs in R whose second element is not in T R ~ - Relational inverse: the pairs in R, but with first and second elements exchanged R S - Relational image: the second elements of pairs in R whose first element is in S. R Q - Overriding: all pairs in R or Q, except pairs in R whose first element is also in Q. R + - Transitive closure of R

Definitions

 [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 R y x y  } S R = {  x: X; y: Y | x S x R y x y  } R T = {  x: X; y: Y | x R y y T x y  } R T = {  x: X; y: Y | x R y y T x y  } 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 ... predicate for _ + omitted ...

#### Pairs and binary relations III

Glossary

 Q R - Relational composition: Q composed with R R Q - Backward relational composition, same as Q R

Definitions

 [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 Q y y R z 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 i up through j min S - Mininum: the smallest element in S, if any max 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 | ... S is 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 X are paired with a member of Y X Y - Total function: every member of X is paired with a member of Y X Y - Partial injection: some members of X are paired with different members of Y X Y - Total injection: every member of X is paired with a different member of Y X Y - Bijection: every member of X is paired with a different member of Y, covering all Y's

Definitions

 X Y == {  f: X Y | Each member of X appears no more than once.  } X Y == {  f: X Y | dom f = X  } X Y == {  f: X Y | Each member of X is paired with a different member of Y.  } X Y == (X Y) (X Y) X Y == ... definition omitted ...

#### Sequences

Glossary

 seq X - Sequence: the set of all sequences of X's seq1 X - Non-empty sequence: the set of all sequences of X's with at least one element iseq X - Injective sequence: the set of all sequences of X's where each element of X appears only once s t - Concatenation: sequence s with sequence t appended head s - Head: the first element of sequence s last s - Last: the last element of sequence s front s - Front: all but the last element of sequence s tail s - Tail: all but the first element of sequence s s in t - Segment relation: the sequence s appears in sequence t

Definitions

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

 [X] head, last : seq1 X X tail, front : seq1 X seq X _ _ : seq X seq X seq X _ in _ : seq X seq X s: seq1 X; u,v: seq X head(s) = s(1) last(s) = s(# s) u v = u {  i: dom v i + #u v(i)  } u in v ( s,t: seq X s u t = v) ... predicates for other operators omitted ...

#### Other Z pages

Z examples in web pages.

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