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.3 and 1.4


version 1.3, 2005/11/23 19:33:59
version 1.4, 2007/06/03 11:33:05



Line 10 




Line 10 




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


 %
 %


 
 


 % $Platon: doc/ztp-zbierka/04-semantika-programov.tex,v 1.2 2004/05/18 19:39:27 nepto Exp $
 % $Platon: doc/ztp-zbierka/04-semantika-programov.tex,v 1.3 2005-11-23 19:33:59 nepto Exp $


 
 


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


 
 




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




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




 
 


 \end{solution} % */
 \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\\


 
 \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}~ \equiv\\


 
                                 & \equiv        & \cmd{if}~ x = 0 ~\cmd{then}~ 0 ~\cmd{else}~ x + \cmd{if}~ x + \cmd{if}


 
                                 x - 1 = 0 ~\cmd{then}~ 0 ~\cmd{else}~ x - 1 + \cmd{if}~ x = 2 ~\cmd{then}~ 0


 
                                 ~\cmd{else} \perp \cmd{fi}~\cmd{fi}~\cmd{fi}\\


 
 ... & &


 
 \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 všemohúci


 
 a~zároveň najmenší všemohúci, čo dokáže nájsť našu sumu.


 
 


 
 \end{solution} % */


 
 


 % vim: ts=4
 % vim: ts=4


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


 
 









Legend:


Removed from v.1.3
 


changed lines


 
Added in v.1.4


















Platon Group <platon@platon.org> http://platon.org/
  Up to  [Platon] / doc / ztp-zbierka
-version 1.3, 2005/11/23 19:33:59
+version 1.4, 2007/06/03 11:33:05
 Line 10
 Line 10
 Line 10
  % 26/02/2003 - created
  %
- % $Platon: doc/ztp-zbierka/04-semantika-programov.tex,v 1.2 2004/05/18 19:39:27 nepto Exp $
+ % $Platon: doc/ztp-zbierka/04-semantika-programov.tex,v 1.3 2005-11-23 19:33:59 nepto Exp $
  \chapter{Sémantika programov}
 Line 136  Rovnosť rozložíme na dva možné prípady.
 Line 136  Rovnosť rozložíme na dva možné prípady.
 Line 136  Rovnosť rozložíme na dva možné prípady.
  \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\\
+ \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}~ \equiv\\
+                                 & \equiv        & \cmd{if}~ x = 0 ~\cmd{then}~ 0 ~\cmd{else}~ x + \cmd{if}~ x + \cmd{if}
+                                 x - 1 = 0 ~\cmd{then}~ 0 ~\cmd{else}~ x - 1 + \cmd{if}~ x = 2 ~\cmd{then}~ 0
+                                 ~\cmd{else} \perp \cmd{fi}~\cmd{fi}~\cmd{fi}\\
+ ... & &
+ \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 všemohúci
+ a~zároveň najmenší všemohúci, čo dokáže nájsť našu sumu.
+ \end{solution} % */
  % vim: ts=4
  % vim600: fdl=0 fdm=marker fdc=0 fmr=/*,*/
 Legend:


Removed from v.1.3
 


changed lines


 
Added in v.1.4
 Legend:


Removed from v.1.3
 


changed lines


 
Added in v.1.4
-Removed from v.1.3
+Added in v.1.4


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