%
% 04-semantika-programov.tex
%
% Developed by Ondrej Jombik <nepto@platon.sk>
% Copyright (c) 2003-2005 Platon Group, http://platon.sk/
% Licensed under terms of GNU General Public License.
% All rights reserved.
%
% Changelog:
% 26/02/2003 - created
%

% $Platon: doc/ztp-zbierka/04-semantika-programov.tex,v 1.10 2007-08-06 04:56:50 nepto Exp $

\chapter{Sémantika programov}

\section{Základy sémantiky}

\begin{example} % /* loop(b, S_1, S_2)

Uvažujme hypotetický iteratívny príkaz~$\cmd{loop}~(b, S_1, S_2)$
definovaný sémantickou rovnicou

$$
\M\lb \cmd{loop}~(b, S_1, S_2) \rb ~=~ \UU\{\phi_i\}
$$

kde
$$
\begin{array}{rcc @{} c @{} l @{} l}
	\phi_0		& =	& \lambda\sigma	& ~\cdot~	& \perp	&	\\
	\phi_{i+1}	& =	& \lambda\sigma	& ~\cdot~	& \cmd{if}~ \W\lb b \rb\sigma
						& ~\cmd{then}~ \phi_i(\M\lb S_1 \rb\sigma)	\\
				&	&				&			&
						& ~\cmd{else}~ \M\lb S_2 \rb\sigma			\\
\end{array}
$$

Na základe základných príkazov (priradenie, kompozícia, vetvenie a cyklus)
definujte programový segment $S$ taký, že platí

$$
\M\lb \cmd{loop}~(b, S_1, S_2) \rb ~=~ \M\lb S \rb
$$

Tvrdenie dokážte.


\end{example} % */

\begin{solution} % /*

Analýzou sémantickej rovnice v~zadaní vieme vytvoriť programový
segment~$S$ skladajúci sa z~častí $S_0$ a $S_2$.

% $$
% \begin{array}{ll}
% 	S:			&
% \left.\begin{array}{@{} l}
% \cmd{while}~ b ~\cmd{do}		\\
% ~~~~ S_1						\\
% \cmd{od}						\\
% \end{array}\right\} S_0			\\
% 				& S_2;			\\
% \end{array}
% $$
$$
\begin{array}{ll @{~} l}
	S:	& \cmd{while}~ b ~\cmd{do} &
	\multirow{3}{*}{$\left.\raisebox{4ex}{}\right\} S_0$} \\
		& ~~~~ S_1						\\
		& \cmd{od}						\\
		& S_2;			\\
\end{array}
$$

Teda pre programový subsegment~$S_0$ platí
$$
\M\lb \cmd{while}~ b ~\cmd{do}~ S_1 ~\cmd{od} \rb ~=~ \UU\{\psi_i\}
$$

kde
$$
\begin{array}{rcc @{} c @{} l @{} l}
	\psi_0		& =	& \lambda\sigma	& ~\cdot~	& \perp	&	\\
	\psi_{i+1}	& =	& \lambda\sigma	& ~\cdot~	& \cmd{if}~ \W\lb b \rb\sigma
						& ~\cmd{then}~ \psi_i(\M\lb S_1 \rb\sigma)	\\
				&	&				&			&
						& ~\cmd{else}~ \sigma								\\
\end{array}
$$

Keďže $\M\lb S_2 \rb\sigma^{'}$ potom pre programový
segment~$S$ platí

$$
\M\lb S_0; S_2 \rb\sigma ~=~ \lambda\sigma ~\cdot~
\M\lb S_2 \rb(\M\lb S_0 \rb\sigma)
$$

Našli sme teda programový segment~$S$. Teraz musíme dokázať ekvivalenciu
s~iteratívnym príkazom $\cmd{loop}~(b, S_1, S_2)$.

$$
\begin{array}{lcl}
\M\lb S \rb
	& =	& \lambda\sigma ~\cdot~ \M\lb S_2 \rb(\M\lb S_0 \rb\sigma)	\\
	& =	& \lambda\sigma ~\cdot~ \M\lb S_2 \rb(\M\lb \cmd{while}~ b ~\cmd{do}~ S_1 ~\cmd{od} \rb\sigma)	\\
	& = & \lambda\sigma ~\cdot~ \M\lb S_2 \rb(\UU\{\psi_i\}\sigma)			\\
\end{array}
$$

Čiže musíme dokázať nasledujúce tvrdenie.

$$
\M\lb S_2 \rb(\UU\{\psi_i\}) ~=~ \UU\{\phi_i\}
$$

Rovnosť rozložíme na dva možné prípady.

\begin{enumerate}
	\item Nech $\UU\{\phi_i\} = \perp$. To znamená, že $\forall \phi_i =
		\perp$. Potom $\M\lb S_2 \rb(\UU\{\psi_i\}) = \perp$. Kedy bude
		$\phi_i$~$\perp$? Ak $i=0$ alebo $\forall i>0: \W\lb b \rb\sigma
		= true$. Rovnako to platí aj pri~$\psi$. Takže $\M\lb S_2
		\rb\perp = \perp$.

	\item Nech $\UU\{\phi_i\} \ne \perp$. Potom $i\ne0$ resp. $i>0$.
		Určite $\exists k: k<i$ také, že $k$-krát bolo $\W\lb b
		\rb$~$true$ a na $k+1$ bolo $false$. Teda $\UU$ bola $\M\lb S_2
		\rb\sigma$.

		Pozrieme sa na~$\psi$. Vieme, že $k$-krát bude $true$, potom
		$false$. Vykonal sa teda rovnaký kód ako pri~$\phi$.
		$\UU\{\psi_i\}$ bola $\sigma$. Takže $\UU$ ľavej strany
		priradenia je~$\M\lb S_2 \rb\sigma$.
\end{enumerate}

\end{solution} % */

\section{Sémantika rekuzívnych programov}

\begin{definition} % /*
	Definujme množinu termov $E_{xp} = \{t, t_i, \dots\}$ resp. $B_{exp}
	= \{b, b_i, \dots\}$, ďalej $X \subseteq E_{xp}$, $F^0 \subseteq
	E_{xp}$, $B^0 \subseteq B_{exp}$.

	\begin{itemize}
		\item ak $f_F \in F^0, t_1 ... t_n \in E_{xp}$, potom $f_F(t_1
			... t_n) \in E_{xp}$
		\item ak $p \in B^n, t_1 ... t_n \in E_{xp}$, potom $p(t_1 ...
			t_n) \in B_{exp}$
		\item ak $b \in B_{exp}, t_1, t_2 \in E_{xp}$, potom $\cmd{if}~ b
			~\cmd{then}~ t_1 ~\cmd{else}~ t_2 ~\cmd{fi} \in E_{xp}$
		\item ak $\phi \in \Phi^n, t_1 ... t_n \in E_{xp}$, potom
			$\phi(t_1 ... t_n) \in E_{xp}$
	\end{itemize}
\end{definition} % */

\begin{definition} % /*
	Definujme syntax rekurzívnej definície:
	$$
	\phi(x_1 ... x_n) \Longleftarrow t[\phi](x_1 ... x_n)
	$$
\end{definition} % */

\begin{definition} % /*
	Definícia programu so systémom rekurzívnych definícií:
$$
\begin{array}{rcl}
	\phi_1(x) & \Longleftarrow & t_1[\phi_1 ... \phi_n](\overline{x})\\
	\phi_2(x) & \Longleftarrow & t_2[\phi_1 ... \phi_n](\overline{x})\\
	& \dots & \\
	\phi_n(x) & \Longleftarrow & t_n[\phi_1 ... \phi_n](\overline{x})
\end{array}
$$

\end{definition} % */

\begin{veta}[Kleene] % /*
	Každý spojitý funkcionál $\tau$ má jediný najmenší pevný bod
	$$
	f_\tau = \sqcup_0^\infty \tau^i[\Omega]
	$$
	kde $\tau^0[\Omega] = \Omega$ a taktiež $\tau^{i+1}[\Omega] =
	\tau[\tau^i[\Omega]]$.

\end{veta} % */

\begin{dosledok} % /*

Kleeneho veta nám teda dáva návod ako nájsť riešenie rekurzívnej
rovnice resp. pevný bod rekurzívneho programu.

Konštrukcia riešenia je nasledovná:
\begin{enumerate}
	\item zadefinujeme postupnosť aproximácií $\tau^i[\Omega]$ pre
		všetky $i \ge 0$
	\item zostrojíme najmenšiu hornú hranicu reťazca $\sqcup_0^\infty
		\tau^i[\Omega]$
\end{enumerate}
\end{dosledok} % */

%%%\begin{example} % /*
%%%	Ako nájsť pevný bod nejakého funkcionálu?
%%%\end{example} % */
%%%
%%%\begin{solution} % /*
%%%	Pevný bod funkcionálu nájdeme vykonaním nasledujúcich krokov:
%%%	\begin{enumerate}
%%%		\item Použijeme krok výpočtu a zjednodušovanie:
%%%			\begin{enumerate}
%%%				\item Z funkcionálu $\phi_1$ dostaneme funkcionál $\phi_2$ a
%%%					platí $\phi_1 = \phi_2$.
%%%				\item 
%%%					Pri zjednodušovaní používame špeciálne pravidlo,
%%%					pomockou ktorého sa dostaneme bližšie k riešeniu.
%%%
%%%					Musíme používať korektné pravidlo, ktorým máme
%%%					garanatované, že nech ho použijeme ako chceme, vždy
%%%					dospejeme k~správnemu riešeniu. Je teda jedno ktorý
%%%					podterm zasubstituujeme.
%%%
%%%					Preto budeme používať pravidlo {\it Full
%%%					substitution (FS)}. To znamená, že urobíme
%%%					substitúciu pre každý výskyt rekurzívneho
%%%					funkcionálu.
%%%				\end{enumerate}
%%%		\item Použijeme Kleeneho vetu.
%%%	\end{enumerate}
%%%\end{solution} % */

\begin{example} % /*
	Majme program:
$$
\begin{array}{l}
	\cmd{int}~ f(\cmd{int}~ x)\\
	\{\\
	~~~~~~\cmd{if}~ (x == 0) ~\cmd{then}~\cmd{return}~ 0;\\
	~~~~~~\cmd{else}~\cmd{return}~ x + f(x - 1);\\
	\}
\end{array}
$$

Nájdite jeho pevný bod.
\end{example} % */

\begin{solution} % /*
	Program počíta prvých $x$ čísiel. Prepíšeme ho do systému
	rekurzívnej definície:
	$$
	\tau[\phi](x): \cmd{if}~ x = 0 ~\cmd{then}~ 0 ~\cmd{else}~ x +
	\phi(x - 1) ~\cmd{fi}
	$$

	Nájdime jeho pevný bod. Keďže je funkcionál spojitý, môžeme použiť
	Kleeneho vetu:

$$
\begin{array}{rcl}
\tau^0[\Omega]	& \equiv	& \Omega\\
\\
\tau^1[\Omega]	& \equiv	& \cmd{if}~ x = 0 ~\cmd{then}~ 0
								~\cmd{else}~ x + \tau^0[\Omega](x - 1) ~\cmd{fi}~ \equiv\\
				& \equiv	& \cmd{if}~ x = 0 ~\cmd{then}~ 0 ~\cmd{else} \perp \cmd{fi}\\
\\
\tau^2[\Omega]	& \equiv	& \cmd{if}~ x = 0 ~\cmd{then}~ 0
								~\cmd{else}~ x + \tau^1[\Omega](x - 1) ~\cmd{fi}~ \equiv\\
				& \equiv	& \cmd{if}~ x = 0 ~\cmd{then}~ 0
								~\cmd{else}~ x + (\cmd{if}~ x - 1 = 0
								~\cmd{then}~ 0 ~\cmd{else} \perp \cmd{fi}) ~\cmd{fi}\\
\\
\tau^3[\Omega]	& \equiv	& \cmd{if}~ x = 0 ~\cmd{then}~ 0
								~\cmd{else}~ x + \tau^2[\Omega](x - 1) ~\cmd{fi}~ \equiv\\
				& \equiv	& \cmd{if}~ x = 0 ~\cmd{then}~ 0\\
				&			& \cmd{else}~ x + (\cmd{if}~ x - 1 = 0
								~\cmd{then}~ 0 ~\cmd{else}~ x - 1 + (\cmd{if}~ x - 1 = 1 ~\cmd{then}~ 0
								~\cmd{else} \perp \cmd{fi}) ~\cmd{fi}) ~\cmd{fi}~ \equiv\\
				& \equiv	& \cmd{if}~ x = 0 ~\cmd{then}~ 0\\
				&			& \cmd{else}~ x + (\cmd{if}~ x = 1 ~\cmd{then}~ 0
											~\cmd{else}~ x - 1 + (\cmd{if}~ x = 2 ~\cmd{then}~ 0
														~\cmd{else} \perp \cmd{fi}) ~\cmd{fi}) ~\cmd{fi}\\
\cdots
\end{array}
$$

Nultý krok je podľa definície. V prvom kroku sme len upravili podmienku $x - 1 = 0$ na $x = 1$, čo
je to isté. Nič iné nie je možné v tomto kroku vykonať.

V druhom kroku je jednoduché dostať sa k výsledku, ale napriek tomu sa nad ním zamyslíme, čo to
znamená. Je to vlastne náš program definovaný pre $x = 0$ a $x = 1$. Pre ostatné hodnoty je
nedefinovaný.

Kroky tri je obdobný ako krok dva, pričom náš program je už samozrejme definovaný aj pre $x = 2$.

Čo sa vlastne pri aproximácii deje? Pri $k$-tej aproximácii by sme mohli s~výsledným funkcionálom
vypočítať sumu prvých $i$ čísiel, pre také $i < k$. Teraz už vlastne stačí zostrojiť najmenšiu hornú
hranicu tých aproximácií. A tou je pevný bod

$$
f_\tau = \frac{x(x + 1)}{2}
$$

% Na tomto mieste je vhodné sa zamyslieť, čo znamená najmenšia horná hranica. To je taký funkcionál,
% že všetky ostatné sú od neho menej schopné. Takže $k$-ta aproximácia dokáže sumy prvých $i$ čísiel,
% ale nie pre ľubovoľné~$i$. Zato pevný bod to dokáže pre hocijaké $i$. Pevný bod je teda najmenší, čo
% dokáže nájsť našu sumu.

\end{solution} % */

\begin{example} % /*
	Majme nasledovnú jednoduchú fukciu:

$$
\begin{array}{rcl}
	f_a(0) & = & 1\\
	f_a(x) & = & a \cdot f_a(x - 1)
\end{array}
$$

	Nájdite pevný bod.
\end{example} % */

\begin{solution} % /*

Najskôr to prepíšeme na funkcionál:

$$
\begin{array}{rcl}
	\phi(x)	& \equiv & \cmd{if}~ x = 0 ~\cmd{then}~ 1 ~\cmd{else}~ a \cdot \phi(x - 1) ~\cmd{fi}
\end{array}
$$

Teraz hľadajme pevný bod:

$$
\begin{array}{rcl}
\tau^0[\Omega]	& \equiv	& \Omega\\
\\
\tau^1[\Omega]	& \equiv	& \cmd{if}~ x = 0 ~\cmd{then}~ 1\\
& & \cmd{else} \perp \cmd{fi}\\
\\
\tau^2[\Omega]	& \equiv	& \cmd{if}~ x = 0 ~\cmd{then}~ 1\\
& & \cmd{else}~
	a \cdot (\cmd{if}~ x = 1 ~\cmd{then}~ 1 ~\cmd{else} \perp \cmd{fi}) ~\cmd{fi}\\
\\
\tau^3[\Omega]	& \equiv	& \cmd{if}~ x = 0 ~\cmd{then}~ 1\\
& & \cmd{else}~
	a \cdot (\cmd{if}~ x = 1 ~\cmd{then}~ 1 ~\cmd{else}~
		a \cdot (\cmd{if}~ x = 2 ~\cmd{then}~ 1 ~\cmd{else} \perp \cmd{fi})
	~\cmd{fi}) ~\cmd{fi}\\
\cdots
\end{array}
$$

Po rozpísaní štvrtého člena už môžeme vidieť ako to pekne aproximuje pevný bod.
Ten zapíšeme nasledovne:

$$
\begin{array}{rcl}
	f_p(x)	& \equiv & \cmd{if}~ x = 0 ~\cmd{then}~ 1 ~\cmd{else}~ a^x ~\cmd{fi}
\end{array}
$$

\end{solution} % */

\begin{example} % /*
	Máme funkciu:

	$$
	\begin{array}{rcl}
		f_0 & = & 0\\
		f(n) & = & f(f(n - 1))
	\end{array}
	$$

	Nájdite pevný bod tejto funkcie.

\end{example} % */

\begin{solution} % /*

Funkciu si najskôr rozpíšeme:
$$
\begin{array}{rcl}
	f(1) & = & f(f(0)) = f(0) = 0\\
	f(2) & = & f(f(1)) = f(f(f(0))) = f(f(0)) = f(0) = 0\\
	f(3) & = & f(f(2)) = f(f(f(1))) = f(f(f(f(0)))) = f(f(f(0))) = f(f(0)) = f(0) = 0
\end{array}
$$

Teraz ju zapíšeme v~tvare:

$$
\phi(x): \cmd{if}~ x = 0 ~\cmd{then}~ 0 ~\cmd{else}~ \phi(\phi(x - 1)) ~\cmd{fi}
$$

Hľadajme pevný bod:

$$
\begin{array}{rcl}
\tau^0	& \equiv	& \Omega\\
\tau^1  & \equiv	& \cmd{if}~ x = 0 ~\cmd{then}~ 0 ~\cmd{else} \perp \cmd{fi}\\
\tau^2  & \equiv	& \cmd{if}~ x = 0 ~\cmd{then}~ 0 ~\cmd{else}~ (\cmd{if}~[\cmd{if}~ x = 1 ~\cmd{then}~ 0
~\cmd{else} \perp \cmd{fi}] = 0 ~\cmd{then}~ 0 ~\cmd{else} \perp \cmd{fi}) ~\cmd{fi}\\
\tau^3  & \equiv	&
		\cmd{if}~ x = 0\\
& &		\cmd{then}~ 0\\
& &		\cmd{else}
		\begin{array}[t]{l}
			\cmd{if}~ [\cmd{if}~ x = 1 ~\cmd{then}~ 0 ~\cmd{else}~ (\cmd{if}~ x = 2 ~\cmd{then}~ 0
				~\cmd{else} \perp \cmd{fi})~\cmd{fi}] = 0\\
			\cmd{then}~ 0\\
			\cmd{else}
			\begin{array}[t]{l}
				\cmd{if}~
					\left[ \begin{array}[c]{l}
						\cmd{if}~
							\left[ \begin{array}[c]{l}
								\cmd{if}~ x = 1\\
								\cmd{then}~ 0\\
								\cmd{else}~ (\cmd{if}~ x = 2 ~\cmd{then}~ 0 ~\cmd{else} \perp \cmd{fi})\\
								\cmd{fi}
							\end{array} \right] = 1\\
						\cmd{then}~ 0\\
						\cmd{else} \perp\\
						\cmd{fi}
					\end{array} \right] = 0\\
				\cmd{then}~ 0\\
				\cmd{else} \perp\\
				\cmd{fi}
			\end{array}\\
			\cmd{fi}
		\end{array}\\
& &		\cmd{fi}
\end{array}
$$

Dosaďme do $\tau^3$ hodnotu $1$:
$$
\begin{array}{lcl}
\tau^3\{x = 1\}	&
	\equiv &
		\cmd{if}~ x = 0\\
& &		\cmd{then}~ 0\\
& &		\cmd{else}
			\begin{array}[t]{l}
				\cmd{if}~ 0 = 0\\
				\cmd{then}~ 0\\
				\cmd{else}~(\cmd{if}~ [\cmd{if} \perp = 1 ~\cmd{then}~ 0 ~\cmd{else} \perp \cmd{fi}]
					= 0 ~\cmd{then}~ 0 ~\cmd{else} \perp \cmd{fi})\\
				\cmd{fi}
			\end{array}\\
& &		\cmd{fi}\\
\tau^3\{x = 1\}	&
	\equiv &
		\cmd{if}~ x = 0 ~\cmd{then}~ 0 ~\cmd{else}~ 0 ~\cmd{fi}
\end{array}
$$

Dosaďme do $\tau^3$ tiež hodnotu $2$:
$$
\begin{array}{lcl}
\tau^3\{x = 2\}	&
	\equiv &
		\cmd{if}~ x = 0\\
& &		\cmd{then}~ 0\\
& &		\cmd{else}
			\begin{array}[t]{l}
				\cmd{if}~ 0 = 0\\
				\cmd{then}~ 0\\
				\cmd{else}~(\cmd{if}~ [\cmd{if}~ 0 = 1 ~\cmd{then}~ 0 ~\cmd{else} \perp \cmd{fi}]
					= 0 ~\cmd{then}~ 0 ~\cmd{else} \perp \cmd{fi})\\
				\cmd{fi}
			\end{array}\\
& &		\cmd{fi}\\
\tau^3\{x = 2\}	&
	\equiv &
		\cmd{if}~ x = 0 ~\cmd{then}~ 0 ~\cmd{else}~ 0 ~\cmd{fi}\\
\\
\tau^3\{x > 2\}	&
	\equiv &
		\cmd{if}~ x = 0\\
& &		\cmd{then}~ 0\\
& &		\cmd{else}
			\begin{array}[t]{l}
				\cmd{if} \perp = 0\\
				\cmd{then}~ 0\\
				\cmd{else}~(\cmd{if} \perp = 1 ~\cmd{then}~ 0 ~\cmd{else} \perp \cmd{fi})\\
				\cmd{fi}
			\end{array}\\
& &		\cmd{fi}\\
\tau^3\{x > 2\}	&
	\equiv &
		\cmd{if}~ x = 0 ~\cmd{then}~ 0 ~\cmd{else} \perp \cmd{fi}
\end{array}
$$

Skúsme teraz $\tau^4$:
$$
\begin{array}{lcl}
\tau^4	&	\equiv	&
	\cmd{if}~ x = 0\\
& &	\cmd{then}~ 0\\
& &	\cmd{else}~(\cmd{if}~[\cmd{if}~ x = 1 ~\cmd{then}~ 0 ~\cmd{else}~ 0 ~\cmd{fi}] = 0
		~\cmd{then}~ 0 ~\cmd{else}~ 0 ~\cmd{fi})\\
& &	\cmd{fi}\\
\tau^4	&	\equiv	&
	\cmd{if}~ x = 0 ~\cmd{then}~ 0 ~\cmd{else}~ 0 ~\cmd{fi}
\end{array}
$$

%Zdá sa, že to už je pevný bod. Overme to:
%
%$$
%\begin{array}{rcl}
%f_P	& \equiv & \cmd{if}~ x = 0 ~\cmd{then}~ 0 ~\cmd{else}~ (\cmd{if}~ [\cmd{if}~ x = 1 ~\cmd{then}~ 0 ~\cmd{else}~ 0
%~\cmd{fi}] = 0 ~\cmd{then}~ 0 ~\cmd{else}~ 0 ~\cmd{fi}) ~\cmd{fi} \equiv\\
%& \equiv & \cmd{if}~ x = 0 ~\cmd{then}~ 0 ~\cmd{else}~ 0 ~\cmd{fi}
%\end{array}
%$$

Vyzerá to tak, že pre $x \ge 0$ je to $0$, inak $\perp$. A to už je pevný bod $f_P$:

$$
\begin{array}{rcl}
	f_P	& \equiv & \cmd{if}~ x \ge 0 ~\cmd{then}~ 0 ~\cmd{else} \perp \cmd{fi}
\end{array}
$$

\end{solution} % */

\begin{example} % /*
	Uvažujme rovnakú funkciu $f$ ako v predchádzajúcom príklade. Nech $g(x)$ je jej pevný bod.
	Ukážte, že je silne ekvivalentný s~$f_P(x)$.
\end{example} % */

\begin{solution} % /*
	Fixpointovou indukciou dokážeme, že pre $x \ge 0$:
$$
f_P(x) \sqsubseteq g(x)
$$

Označme
$$
g(x) \equiv \cmd{if}~ x \ge 0 ~\cmd{then}~ 0 ~\cmd{else} \perp \cmd{fi}
$$

Podľa fixpointovej indukcie stačí dokázať, že $\tau[g] \sqsubseteq g$, čiže:

$$
\begin{array}{lcl}
	\left( \begin{array}{lcl}
	\cmd{if}~ x = 0\\
	\cmd{then}~ 0\\
	\cmd{else}~(\cmd{if}~[\cmd{if}~ x - 1 \ge 0 ~\cmd{then}~ 0 ~\cmd{else} \perp \cmd{fi}] \ge 0
			~\cmd{then}~ 0 ~\cmd{else} \perp \cmd{fi})\\
	\cmd{fi}
	\end{array} \right)
& \sqsubseteq &
	\left( \begin{array}{l}
	\cmd{if}~ x = 0\\
	\cmd{then}~ 0\\
	\cmd{else} \perp\\
	\cmd{fi}
	\end{array} \right)
\end{array}
$$

Rozdelíme to na nasledujúce prípady:
\begin{enumerate}
\item $x = 0$
	$$
	\begin{array}{lcl}
	\tau[g](x) & = & 0\\
	\tau[g](x) & = & g(x)
	\end{array}
	$$
\item $x - 1 \ge 0 \equiv x \ge 1$
	$$
	\begin{array}{lcl}
	\tau[g](x)	&	=	&
		\cmd{if}~ x = 0\\
	& &	\cmd{then}~ 0\\
	& &	\cmd{else}~(\cmd{if}~ 0 \ge 0
			~\cmd{then}~ 0 ~\cmd{else} \perp \cmd{fi})\\
	& &	\cmd{fi}\\
	\tau[g](x)	&	=	&
		\cmd{if}~ x = 0 ~\cmd{then}~ 0 ~\cmd{else}~ 0 ~\cmd{fi}\\
	\tau[g](x)	&	=	& g(x)
	\end{array}
	$$
\end{enumerate}

Teda platí $f_P \sqsubseteq g$. A navyše pre $x < 0$ platí $g(x) \sqsubseteq f_P(x)$,
pretože $g(x) = \perp$. Celkovo platí
$$
(g \sqsubseteq f_P) \land (f_P \sqsubseteq g) ~\Longrightarrow~ f_P \equiv g
$$

Teda $g$ je najmenší pevný bod.
\end{solution} % */

\begin{example} % /*
	Máme funkciu:

$$
	\phi(x): \cmd{if}~ x > 0 ~\cmd{then}~ \phi(\phi(x-1)) ~\cmd{else}~ x ~\cmd{fi}
$$

pre $x \in \mathbb{N}$.

Nájdite pevný bod tejto funkcie.

\end{example} % */

\begin{solution} % /*
	Najskôr si rozpíšeme čo to vlastne robí:

$$
\begin{array}[t]{rcl}
	\phi(0)	& =	& \cmd{if}~ 0 > 0 ~\cmd{then} \perp \cmd{else}~ 0 ~\cmd{fi}\\
			& =	& 0\\
	\phi(1)	& =	& \cmd{if}~ 1 > 0 ~\cmd{then}~ \phi(0) ~\cmd{else}~ 1 ~\cmd{fi}~ =\\
			& =	& \cmd{if}~ 1 > 0 ~\cmd{then}~ 0 ~\cmd{else}~ 1 ~\cmd{fi}~ =\\
			& =	& 0\\
	\phi(2)	& =	& \cmd{if}~ 2 > 0 ~\cmd{then}~ \phi(1) ~\cmd{else}~ 2 ~\cmd{fi}~ =\\
			& =	& \cmd{if}~ 2 > 0 ~\cmd{then}~ (\cmd{if}~ 1 > 0 ~\cmd{then}~ 0
					~\cmd{else}~ 1 ~\cmd{fi}) ~\cmd{else}~ 2 ~\cmd{fi}~ =\\
			& =	& \cmd{if}~ 2 > 0 ~\cmd{then}~ 0 ~\cmd{else}~ 2 ~\cmd{fi}~ =\\
			& =	& 0
\end{array}
$$

Riešenie:

$$
\begin{array}[t]{lcl}
\tau^0	& \equiv & \Omega\\
\tau^1	& \equiv & \cmd{if}~ x > 0 ~\cmd{then} \perp \cmd{else}~ x ~\cmd{fi}\\
\tau^2	& \equiv & \cmd{if}~ x > 0\\
		&	     & \cmd{then}
					\begin{array}[t]{l}
						\cmd{if}~[\cmd{if}~ x > 1 ~\cmd{then} \perp \cmd{else}~ x - 1 ~\cmd{fi}] > 0\\
						\cmd{then} \perp\\
						\cmd{else}~(\cmd{if}~ x > 1 ~\cmd{then} \perp \cmd{else}~ x - 1 ~\cmd{fi})\\
						\cmd{fi}
					\end{array}\\
			&	& \cmd{else}~ ?\\
			&	& \cmd{fi}\\
\tau^2\{x > 1\}
		& \equiv & \cmd{if}~ x > 0 ~\cmd{then}~ (\cmd{if} \perp > 0 ~\cmd{then} \perp
					\cmd{else} \perp \cmd{fi}) ~\cmd{else}~ x ~\cmd{fi}~ \equiv\\
		& \equiv & \cmd{if}~ x > 0 ~\cmd{then} \perp \cmd{else}~ x ~\cmd{fi}~ \equiv\\
		& \equiv & \tau^1\\
\tau^2\{x \le 1\}
		& \equiv & \cmd{if}~ x > 0 ~\cmd{then}~ (\cmd{if}~ x > 1 ~\cmd{then} \perp
					\cmd{else}~ x - 1 ~\cmd{fi}) ~\cmd{else}~ x ~\cmd{fi}~ \equiv\\
		& \equiv & \cmd{if}~ x > 0 ~\cmd{then}~ x - 1 ~\cmd{else}~ x ~\cmd{fi}
\end{array}
$$

A teraz pre $\tau^3$:

$$
\begin{array}[t]{lcl}
\tau^3
&\equiv	& \cmd{if}~ x > 0\\
&		& \cmd{then}
			\begin{array}[t]{l}
				\cmd{if}~ [\cmd{if}~ x > 1 ~\cmd{then}~ x - 2 ~\cmd{else}~ x - 1 ~\cmd{fi}] > 0\\
				\cmd{then}~ [\cmd{if}~ x > 1 ~\cmd{then}~ x - 2 ~\cmd{else}~ x - 1 ~\cmd{fi}] - 1\\
				\cmd{else}~ (\cmd{if}~ x > 1 ~\cmd{then}~ x - 2 ~\cmd{else}~ x - 1 ~\cmd{fi})\\
				\cmd{fi}
			\end{array}\\
&		& \cmd{else}~ x\\
&		& \cmd{fi}\\
\tau^3\{x > 1\}
&\equiv	& \cmd{if}~ x > 0 ~\cmd{then}~ (\cmd{if}~ x > 2 ~\cmd{then}~ x - 3
			~\cmd{else}~ x - 2 ~\cmd{fi}) ~\cmd{else}~ x ~\cmd{fi}\\
\tau^3\{x \le 1\}
&\equiv	& \cmd{if}~ x > 0 ~\cmd{then}~ (\cmd{if}~ x > 1 ~\cmd{then}~ x - 2
			~\cmd{else}~ x - 1 ~\cmd{fi}) ~\cmd{else}~ x ~\cmd{fi} \equiv\\
&\equiv	& \cmd{if}~ x > 0 ~\cmd{then}~ x - 2 ~\cmd{else}~ x ~\cmd{fi}
\end{array}
$$

Vznikli nám tri možnosti $\tau^3_1$, $\tau^3_2$ a $\tau^3_3$:

$$
\begin{array}{lcl}
\tau^3_1			& \equiv & \cmd{if}~ x > 0 ~\cmd{then}~ (\cmd{if}~ x > 2 ~\cmd{then}~ x - 3
									~\cmd{else}~ x - 2 ~\cmd{fi}) ~\cmd{else}~ x ~\cmd{fi}\\
\tau^3_2\{x > 2\}	& \equiv & \cmd{if}~ x > 0 ~\cmd{then}~ x - 3 ~\cmd{else}~ x ~\cmd{fi}
									~\equiv~ \tau^3_1\\
\tau^3_2\{x \le 2\}	& \equiv & \cmd{if}~ x > 0 ~\cmd{then}~ x - 2 ~\cmd{else}~ x ~\cmd{fi}
									~\equiv~ \tau^3_1\\
\tau^3_3			& \equiv & \cmd{if}~ x > 0 ~\cmd{then}~ x - 2 ~\cmd{else}~ x ~\cmd{fi}
\end{array}
$$

Vidíme, že prípad $\tau^3_2$ je totožný s~$\tau^3_1$. Takže ďalej nám stačí rozvinúť len možnosti
$\tau^3_1$ a $\tau^3_3$. Začneme s možnosťou $\tau[\tau^3_3]$:

$$
\begin{array}{lclcl}
\tau^4	& \equiv	& \tau[\tau^3_3]	& \equiv &
		\cmd{if}~ x > 0\\
& & & &	\cmd{then}
			\begin{array}[t]{l}
				\cmd{if}~ [\cmd{if}~ x > 1 ~\cmd{then}~ x - 3 ~\cmd{else}~ x - 1 ~\cmd{fi}] > 0\\
				\cmd{then}~ [\cmd{if}~ x > 1 ~\cmd{then}~ x - 3 ~\cmd{else}~ x - 1 ~\cmd{fi}] - 2\\
				\cmd{else}~ (\cmd{if}~ x > 1 ~\cmd{then}~ x - 3 ~\cmd{else}~ x - 1 ~\cmd{fi})\\
				\cmd{fi}
			\end{array}\\
& & & &	\cmd{else}~ x\\
& & & &	\cmd{fi}
\end{array}
$$

Čiže konkrétne vyjadrené:

$$
\begin{array}{lcl}
\tau^4\{x > 1\}				& \equiv & \cmd{if}~ x > 0 ~\cmd{then}~
		(\cmd{if}~ x > 3 ~\cmd{then}~ x - 5 ~\cmd{else}~ x - 3 ~\cmd{fi}) ~\cmd{else}~ x ~\cmd{fi}\\
\tau^4\{x > 1\}\{x > 3\}	& \equiv & \cmd{if}~ x > 0 ~\cmd{then}~ x - 5 ~\cmd{else}~ x ~\cmd{fi}\\
\tau^4\{x > 1\}\{x \le 3\}	& \equiv & \cmd{if}~ x > 0 ~\cmd{then}~ x - 3 ~\cmd{else}~ x ~\cmd{fi}\\
\tau^4\{x \le 1\}			& \equiv & \cmd{if}~ x > 0 ~\cmd{then}~
		(\cmd{if}~ x > 1 ~\cmd{then}~ x - 3 ~\cmd{else}~ x - 1 ~\cmd{fi}) ~\cmd{else}~ x ~\cmd{fi}\\
& \equiv & \cmd{if}~ x > 0 ~\cmd{then}~ x - 1 ~\cmd{else}~ x ~\cmd{fi}
\end{array}
$$

Pokračujeme s možnosťou $\tau[\tau^3_1]$:

$$
\begin{array}{lclcl}
\tau^4	& \equiv	& \tau[\tau^3_1]	& \equiv &
		\cmd{if}~ x > 0\\
& & & &	\cmd{then}
			\begin{array}[t]{l}
				\cmd{if}~ [\cmd{if}~ x > 1 ~\cmd{then}~ x - 4 ~\cmd{else}~ x ~\cmd{fi}] > 0\\
				\cmd{then}~ [\cmd{if}~ x > 1 ~\cmd{then}~ x - 4 ~\cmd{else}~ x ~\cmd{fi}] - 3\\
				\cmd{else}~ (\cmd{if}~ x > 1 ~\cmd{then}~ x - 4 ~\cmd{else}~ x ~\cmd{fi})\\
				\cmd{fi}
			\end{array}\\
& & & &	\cmd{else}~ x\\
& & & &	\cmd{fi}
\end{array}
$$

Aj toto konkrétne vyjadríme:

$$
\begin{array}{lcl}
\tau^4\{x > 1\}				& \equiv & \cmd{if}~ x > 0 ~\cmd{then}~
		(\cmd{if}~ x > 4 ~\cmd{then}~ x - 7 ~\cmd{else}~ x - 4 ~\cmd{fi}) ~\cmd{else}~ x ~\cmd{fi}\\
\tau^4\{x > 1\}\{x > 4\}	& \equiv & \cmd{if}~ x > 0 ~\cmd{then}~ x - 7 ~\cmd{else}~ x ~\cmd{fi}\\
\tau^4\{x > 1\}\{x \le 4\}	& \equiv & \cmd{if}~ x > 0 ~\cmd{then}~ x - 4 ~\cmd{else}~ x ~\cmd{fi}\\
\tau^4\{x \le 1\}			& \equiv & \cmd{if}~ x > 0 ~\cmd{then}~
		(\cmd{if}~ x > 0 ~\cmd{then}~ x - 3 ~\cmd{else}~ x ~\cmd{fi}) ~\cmd{else}~ x ~\cmd{fi}\\
& \equiv & \cmd{if}~ x > 0 ~\cmd{then}~ x - 3 ~\cmd{else}~ x ~\cmd{fi}
\end{array}
$$

Takto postupne konštruujeme aproximácie. Evidentne vyzerajú dobre, v~každom kroku nám pribudne $+1$
v niektorej z nich. Aký je teda pevný bod?

$$
f_P \equiv \cmd{if}~ x > 0 ~\cmd{then}~ 0 ~\cmd{else}~ x ~\cmd{fi}
$$

Čiže

$$
\begin{array}{cl}
f_P: &	\cmd{if}~ x > 0\\
	&	\cmd{then}
			\begin{array}[t]{l}
				\cmd{if}~ [\cmd{if}~ x > 1 ~\cmd{then}~ 0 ~\cmd{else}~ x - 1 ~\cmd{fi}] > 0\\
				\cmd{then}~ 0\\
				\cmd{else}~ (\cmd{if}~ x > 1 ~\cmd{then}~ 0 ~\cmd{else}~ x - 1 ~\cmd{fi})\\
				\cmd{fi}
			\end{array}\\
	&	\cmd{else}~ x\\
	&	\cmd{fi}
\end{array}
$$

sa nám rozloží na tri prípady:

\begin{enumerate}
\item
$
	\begin{array}[t]{rcl}
		x > 1 & \Rightarrow & \cmd{if}~ x > 0 ~\cmd{then}~ (\cmd{if}~ 0 > 0 ~\cmd{then}~ 0
		~\cmd{else}~ 0 ~\cmd{fi}) ~\cmd{else}~ x ~\cmd{fi} =\\
		& = & \cmd{if}~ x > 0 ~\cmd{then}~ 0 ~\cmd{else}~ x ~\cmd{fi}
	\end{array}
$
\item
$
	\begin{array}[t]{rcl}
		x = 1 & \Rightarrow & \cmd{if}~ x > 0 ~\cmd{then}~ (\cmd{if}~ x > 1 ~\cmd{then}~ 0
		~\cmd{else}~ x - 1 ~\cmd{fi}) ~\cmd{else}~ x ~\cmd{fi} =\\
		& = & \cmd{if}~ x > 0 ~\cmd{then}~ 0 ~\cmd{else}~ x ~\cmd{fi}
	\end{array}
$
\item
$
	\begin{array}[t]{rcl}
		x > 0 & \Rightarrow & \cmd{if}~ x > 0 ~\cmd{then}~ 0 ~\cmd{else}~ x ~\cmd{fi} =\\
		& = & \cmd{if}~ x > 0 ~\cmd{then}~ 0 ~\cmd{else}~ x ~\cmd{fi}
	\end{array}
$
\end{enumerate}

Ukázali sme, že $f_P$ je pevný bod.
%Je to ten posledný tretí prípad $0 - 1 = \perp$, pretože $x \in \mathbb{N}$.

\end{solution} % */

\begin{example} % /*
	Uvažujme rovnakú funkciu $f$ ako v predchádzajúcom príklade. Nech $g(x)$ je jej pevný bod.
	Ukážte, že je silne ekvivalentný s~$f_P(x)$.
\end{example} % */

\begin{solution} % /*
	Fixpointovou indukciou dokážeme, že pre $x \ge 0$:
$$
f_P(x) \sqsubseteq g(x)
$$

Označme
$$
g(x) \equiv \cmd{if}~ x > 0 ~\cmd{then}~ 0 ~\cmd{else}~ x ~\cmd{fi}
$$

Podľa fixpointovej indukcie stačí dokázať, že $\tau[g] \sqsubseteq g$, čiže:

$$
\begin{array}{lcl}
	\left( \begin{array}{lcl}
	\cmd{if}~ x > 0\\
	\cmd{then}
		\begin{array}[t]{l}
			\cmd{if}~[\cmd{if}~ x - 1 > 0 ~\cmd{then}~ 0 ~\cmd{else}~ x - 1 ~\cmd{fi}] > 0\\
			\cmd{then}~ 0\\
			\cmd{else}~ (\cmd{if}~ x - 1 > 0 ~\cmd{then}~ 0 ~\cmd{else}~ x - 1 ~\cmd{fi})\\
			\cmd{fi}
		\end{array}\\
	\cmd{else}~x\\
	\cmd{fi}
	\end{array} \right)
& \sqsubseteq &
	\left( \begin{array}{l}
	\cmd{if}~ x > 0\\
	\cmd{then}~ 0\\
	\cmd{else}~ x\\
	\cmd{fi}
	\end{array} \right)
\end{array}
$$

Rozdelíme to na nasledujúce prípady:
\begin{enumerate}
	\item $x = 0: \tau[g](x) = 0 = g(x)$
	\item $x > 0: \tau[g](x) = 0 = g(x)$
\end{enumerate}

Teda platí $f_P \sqsubseteq g$. A navyše pre $x < 0$ platí $g(x) = x$, potom musí $f(x) = x$ aby
platilo $g \sqsubseteq f_P$. Celkovo platí
$$
(g \sqsubseteq f_P) \land (f_P \sqsubseteq g) ~\Longrightarrow~ f_P \equiv g
$$

Teda $g$ je najmenší pevný bod.

\end{solution} % */

% vim: ts=4 tw=100
% vim600: fdl=0 fdm=marker fdc=0 fmr=/*,*/