%
% 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=/*,*/
Platon Group <platon@platon.org> http://platon.org/
|