SYNTHESIS

Based on chapter 10 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.


Sets (functions, relations, ...) and logic are all we need to write small formal descriptions.

Well-chosen notational conventions can make mathematical texts easier to read.

Formal descriptions are not just paraphrased natural language. Writing useful formal descriptions requires design judgment.


SET COMPREHENSION

Combine declaration, predicate, expression.

{  declaration | predicate @ expression  }

can be thought of this way

{  source | filter @ pattern  }

The expression and predicate are optional.

\nat == {  i: \num | i \geq 0  }

ODD == { i: \num @ 2*i+1 }

If the expression is the characteristic tuple, it can be omitted.

line == {  x,y: \num | y = m*x+b  }

means the same as

line == {  x,y: \num | y = m*x+b @ (x,y)  }

SPECIFICATIONS

Set comprehensions are specifications in miniature.

A prime number is an integer larger than 1 that is only divisible by itself and 1. Informally,

PRIME == { 2, 3, 5, 7, 11, 13, 17, ... }

Paraphrasing the English

PRIME == {  n: \nat | n > 1 \land \lnot (\exists m: 2 .. n-1 @ n mod m = 0)  }

Can't we do better? A prime is not a product of numbers larger than 1.

\nat2 == \nat \ { 0, 1 }
PRIME == \nat2 \ {  n,m: \nat2 @ n * m  }

We can make specifications clearer by moving away from a literal paraphrase of the English, and using set operators instead of negation and quantification.


LAMBDA EXPRESSION

Lambda expressions define functions.

(\lambda declaration | predicate @ expression)

isqr == (\lambda i: \num @ i*i)

means the same as this set comprehension.

isqr == {  i: \num @ i \mapsto i*i  }

Both mean the same as

\begin{axdef}
isqr: \num \fun \nat
\where
\forall i: \num @ isqr i = i*i
\end{axdef}

Lambda expressions enable us to use functions without writing declarations.

9 = (\lambda i: \num @ i*i) 3

RESTRICTED QUANTIFIERS

Restricted quantifiers abbreviate common predicates.

\forall i: ns | odd(i) @ i \leq nmax

means

\forall i: ns @ odd(i) \implies i \leq nmax

and

\exists i: ns | odd(i) @ i \leq nmax

means

\exists i: ns @ odd(i) \land i \leq nmax

In general

(\forall d | p @ q) \iff (\forall d @ p \implies q)
(\exists d | p @ q) \iff (\exists d @ p \land q)

CONVENIENCES AND SHORTCUTS

Local definitions factor out common expressions.

(let r == iroot(a) @ r*r \leq a < (r+1)*(r+1))

means

iroot(a) * iroot(a) \leq a < (iroot(a)+1) * (iroot(a)+1)

Conditional expressions simplify two-way case analyses.

| x | = if x \geq 0 then x else -x

means

(x \geq 0 \land| x | = x) \lor (x < 0 \land | x | = -x)

Back to Z lectures.


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