\section{Appendix}

%\begin{definition}[Greatest element]
%A greatest element of a partially ordered set ($X,\leq$) is a $y$ $\in$
%$X$ such that
%\[ \forall \; x  \in \;X, \; x \; \leq y \]
%\end{definition}

%\begin{definition}[Maximal]
%A maximal element of a partially ordered set ($X,\leq$) is a $y$ $\in$
%$X$ such that for no $x$ in $X$ is $y \; \leq \; x$.
%\end{definition}


\begin{definition}[Directed set]
Let the set $X$ be partially ordered by R. A nonempty set $S$ is
directed iff:
\[ \forall x_1, x_2 \in S, \mbox{  }\exists x_3 \mbox{ } \in S \mbox{ such that }
x_1 \sqsubseteq x_3 \mbox{ and } x_2 \sqsubseteq x_3.
\]
\end{definition}

To give an analogy, directed sets are like
the Cauchy sequences in analysis.\\


%\noindent
%{\bf Example 1:} \{a, b, d\} of the previous example is directed.
%\\
\noindent
{\bf Example 1:} Given a set $X$, define $S$ to be the set of all finite subsets of X:
\[ S = \{ F \subseteq X: \mbox{  }\mid F\mid < \omega \}
\]
$S$ is partially ordered by subset inclusion and is directed: 
\begin{center}
$\forall F_1, F_2 \in S,\mbox{ } F_1 \cup F_2 \in S$  is an upper bound.
\end{center}

\begin{definition}[Chain]
For a partially ordered set $X$, a subset $S$ of $X$ is a chain iff $S$ is nonempty,
and $\forall x_1, \mbox{ }x_2 \in S, \mbox{ }x_1 \ap x_2 \mbox{ } or \mbox{ }x_2 \ap x_1$.
\end{definition}
Directed sets are more general than chains,
for example,
%Example 1 is not a chain because b and d are incomparable.  More significant,
in Example 2, if X is uncountable then no chain of elements
in $S$ has the same lub as S.

\begin{definition}
A partially ordered set $(X, R)$ is a complete partial order (cpo) iff:
\begin{enumerate}
\item
$\exists \bot \in X$ s.t. $\bot \ap X$.
\item
$\forall$ directed $S \subseteq X$, \mbox{ }$\bigsqcup S \in X$ exists.
\end{enumerate}
\end{definition}

Despite the technical distinction between chains and directed sets the
difference won't bother us. For example, $cpo_{chain}  = cpo_{dir}$, since if
every chain has a lub then every directed set has a lub.\\

\noindent
{\bf Example 1:} $(P(X), \subseteq)$ is a cpo:
\begin{enumerate}
\item
there exists the least element $\bot = \emptyset$;
\item
$\forall$ directed $S \subseteq P(X)$, \mbox{  }$\bigsqcup S = \bigcup S \in P(X)$.
\end{enumerate}
\noindent
{\bf Example 2:} $(N_{\bot}, \ap)$ is a cpo with $\bot \ap N$.
\begin{verbatim}

                0  1  2  3   ...   n ...


                          _
\end{verbatim}
\noindent
N.B. \hspace{1em} $N_{\bot}$ captures the intuition that a program 
running forever ($\bot$) is
less defined than a program converging to some result.

\begin{definition}
A function $f: X \rightarrow Y$, where $X$ and $Y$ are partially ordered sets,
is monotone iff $\forall c_1, c_2 \in X, \mbox{ }c_1 \ap_X c_2 \Longrightarrow 
f(c_1) \ap_Y f(c_2)$.
 The function $f$ is continuous iff $f$ is monotone and $\forall$ directed
$S \subseteq X, \mbox{ }f(\bigsqcup S) = \bigsqcup \{f(x): x \in S\}$.
\end{definition}

Note monotone functions need not be continuous, e.g., let $A = \{0,1,..\} \mbox{ }\cup
\{\omega, \omega + 1\}$ and $f: A \rightarrow A$ where $f(n) = n\mbox{ } \forall
n \in N,\mbox{ } f(\omega) = f(\omega+1)=\omega+1$.
$f$  not continuous can be seen from the fact that it does not commute with
taking the limit:
\[ f(\bigsqcup S) = f(\omega) = \omega + 1 \neq \omega =
\bigsqcup S = \bigsqcup f(S) \]

We denote the set of all continuous functions from $X$ to $Y$ by 
$X \rightarrow_c Y$, and the set of all monotone functions
by $X \rightarrow_m Y$.


\begin{lemma}
If $X, Y$ are cpo's, then so are $X \rightarrow_c Y$, $X \rightarrow_m Y$
with the order $f \ap g$ iff $\forall x \in X, \mbox{ }f(x) \ap g(x)$.
\end{lemma}
\begin{proof}
\begin{itemize}
\item
$\ap$ is a partial order.
\item
There is a least element defined as: 
\[\bot_{X \rightarrow_m Y}(x) = \bot_Y \]
i.e., $\bot_{X \rightarrow_m Y}$ is everywhere less than or equal to every function:
\[\forall x \in X, \mbox{  }z \in X \rightarrow_m Y, 
\mbox{  }\bot_{X \rightarrow_m Y} (x) = \bot_Y \ap g(x) \]
\item
Let $F \subseteq (X\rightarrow_m Y)$
be a directed set. Define the function $g$ by
\[g(x) = \bigsqcup \{f(x) : f \in F\} \]
Since $F$ is a directed set :
\[\forall f_1,f_2  \;\; \exists f_3 \in F \; s.t.\; f_1 \ap f_3 \mbox{ and } 
f_2 \ap f_3 \]
This implies:
\[ \forall x \in X \mbox{  }f_1(x) \ap f_3(x) \mbox{  and  } f_2(x) \ap f_3(x)\]
We conclude that $\{f(x) : f \in F\}$ forms a directed set for each $x$.
Thus, it has a lub, so $g(x)$ is well defined and clearly $g$ is a upper bound
of $F$:
\[\forall f_i \in F, \mbox{  }\forall x \in X \mbox{  }f_i (x) \ap g(x) \Longrightarrow F \ap g \]
Moreover, it is the least upper bound, for if there was a smaller upper bound,
there would exist some $x$ such
that $g(x)$ were not the lub of the $\{f(x): f \in F\}$. 
\item
we have to prove now that $g$ is monotone.
Suppose $x \ap x'$, then by monotonicity of $f$:
\[\forall f \in F, \mbox{   }f(x) \ap f(x') \]
and this implies:
\[ \bigsqcup \{f(x): f \in F\} \ap \bigsqcup \{f(x'): f \in F\} \]
Thus: 
\[ g(x) = \bigsqcup \{f(x) \} \ap \bigsqcup \{f(x') \} = g(x').\]
\end{itemize}
\end{proof}

We have thus shown that a set of monotone functions is a cpo.
We state without proof that $X \rightarrow_c Y$ is also a cpo.\\


\begin{theorem}[Tarski-Knaster]
Let $X$ be a cpo and let $f: 
X \rightarrow_m X$. Then $f$ has a least fixed point.
\end{theorem}
\begin{proof}

Define the sequence of values:
\begin{center}
\begin{tabular}{l}
 $x_0 = \bot$\\
$x_\alpha = \bigsqcup\{ f(x_\beta) : \beta < \alpha\}$
\end{tabular}
\end{center}
where $\alpha$ range over the ordinals.

For any ordinal $\alpha$ by transfinite induction we have 
$x_\alpha \ap f(x_\alpha)$.
This implies :
\[\forall \beta \leq \alpha, \mbox{  }x_{\beta} \ap x_{\alpha}\]
So, $\{f(x_\beta) : \beta < \alpha\}$ is a directed set in $X$. 
Consider the directed set $x_0, x_1, \ldots x_\kappa$,
such that $\kappa > \mid X \mid$.
By pigeonholing there must exist $\kappa_1, \kappa_2$ s.t. $\kappa_1 < \kappa_2
\leq \kappa$,
and $x_{\kappa_{1}} = x_{\kappa_{2}}$.
But:
\[ f(x_{\kappa_{1}}) \ap x_{\kappa_{2}} \Longrightarrow
f(x_{\kappa_{1}}) \ap x_{\kappa_{1}}\]\
Moreover we know $x_{\kappa_{1}} \ap f(x_{\kappa_{1}})$, 
it follows that $f(x_{\kappa_{1}}) = x_{\kappa_{1}}$,
hence $x_{\kappa_{1}}$ is a fixed point of $f$.

To see that $x_{\kappa_{1}}$ is the least fixed point, suppose $y$
is a fixed point of $f$. By monotonicity of $f$:
\begin{center}
\begin{tabular}{l}
$\bot \ap y$ \\
$f(\bot) \ap f(y) = y$ \\
$f^{2}(\bot) \ap f^{2}(y)=y $\\
$\vdots$ \\
\end{tabular}
\end{center}
by induction:
\[x_{\kappa_{1}} \ap y.\]
\end{proof}

\begin{lemma}
$\mu : (X \rightarrow X) \rightarrow X$ is monotone.
\end{lemma}
\begin{proof}
Suppose $f \ap g$.  By monotonicity:
\[ x^f_{0} \ap x^g_{0}\] 
\[ x^f_{1} \ap x^g_{1}\] 
\[\vdots\]
by induction:
\[\mu f \ap \mu g\]
\end{proof}



\section*{Notation}
$\begin{array}{ll}
\reduces{}{}_R & \mbox{reduction relation induced by R}\\
\reduces{}{+} & \mbox{1 or more steps reduction}\\
\reduces{}{n} & \mbox{n steps reduction}\\
\reduce{}{\alpha} & \mbox{reduction of the $\alpha$-redex}\\
\alpha \subseteq t & \mbox{$\alpha$ is a subterm of t}
\end{array}$

\tableofcontents

\end{document}























We want to introduce the reader to a principle
similar to mathematical induction  called {\em noetherian induction}
\footnote{Noetherian is the same term than Strongly 
Normalizable ({\em SN}). A reduction system is said to be SN
if all reduction paths for every term are of finite length.}
or transfinite induction.

%*  try to write the diagraam og no-diamond
%$$\begin{diagram}
%& & & &
%(_{\alpha} (\lambda\; x.x \; x)(_{\beta} I \;I))
%& & & &  \\ 
%& \SW_{\alpha}  & & & &  & & \SE_{\beta}  &  \\
%(_{\beta_0} I I)(_{\beta_1} I I)
%& & & & & & & & & (_{\alpha} (\lambda\; x.x\;x)I) \\ 
%& \SE_{\beta_0} & & & &  & & \SW_{_\alpha} & \\ 
%& & I (_{\beta_1} I I )
%& & & & & & \\
%& & & \SE_{\beta_1} & &  & & &   \\
%& & & & I & & & &  \\
%\end{diagram}$$
