Platon Technologies
not logged in Login Registration
EnglishSlovak
open source software development celebrating 10 years of open source development! Friday, October 16, 2026
[BACK] [TXT][DIR] Up to [Platon] / doc / ztp-zbierka

Diff for doc/ztp-zbierka/04-semantika-programov.tex between version 1.9 and 1.10

version 1.9, 2007/07/30 04:55:09 version 1.10, 2007/08/06 04:56:50
Line 10 
Line 10 
 % 26/02/2003 - created  % 26/02/2003 - created
 %  %
   
 % $Platon: doc/ztp-zbierka/04-semantika-programov.tex,v 1.8 2007-07-14 20:53:45 nepto Exp $  % $Platon: doc/ztp-zbierka/04-semantika-programov.tex,v 1.9 2007-07-30 04:55:09 nepto Exp $
   
 \chapter{Sémantika programov}  \chapter{Sémantika programov}
   
Line 474  $$
Line 474  $$
 & &             \cmd{fi}\\  & &             \cmd{fi}\\
 \tau^3\{x = 2\} &  \tau^3\{x = 2\} &
         \equiv &          \equiv &
                 \cmd{if}~ x = 0 ~\cmd{then}~ 0 ~\cmd{else}~ 0 ~\cmd{fi}                  \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}  \end{array}
 $$  $$
   
Line 502  $$
Line 518  $$
 %\end{array}  %\end{array}
 %$$  %$$
   
 A to už je pevný bod $f_P$:  Vyzerá to tak, že pre $x \ge 0$ je to $0$, inak $\perp$. A to už je pevný bod $f_P$:
   
 $$  $$
 \begin{array}{rcl}  \begin{array}{rcl}
         f_P     & \equiv & \cmd{if}~ x = 0 ~\cmd{then}~ 0 ~\cmd{else}~ 0 ~\cmd{fi}          f_P     & \equiv & \cmd{if}~ x \ge 0 ~\cmd{then}~ 0 ~\cmd{else} \perp \cmd{fi}
 \end{array}  \end{array}
 $$  $$
   
 \end{solution} % */  \end{solution} % */
   
 \begin{example} % /*  \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}
           \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}
   & \sqsubseteq &
           \begin{array}{l}
           \cmd{if}~ x = 0\\
           \cmd{then}~ 0\\
           \cmd{else} \perp\\
           \cmd{fi}
           \end{array}
   \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:          Máme funkciu:
   
 $$  $$
Line 661  $$
Line 748  $$
 \end{array}  \end{array}
 $$  $$
   
 Aj toto konkretne vyjadríme:  Aj toto konkrétne vyjadríme:
   
 $$  $$
 \begin{array}{lcl}  \begin{array}{lcl}
Line 679  Takto postupne konštruujeme aproximácie.
Line 766  Takto postupne konštruujeme aproximácie.
 v niektorej z nich. Aký je teda pevný bod?  v niektorej z nich. Aký je teda pevný bod?
   
 $$  $$
 f_P \equiv \cmd{if}~ x > 0 ~\cmd{then} \perp \cmd{else}~ x ~\cmd{fi}  f_P \equiv \cmd{if}~ x > 0 ~\cmd{then}~ 0 ~\cmd{else}~ x ~\cmd{fi}
 $$  $$
   
 Čiže  Čiže
Line 689  $$
Line 776  $$
 f_P: &  \cmd{if}~ x > 0\\  f_P: &  \cmd{if}~ x > 0\\
         &       \cmd{then}          &       \cmd{then}
                         \begin{array}[t]{l}                          \begin{array}[t]{l}
                                 \cmd{if}~ [\cmd{if}~ x > 1 ~\cmd{then} \perp \cmd{else}~ x - 1 ~\cmd{fi}] > 0\\                                  \cmd{if}~ [\cmd{if}~ x > 1 ~\cmd{then}~ 0 ~\cmd{else}~ x - 1 ~\cmd{fi}] > 0\\
                                 \cmd{then} \perp\\                                  \cmd{then}~ 0\\
                                 \cmd{else}~ (\cmd{if}~ x > 1 ~\cmd{them} \perp \cmd{else}~ x - 1 ~\cmd{fi})\\                                  \cmd{else}~ (\cmd{if}~ x > 1 ~\cmd{then}~ 0 ~\cmd{else}~ x - 1 ~\cmd{fi})\\
                                 \cmd{fi}                                  \cmd{fi}
                         \end{array}\\                          \end{array}\\
         &       \cmd{else}~ x\\          &       \cmd{else}~ x\\
Line 705  sa nám rozloží na tri prípady:
Line 792  sa nám rozloží na tri prípady:
 \item  \item
 $  $
         \begin{array}[t]{rcl}          \begin{array}[t]{rcl}
                 x > 1 & \Rightarrow & \cmd{if}~ x > 0 ~\cmd{then}~ (\cmd{if}~ \perp > 0 ~\cmd{then} \perp                  x > 1 & \Rightarrow & \cmd{if}~ x > 0 ~\cmd{then}~ (\cmd{if}~ 0 > 0 ~\cmd{then}~ 0
                 \cmd{else} \perp \cmd{fi}) ~\cmd{else}~ x ~\cmd{fi} =\\                  ~\cmd{else}~ 0 ~\cmd{fi}) ~\cmd{else}~ x ~\cmd{fi} =\\
                 & = & \cmd{if}~ x > 0 ~\cmd{then} \perp \cmd{else}~ x ~\cmd{fi}                  & = & \cmd{if}~ x > 0 ~\cmd{then}~ 0 ~\cmd{else}~ x ~\cmd{fi}
         \end{array}          \end{array}
 $  $
 \item  \item
 $  $
         \begin{array}[t]{rcl}          \begin{array}[t]{rcl}
                 x = 1 & \Rightarrow & \cmd{if}~ x > 0 ~\cmd{then}~ (\cmd{if}~ x > 1 ~\cmd{then} \perp                  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{else}~ x - 1 ~\cmd{fi}) ~\cmd{else}~ x ~\cmd{fi} =\\
                 & = & \cmd{if}~ x > 0 ~\cmd{then} \perp \cmd{else}~ x ~\cmd{fi}                  & = & \cmd{if}~ x > 0 ~\cmd{then}~ 0 ~\cmd{else}~ x ~\cmd{fi}
         \end{array}          \end{array}
 $  $
 \item  \item
 $  $
         \begin{array}[t]{rcl}          \begin{array}[t]{rcl}
                 x = 0 & \Rightarrow & \cmd{if}~ x > 0 ~\cmd{then}~ 0 - 1 ~\cmd{else}~ x ~\cmd{fi} =\\                  x > 0 & \Rightarrow & \cmd{if}~ x > 0 ~\cmd{then}~ 0 ~\cmd{else}~ x ~\cmd{fi} =\\
                 & = & \cmd{if}~ x > 0 ~\cmd{then} \perp \cmd{else}~ x ~\cmd{fi}                  & = & \cmd{if}~ x > 0 ~\cmd{then}~ 0 ~\cmd{else}~ x ~\cmd{fi}
         \end{array}          \end{array}
 $  $
 \end{enumerate}  \end{enumerate}
   
 Je to ten posledný tretí prípad $0 - 1 = \perp$, pretože $x \in \mathbb{N}$.  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}
           \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}
   & \sqsubseteq &
           \begin{array}{l}
           \cmd{if}~ x > 0\\
           \cmd{then}~ 0\\
           \cmd{else}~ x\\
           \cmd{fi}\\
           ~\\
           ~\\
           ~
           \end{array}
   \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} % */  \end{solution} % */
   
Legend:
Removed from v.1.9  
changed lines
  Added in v.1.10
Platon Group <platon@platon.org> http://platon.org/
Copyright © 2002-2006 Platon Group
Site powered by Metafox CMS 		Go to Top