Opensource.Platon.SK CVS: doc/statnica-teoria-prog/06-funkcionalne-programovanie.tex - diff

   Up to  [Platon] / doc / statnica-teoria-prog
Diff for doc/statnica-teoria-prog/06-funkcionalne-programovanie.tex between version 1.1 and 1.2


version 1.1, 2006/08/17 08:04:27
version 1.2, 2006/08/19 08:23:02



Line 10 




Line 10 




 % 2006-08-17 - created
 % 2006-08-17 - created


 %
 %


 
 


 % $Platon: $
 % $Platon: doc/statnica-teoria-prog/06-funkcionalne-programovanie.tex,v 1.1 2006-08-17 08:04:27 nepto Exp $


 
 


 \chapter{Funkcionálne programovanie}
 \chapter{Funkcionálne programovanie}


 
 


 
 \section{$\lambda$-kalkul} % /*


 
 


 
 \begin{defn}


 
         $$


 
         \langle exp \rangle := \lambda var . exp ~|~ exp ~|~ (exp) ~|~ const ~|~ (exp)(exp)


 
         $$


 
         kde


 
         \begin{enumerate}


 
                 \item $\lambda var . exp$ sa nazýva {\it lambda abstrakcia}


 
                 \item $(exp)(exp)$ sa nazýva {\it aplikácia}


 
                 \end{enumerate}


 
 \end{defn}


 
 


 
 \begin{defn}[Substitútcia] ~


 
         \begin{enumerate}


 
                 \item $x[x/a] = a$


 
                 \item $y[x/a] = y$


 
                 \item $c[x/a] = c$ (konšt.)


 
                 \item $(MN)[x/a] = (M[x/a])(N[x/a])$, čiže aplikácia termu $N[x/a]$ do $M[x/a]$


 
                 \item $(\lambda x M)[x/a] = \lambda x M$


 
                 \item $(\lambda y M)[x/a] = \lambda y M[x/a]$ ak $y$ nie je v $a$


 
                 \item $(\lambda y M)[x/a] = \lambda w (M[y/w])[x/a]$ ak $y$ je v $a$ (name clash problem)


 
         \end{enumerate}


 
 \end{defn}


 
 


 
 \begin{defn}[$\beta$-redukcia]


 
         $$


 
         (\lambda y M) N \Rightarrow_\beta M[y/N]


 
         $$


 
 \end{defn}


 
 


 
 % */


 
 


 
 \section{Čistý $\lambda$-kalkul} % /*


 
 


 
 \begin{defn}


 
         Rovnaká definícia ako $\lambda$-kalkul, ale neobsahuje $\langle exp \rangle := const$, tj. bez


 
         konštant, len funkcie vyjadrené ako lambda abstrakcie.


 
 \end{defn}


 
 


 
 \begin{defn}[IF-THEN-ELSE]


 
         Vyrobíme $\lambda$ term, ktorý nám zabezpečí funkcionalitu IF-THEN-ELSE.


 
         \begin{itemize}


 
                 \item označme $T$ tento $\lambda$ term $\lambda xy . x$, teda takto zakódujeme TRUE


 
                 \item označme $F$ tento $\lambda$ term $\lambda xy . y$, teda takto zakódujeme FALSE


 
                 \item označme $M$ tento $\lambda$ term $\lambda x . xT$, teda je to výber prvého argumentu


 
                 \item označme $M$ tento $\lambda$ term $\lambda x . xF$, teda je to výber druhého argumentu


 
         \end{itemize}


 
 \end{defn}


 
 


 
 \begin{defn}[IF]


 
         Nech $C$ je $\lambda$ term, potom {\bf IF $C$ THEN $M$ ELSE $N$} je v čistom lambda kalkule nasledujúci


 
         term:


 
         $$


 
         CMN


 
         $$


 
 \end{defn}


 
 


 
 \begin{veta} ~


 
         \begin{enumerate}


 
                 \item $(C \Rightarrow_\beta T) \Rightarrow (CMN \Rightarrow_\beta M)$


 
                 \item $(C \Rightarrow_\beta F) \Rightarrow (CMN \Rightarrow_\beta N)$


 
                 \item $(C \Rightarrow_\beta T) \Rightarrow (CMN = TMN = (\lambda xy . x)MN = M$


 
                 \item $(C \Rightarrow_\beta F) \Rightarrow (CMN = FMN = (\lambda xy . y)MN = N$


 
         \end{enumerate}


 
 \end{veta}


 
 


 
 ~


 
 


 
 Prevod konštánt do čistého $\lambda$-kalkulu pomocou numerálov:


 
 


 
 \begin{defn}


 
         Usporiadaná dvojica termov $M$ a $N$ je term:


 
         $$


 
         (M, N) = \lambda z . zMN


 
         $$


 
 \end{defn}


 
 


 
 \begin{defn}[Projekcie]


 
         Nech $L = (M, N)$, potom projekcie sú definované nasledovne:


 
         \begin{enumerate}


 
                 \item $(L)_1 = LT$


 
                 \item $(L)_2 = LF$


 
         \end{enumerate}


 
 \end{defn}


 
 


 
 \begin{defn}


 
         Pre každé nezáporné celé číslo je numerál toto:


 
         $$


 
         (0) = \lambda x . x


 
         $$


 
 \end{defn}


 
 


 
 % */


 
 


 % 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.1
 


changed lines


 
Added in v.1.2


















Platon Group <platon@platon.org> http://platon.org/
  Up to  [Platon] / doc / statnica-teoria-prog
-version 1.1, 2006/08/17 08:04:27
+version 1.2, 2006/08/19 08:23:02
 Line 10
 Line 10
 Line 10
  % 2006-08-17 - created
  %
- % $Platon: $
+ % $Platon: doc/statnica-teoria-prog/06-funkcionalne-programovanie.tex,v 1.1 2006-08-17 08:04:27 nepto Exp $
  \chapter{Funkcionálne programovanie}
+ \section{$\lambda$-kalkul} % /*
+ \begin{defn}
+         $$
+         \langle exp \rangle := \lambda var . exp ~|~ exp ~|~ (exp) ~|~ const ~|~ (exp)(exp)
+         $$
+         kde
+         \begin{enumerate}
+                 \item $\lambda var . exp$ sa nazýva {\it lambda abstrakcia}
+                 \item $(exp)(exp)$ sa nazýva {\it aplikácia}
+                 \end{enumerate}
+ \end{defn}
+ \begin{defn}[Substitútcia] ~
+         \begin{enumerate}
+                 \item $x[x/a] = a$
+                 \item $y[x/a] = y$
+                 \item $c[x/a] = c$ (konšt.)
+                 \item $(MN)[x/a] = (M[x/a])(N[x/a])$, čiže aplikácia termu $N[x/a]$ do $M[x/a]$
+                 \item $(\lambda x M)[x/a] = \lambda x M$
+                 \item $(\lambda y M)[x/a] = \lambda y M[x/a]$ ak $y$ nie je v $a$
+                 \item $(\lambda y M)[x/a] = \lambda w (M[y/w])[x/a]$ ak $y$ je v $a$ (name clash problem)
+         \end{enumerate}
+ \end{defn}
+ \begin{defn}[$\beta$-redukcia]
+         $$
+         (\lambda y M) N \Rightarrow_\beta M[y/N]
+         $$
+ \end{defn}
+ % */
+ \section{Čistý $\lambda$-kalkul} % /*
+ \begin{defn}
+         Rovnaká definícia ako $\lambda$-kalkul, ale neobsahuje $\langle exp \rangle := const$, tj. bez
+         konštant, len funkcie vyjadrené ako lambda abstrakcie.
+ \end{defn}
+ \begin{defn}[IF-THEN-ELSE]
+         Vyrobíme $\lambda$ term, ktorý nám zabezpečí funkcionalitu IF-THEN-ELSE.
+         \begin{itemize}
+                 \item označme $T$ tento $\lambda$ term $\lambda xy . x$, teda takto zakódujeme TRUE
+                 \item označme $F$ tento $\lambda$ term $\lambda xy . y$, teda takto zakódujeme FALSE
+                 \item označme $M$ tento $\lambda$ term $\lambda x . xT$, teda je to výber prvého argumentu
+                 \item označme $M$ tento $\lambda$ term $\lambda x . xF$, teda je to výber druhého argumentu
+         \end{itemize}
+ \end{defn}
+ \begin{defn}[IF]
+         Nech $C$ je $\lambda$ term, potom {\bf IF $C$ THEN $M$ ELSE $N$} je v čistom lambda kalkule nasledujúci
+         term:
+         $$
+         CMN
+         $$
+ \end{defn}
+ \begin{veta} ~
+         \begin{enumerate}
+                 \item $(C \Rightarrow_\beta T) \Rightarrow (CMN \Rightarrow_\beta M)$
+                 \item $(C \Rightarrow_\beta F) \Rightarrow (CMN \Rightarrow_\beta N)$
+                 \item $(C \Rightarrow_\beta T) \Rightarrow (CMN = TMN = (\lambda xy . x)MN = M$
+                 \item $(C \Rightarrow_\beta F) \Rightarrow (CMN = FMN = (\lambda xy . y)MN = N$
+         \end{enumerate}
+ \end{veta}
+ ~
+ Prevod konštánt do čistého $\lambda$-kalkulu pomocou numerálov:
+ \begin{defn}
+         Usporiadaná dvojica termov $M$ a $N$ je term:
+         $$
+         (M, N) = \lambda z . zMN
+         $$
+ \end{defn}
+ \begin{defn}[Projekcie]
+         Nech $L = (M, N)$, potom projekcie sú definované nasledovne:
+         \begin{enumerate}
+                 \item $(L)_1 = LT$
+                 \item $(L)_2 = LF$
+         \end{enumerate}
+ \end{defn}
+ \begin{defn}
+         Pre každé nezáporné celé číslo je numerál toto:
+         $$
+         (0) = \lambda x . x
+         $$
+ \end{defn}
+ % */
  % vim: ts=4 tw=100
  % vim600: fdl=0 fdm=marker fdc=0 fmr=/*,*/
 Legend:


Removed from v.1.1
 


changed lines


 
Added in v.1.2
 Legend:


Removed from v.1.1
 


changed lines


 
Added in v.1.2
-Removed from v.1.1
+Added in v.1.2


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