%
% 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=/*,*/