Platon Technologies
not logged in Login Registration
EnglishSlovak
open source software development celebrating 10 years of open source development! Thursday, March 28, 2024

File: [Platon] / doc / statnica-teoria-prog / 06-funkcionalne-programovanie.tex (download)

Revision 1.3, Mon Sep 4 09:31:52 2006 UTC (17 years, 6 months ago) by nepto


Changes since 1.2: +6 -6 lines

Some late fixes

%
% 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/
Copyright © 2002-2006 Platon Group
Site powered by Metafox CMS
Go to Top