Opensource.Platon.SK CVS: doc/ztp-zbierka/04-semantika-programov.tex - diff

   Up to  [Platon] / doc / ztp-zbierka
Diff for doc/ztp-zbierka/04-semantika-programov.tex between version 1.7 and 1.8


version 1.7, 2007/07/14 06:56:14
version 1.8, 2007/07/14 20:53:45



Line 10 




Line 10 




 % 26/02/2003 - created
 % 26/02/2003 - created


 %
 %


 
 


 % $Platon: doc/ztp-zbierka/04-semantika-programov.tex,v 1.6 2007-07-12 04:29:45 nepto Exp $
 % $Platon: doc/ztp-zbierka/04-semantika-programov.tex,v 1.7 2007-07-14 06:56:14 nepto Exp $


 
 


 \chapter{Sémantika programov}
 \chapter{Sémantika programov}


 
 




Line 512  $$




Line 512  $$




 
 


 \end{solution} % */
 \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 konkretne 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} \perp \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} \perp \cmd{else}~ x - 1 ~\cmd{fi}] > 0\\


 
                                 \cmd{then} \perp\\


 
                                 \cmd{else}~ (\cmd{if}~ x > 1 ~\cmd{them} \perp \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}~ \perp > 0 ~\cmd{then} \perp


 
                 \cmd{else} \perp \cmd{fi}) ~\cmd{else}~ x ~\cmd{fi} =\\


 
                 & = & \cmd{if}~ x > 0 ~\cmd{then} \perp \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} \perp


 
                 \cmd{else}~ x - 1 ~\cmd{fi}) ~\cmd{else}~ x ~\cmd{fi} =\\


 
                 & = & \cmd{if}~ x > 0 ~\cmd{then} \perp \cmd{else}~ x ~\cmd{fi}


 
         \end{array}


 
 $


 
 \item


 
 $


 
         \begin{array}[t]{rcl}


 
                 x = 0 & \Rightarrow & \cmd{if}~ x > 0 ~\cmd{then}~ 0 - 1 ~\cmd{else}~ x ~\cmd{fi} =\\


 
                 & = & \cmd{if}~ x > 0 ~\cmd{then} \perp \cmd{else}~ x ~\cmd{fi}


 
         \end{array}


 
 $


 
 \end{enumerate}


 
 


 
 Je to ten posledný tretí prípad $0 - 1 = \perp$, pretože $x \in \mathbb{N}$.


 
 


 
 \end{solution} % */


 
 


 % vim: ts=4 tw=100
 % vim: ts=4 tw=100


 % vim600: fdl=0 fdm=marker fdc=0 fmr=/*,*/
 % vim600: fdl=0 fdm=marker fdc=0 fmr=/*,*/









Legend:


Removed from v.1.7
 


changed lines


 
Added in v.1.8


















Platon Group <platon@platon.org> http://platon.org/
  Up to  [Platon] / doc / ztp-zbierka
-version 1.7, 2007/07/14 06:56:14
+version 1.8, 2007/07/14 20:53:45
 Line 10
 Line 10
 Line 10
  % 26/02/2003 - created
  %
- % $Platon: doc/ztp-zbierka/04-semantika-programov.tex,v 1.6 2007-07-12 04:29:45 nepto Exp $
+ % $Platon: doc/ztp-zbierka/04-semantika-programov.tex,v 1.7 2007-07-14 06:56:14 nepto Exp $
  \chapter{Sémantika programov}
 Line 512  $$
 Line 512  $$
 Line 512  $$
  \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 konkretne 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} \perp \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} \perp \cmd{else}~ x - 1 ~\cmd{fi}] > 0\\
+                                 \cmd{then} \perp\\
+                                 \cmd{else}~ (\cmd{if}~ x > 1 ~\cmd{them} \perp \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}~ \perp > 0 ~\cmd{then} \perp
+                 \cmd{else} \perp \cmd{fi}) ~\cmd{else}~ x ~\cmd{fi} =\\
+                 & = & \cmd{if}~ x > 0 ~\cmd{then} \perp \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} \perp
+                 \cmd{else}~ x - 1 ~\cmd{fi}) ~\cmd{else}~ x ~\cmd{fi} =\\
+                 & = & \cmd{if}~ x > 0 ~\cmd{then} \perp \cmd{else}~ x ~\cmd{fi}
+         \end{array}
+ $
+ \item
+ $
+         \begin{array}[t]{rcl}
+                 x = 0 & \Rightarrow & \cmd{if}~ x > 0 ~\cmd{then}~ 0 - 1 ~\cmd{else}~ x ~\cmd{fi} =\\
+                 & = & \cmd{if}~ x > 0 ~\cmd{then} \perp \cmd{else}~ x ~\cmd{fi}
+         \end{array}
+ $
+ \end{enumerate}
+ Je to ten posledný tretí prípad $0 - 1 = \perp$, pretože $x \in \mathbb{N}$.
+ \end{solution} % */
  % vim: ts=4 tw=100
  % vim600: fdl=0 fdm=marker fdc=0 fmr=/*,*/
 Legend:


Removed from v.1.7
 


changed lines


 
Added in v.1.8
 Legend:


Removed from v.1.7
 


changed lines


 
Added in v.1.8
-Removed from v.1.7
+Added in v.1.8


Copyright © 2002-2006 Platon Group Site powered by Metafox CMS	Go to Top