Up to [Platon] / doc / ztp-zbierka

Several changed and corrections done on the Heathrow airport

%
% 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=/*,*/