%
% 06-funkcionalne-programovanie.tex
%
% Developed by Ondrej Jombik <nepto@platon.sk>
% Copyright (c) 2006 Platon Group, http://platon.sk/
% Licensed under terms of GNU General Public License.
% All rights reserved.
%
% Changelog:
% 2006-08-17 - created
%
% $Platon: doc/statnica-teoria-prog/06-funkcionalne-programovanie.tex,v 1.2 2006-08-19 08:23:02 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 $N$ 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)$\\
$(C \Rightarrow_\beta T) \Rightarrow CMN = TMN = (\lambda xy . x)MN = M$
\item $(C \Rightarrow_\beta F) \Rightarrow (CMN \Rightarrow_\beta N)$\\
$(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=/*,*/
Platon Group <platon@platon.org> http://platon.org/
|