% synthesis-slides.tex (root is synthesis.tex)

% width of centered minipage to match zed indent
\newcommand{\minindent}{5.25in} 

\pagestyle{empty}

\begin{slide}{}
SYNTHESIS

Sets (functions, relations, \dots) 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.

\end{slide}

\begin{slide}{}
SET COMPREHENSION

Combine declaration, predicate, expression.

\[ \{~ declaration | predicate @ expression ~\} \] 
can be thought of this way

\[	\{~ source | filter @ pattern ~\} \]

The expression and predicate are optional.

\begin{zed} \nat == \{~ i: \num | i \geq 0 ~\} \end{zed}

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

If the expression is the {\em characteristic tuple}, it can be
omitted.

\begin{zed} line == \{~ x,y: \num | y = m*x+b ~\} \end{zed}
means the same as

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

\end{slide}

\begin{slide}{}
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,

\begin{zed} PRIME == \{ 2, 3, 5, 7, 11, 13, 17, \dots \} \end{zed}
Paraphrasing the English

\begin{zed}
	PRIME == \{~ n: \nat | n > 1 \land \\
\t2 			\lnot (\exists m: 2 \upto n-1 @ n \mod m = 0) ~\}
\end{zed}
Can't we do better? A prime is {\em not} a product of numbers larger
than 1.

\begin{zed}
	\nat_2 == \nat \setminus \{ 0, 1 \}
\also
	PRIME == \nat_2 \setminus \{~ n,m: \nat_2 @ n * m ~\}
\end{zed}
We can make specifications clearer by moving away from a literal
paraphrase of the English, and using set operators instead of negation and
quantification.

\end{slide}

\begin{slide}{}
LAMBDA EXPRESSION

{\em Lambda expressions} define functions.

\[ (\lambda declaration | predicate @ expression) \] 

\begin{zed} isqr == (\lambda i: \num @ i*i) \end{zed}
means the same as this set comprehension.

\begin{zed} isqr == \{~ i: \num @ i \mapsto i*i ~\} \end{zed}
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 \]
\end{slide}

\begin{slide}{}
RESTRICTED QUANTIFIERS

{\em Restricted quantifiers} abbreviate common predicates.

\begin{zed} \forall i: ns | odd(i) @ i \leq nmax \end{zed}
means

\begin{zed} \forall i: ns @ odd(i) \implies i \leq nmax \end{zed}
and

\begin{zed} \exists i: ns | odd(i) @ i \leq nmax \end{zed}
means 

\begin{zed} \exists i: ns @ odd(i) \land i \leq nmax \end{zed}
In general

\begin{zed}
\also
	(\forall d | p @ q) \iff (\forall d @ p \implies q)
\also
	(\exists d | p @ q) \iff (\exists d @ p \land q)
\end{zed}

\end{slide}

\begin{slide}{}
CONVENIENCES AND SHORTCUTS

{\em Local definitions} factor out common expressions.

\begin{zed}
	(\LET r == iroot(a) @ r*r \leq a < (r+1)*(r+1))
\end{zed}
means 
\begin{zed}
        iroot(a) * iroot(a) \leq a < \\
\t3			(iroot(a)+1) * (iroot(a)+1)
\end{zed}

{\em Conditional expressions} simplify two-way case analyses.

\def\abs({\vert}
\def\sba){\vert}

\begin{zed} \abs(x\sba) = \IF x \geq 0 \THEN x \ELSE -x \end{zed}
means
\begin{zed}
(x \geq 0 \land \abs(x\sba) = x) \lor (x < 0 \land \abs(x\sba) = -x)
\end{zed}

\end{slide}