Programovanie v $\lambda$-kalkule
$\lambda$-kalkul je univerzálny výpočtový model a môže byť považovaný za najstarší a najjednoduchší Turingovsky úplný programovací jazyk. Pojem univerzálny zjednodušené povedané znamená, že môže vykonať akýkoľvek program.
Jazyky vyšších úrovní majú mnoho syntaktických foriem a údajových štruktúr, pričom minimalistický jazyk $\lambda$-kalkulu obsahuje len 3 syntaktické formy termov. Z tohto dôvodu na prvý pohľad nie je zrejme, ako je možné tieto vyššie-úrovňové konštrukcie preložiť do $\lambda$-kalkulu.
V tejto kapitole bude predstavených niekoľko štandardných príkladov programovania v $\lambda$-kalkule. Začneme definíciou funkcií vyššieho rádu a následne bude postupne predstavené ako je možné definovať v $\lambda$-kalkule:
- Boolean hodnoty,
- operácie nad Boolean hodnotami,
- údajové štruktúry na príklade jednoduchej štruktúry dvojica (pair) a operácie nad ňou,
- prirodzené čísla,
- základné aritmetické operácie nad prirodzenými číslami,
Všetky tieto operácie sú definované ako kombinátory.
Na záver bude predstavené ako definovať a vypočítať rekurzívne funkcie využitím kombinátora fixného bodu.
Poznámka
Pre praktickú demonštráciu uvedených postupov bude využitý reálny funkcionálny programovací jazyk OCaml.
- Term $\lambda x. x$ je možné v jazyku OCaml ako
fun x -> x
- Jazyk OCaml využíva pre definíciu funkcií syntaktickú konštrukciu let (ktorej sa budeme venovať podrobnejšie neskôr). Identickú funkciu $id = \lambda x. x$ je možné v jazyku OCaml definovať následovne:
let id = fun x -> x
- resp. využitím ekvivalentného zápisu:
let id x = x
Poznámka
V jazyku Haskell je možné definovať $\lambda$-termy následovne:
\x -> x
Funkcie vyššieho rádu
Na začiatok je potrebné si všimnúť, že $\lambda$-kalkul neposkytuje vstavanú podporu pre funkcie s viacerými argumentami. Samozrejme, nebolo by zložité rozšíriť jeho definíciu o podporu takýchto konštrukcií, avšak je jednoduchšie dosiahnuť rovnaký efekt použitím funkcií vyššieho rádu, ktoré vracajú ako výsledky iné funkcie.
Majme term $s$ obsahujúci dve voľné premenné $x$ a $y$ a chceme definovať funkciu $f$, ktorá pre každý pár $(v, u)$ argumentov vráti výsledok nahradenia $v$ za $x$ a $u$ za $y$ v terme $s$.
Namiesto toho, aby sme písali $$f = \lambda(x, y).s$$ ako by to bolo možné v nejakom jazyku vyššej úrovne, budeme písať $$f = \lambda x.\lambda y.s$$
- To znamená, že $f$ je funkcia, ktorá má jeden parameter $x$.
- Ak je aplikovaná na hodnotu $v$ substituuje premennú $x$ a vráti novú funkciu.
- Nová funkcia má jeden parameter $y$ a keď je aplikovaná hodnotu $u$, substituuje ju za premennú $y$ a vráti požadovaný výsledok.
Funkciu $f$ aplikujeme postupne na argumenty: $$f\ v\ u,$$ pričom aplikácia je ľavo asociatívna, to znamená: $$(f\ v)\ u,$$ čo sa redukuje tak, že funkcia $f$ je aplikovaná na argument $v$, táto aplikácia poskytne novú funkciu, ktorá bude aplikovaná na argument $u$: $$((\lambda x.\lambda y.s)\ v)\ u \to (\lambda y.[x \mapsto v]s)\ u \to [y \mapsto u][x \mapsto v]s$$
Táto transformácia funkcií s viacerými argumentmi na funkcie vyššieho rádu sa nazýva currying na počesť Haskella Curryho.
Poznámka
Na počesť Haskella Curryho je pomenovaný aj populárny funkcionálny programovací jazyk Haskell.
Príklad
Majme funkciu
$$ \begin{array}{lcl} (\lambda x. \lambda y. x\ y)\ u\ v & = & \quad \quad \quad \quad \text{//Funkcia vyššieho rádu}\\ ((\lambda x. \lambda y. x\ y)\ u)\ v & \to & \quad \quad \quad \quad \text{//Ľavá asociativita}\\ (\lambda y. u\ y)\ v & \to & \quad \quad \quad \quad \text{//Nová funkcia } \lambda y. u\ y \\ u\ v & \to & \quad \quad \quad \quad \text{//Normálna forma} \\ \end{array} $$
Churchove Boolean hodnoty ako kombinátory
Church definoval $\lambda$-kalkul na základe sloganu "všetko sa dá vyjadriť funkciou". V čistom $\lambda$-kalkule nie sú definované konštanty. Otázka, ktorá nás napadne, znie:
Je možné definovať pravdivostné hodnoty true a false ako funkcie?
Church definoval kombinátory pre konštanty pravdivostných hodnôt ako funkcie dvoch premenných: $$ \begin{array}{lcl} true &=& \lambda x.\lambda y.x\\ false &=& \lambda x.\lambda y.y \end{array} $$
Termy $true$ a $false$ je možné vnímať ako reprezentáciu boolean hodnôt "pravda" a "nepravda" v tom zmysle, že tieto termy je možné použiť na vykonávanie operácie testovania pravdivostnej hodnoty.
Následne je možné použiť aplikáciu ($\lambda$-aplikáciu) na definovanie kombinátora $test$, ktorý je analógiou programovej konštrukcie if then else, s vlastnosťou, že $$test\ b\ u\ v$$ sa redukuje na $u$, ak $b$ je $true$, resp. redukuje sa na $v$, ak $b$ je $false$, následovne: $$ test = \lambda b. \lambda c.\lambda a.\ b\ c\ a $$
Je potrebné si uvedomiť, že kombinátor $test$ len substituuje premenne $b,c,a$ za argumenty, pričom aby ďalší výpočet mal zmysel, ako prvý argument je očakávaná Boolean hodnota, resp. funkcia ktorá sa redukuje na Boolean hodnotu.
Až následne samotná Boolean hodnota $b$ je "podmienka":
- $true$ je funkcia, ktorá očakáva dva argumenty a vráti prvý z nich.
- $false$ je funkcia, ktorá očakáva dva argumenty a vráti druhý z nich.
Príklad
Majme daný následujúci term: $$test\ true\ u\ v$$ Pre nájdenie jeho normálnej formy, v prvom kroku pristúpime k nahradeniu $test$ jeho definíciou a pokračuje redukciou: $$ \begin{array}{lc} test\ true\ u\ v &= \\ (\lambda b. \lambda c.\lambda a.\ b\ c\ a)\ true\ u\ v & \to \\ (\lambda c.\lambda a.\ true\ c\ a)\ u\ v & \to \\ (\lambda a.\ true\ u\ a)\ v & \to \\ true\ u\ v & = \\ (\lambda x.\lambda y.x)\ u\ v & \to \\ (\lambda y.u)\ v & \to \\ u \\ \end{array} $$
Poznámka
Pri nahrádzaní názvov funkcií resp. kombinátorov ich reálnou definíciou, je vždy potrebné danú definíciu uzavrieť do zátvoriek.
Príklad
V jazyku OCaml je možné tieto kombinátory definovať nasledovne:
let tru = fun x -> fun y -> x;;
let fls = fun x -> fun y -> y;;
let test = fun a -> fun b -> fun c -> a b c;;
Boolean operácie
Pre Churchove pravdivostné hodnoty je možné definovať aj logické operácie ako funkcie. Napríklad konjunkciu, disjunkciu a negáciu je možné definovať následovne:
\begin{align*} and & = \lambda b. \lambda c. \ b \ c \ false \newline or & = \lambda b. \lambda c. \ b \ true \ c \newline not & = \lambda b. \ b \ false \ true \end{align*}
- Funkcia $and$ má dva parametre: boolovské hodnoty $b$ a $c$:
- ak $b$ je $true$, potom and vráti $c$,
- ak $b$ je $false$, potom and vráti $false$.
- Podobne sa je možné vysvetliť aj ostatné dva kombinátory.
Poznámka
Definícia ďalších logických operátorov je možná aj prostredníctvom už existujúcich kombinátorov. Ak máme definovanú jednu binárnu logickú operáciu a negáciu, prostredníctvom nich je možné vyjadriť všetky ostatné spojky.
Príklad
V jazyku OCaml je možné tieto kombinátory definovať nasledovne:
let andb = fun a -> fun b -> a b tru;;
let orb = fun a -> fun b -> a tru b;;
let negb = fun a -> a fls tru;;
Údajová štruktúra dvojica hodnôt
Ak už máme definované Boolean hodnoty, je možné definovať kombinátory poskytujúce údajové štruktúry. Ako príklad demonštrujeme jednoduchú údajovú štruktúra dvojica hodnôt (pair):
\begin{align*} pair & = \lambda f. \lambda s. \lambda b. \ b \ f \ s \newline fst & = \lambda p. \ p \ true \newline snd & = \lambda p. \ p \ false \end{align*}
- Funkcia $pair$ je definovaná pomocou Boolean hodnoty $b$. Jej aplikácia $pair \ v \ w$ vytvorí dvojicu z hodnôt $v$ a $w$.
- Funkcia $fst$ vráti prvý člen dvojice.
- Funkcia $snd$ vráti druhý člen dvojice.
- $fst$ a $snd$ sú projekcie, získame ich dosadením príslušnej Boolean hodnoty.
Príklad
Majme daný následujúci term: $$fst\ (pair\ u\ v)$$ Najdite jeho normálnu formu.
Riešenie
$$ \begin{array}{rll} fst\ (pair \ u \ v) = & fst((\lambda f . \lambda s . \lambda b. \ b \ f \ s) \ u \ v) \\ & fst((\lambda s . \lambda b. \ b \ u \ s) \ v) & \to\\ & fst(\lambda b. \ b \ u \ v) & \to \\ & (\lambda p. \ p \ true)(\lambda b. \ b \ u \ v)& \to \\ & (\lambda b. \ b \ u \ v) \ tru & \to \\ & true \ u \ v & = \\ & (\lambda x . \lambda y . x) \ u \ v & \to \\ & (\lambda y . \ u) \ v & \to \\ & u \end{array} $$
Príklad
V jazyku OCaml je možné tieto kombinátory definovať nasledovne:
let pair = fun f -> fun s -> fun b -> b f s;;
let first = fun p -> p tru;;
let second = fun p -> p fls;;
Churchove čísla ako kombinátory
Church definoval aj prirodzené čísla a nulu ako $\lambda$-termy, konkrétne ako funkcie s dvoma parametrami: $$\lambda successor.\lambda zero.'\text{niečo}'$$
Využil poznatok, že každé prirodzené číslo sa dá vyjadriť pomocou nuly a funkcie nasledovníka (successor):
$$ \begin{array}{rcl} 0 & = & \lambda s. \lambda z. \ z \\ 1 & = & \lambda s. \lambda z. \ s \ z \\ 2 & = & \lambda s. \lambda z. \ s \ (s \ z) \\ 3 & = & \lambda s. \lambda z. \ s \ (s \ (s \ z)) \\ \vdots & & \end{array} $$
- $s$ označuje successor, $z$ označuje nulu.
- Pri definícii nuly ako funkcie $0$ sa v tele funkcie nenachádza $s$.
- Pri definícii jednotky ako funkcie $1$ sa $s$ aplikuje raz na nulu.
- Pri definícii dvojky ako funkcie $2$ sa $s$ aplikuje dvakrát, atď.
To je možné zovšeobecniť to nasledujúcim spôsobom:
Každé prirodzené číslo $n$ je definované kombinátorom $n$, t.j. funkciou, ktorá má dva parametre:
-
$s$ pre successor;
-
$z$ pre nulu.
-
Číslo $n$ dostaneme $n$ násobnou aplikáciou $s$ na $z$.
Všimnime si, že $false$ a $0$ sú definované rovnakým termom (platí $\alpha$-konverzia).
$$ false = \lambda x.\lambda y.y \quad \quad \quad 0 = \lambda s.\lambda z.z$$
Poznámka
Podobné situácie sú napríklad v asemblerovských jazykoch, kde rovnaká postupnosť bitov môže reprezentovať mnoho rôznych hodnôt: celé čísla, reálne čísla, adresy. Závisí od interpretácie, s ktorou hodnotou pracujeme.
Sčı́tanie Churchových čı́sel
Funkciu sčítania Churchových čísel $m$ a $n$ definujeme ako funkciu $add$:
$$plus = \lambda m.\lambda n.\lambda s.\lambda z.\ m\ s\ (n\ s\ z)$$
- Funkcia $add$ vezme dva argumenty (hodnoty parametrov $m$ a $n$) a vráti ich súčet.
- Uvedomme si, že výsledok je funkcia dvoch premenných $s$ a $z$.
- Aplikuje sa $n$-krát $s$ na $z$ a $m$-krát $s$ na $(n\ s\ z)$. Tak dostaneme súčet $m + n$.
Poznámka
Zjednodušene povedané, funkcia $plus$ väzme všetky aplikácie nasledovníka $s$ z čísla $m$ a "pripíše" pred číslo $n$.
Príklad
Majme daný následujúci term: $$plus\ \ 1\ \ 2$$ Nájdite jeho normálnu formu.
Riešenie
$$ \begin{array}{lcl} plus\ \ 1\ \ 2 & = & (\lambda m.\lambda n.\lambda s.\lambda z.\ m\ s\ (n\ s\ z))\ \ 1\ \ 2 \to \\ & & (\lambda n.\lambda s.\lambda z.\ 1\ s\ (n\ s\ z))\ \ 2 \to \\ & & \lambda s.\lambda z.\ \underline{1\ s}\ (2\ s\ z) = \\ & & \lambda s.\lambda z.\ \underline{(\lambda s. \lambda z. \ s \ z)\ s}\ (2\ s\ z) \to \\ & & \lambda s.\lambda z.\ (\lambda z. \ s \ z)\ (\underline{2\ s}\ z) = \\ & & \lambda s.\lambda z.\ (\lambda z. \ s \ z)\ (\underline{(\lambda s. \lambda z. \ s \ (s \ z))\ s}\ z) \to \\ & & \lambda s.\lambda z.\ (\lambda z. \ s \ z)\ (\underline{(\lambda z. \ s \ (s \ z))\ \ z}) \to \\ & & \lambda s.\lambda z.\ \underline{(\lambda z. \ s \ z)\ (s \ (s \ z))} \to \\ & & \lambda s.\lambda z.\ s\ (s \ (s \ z)) = 3 \\ \end{array} $$
Násobenie Churchových čı́sel
Násobenie Churchových čísel je možné definovať ako funkciu dvoch premenných:
$$times = \lambda m.\lambda n.\ m\ (plus\ n)\ 0$$
V tomto zápise je Churchove číslo $m$ násobené Churchovým číslom $n$.
Je potrebné si uvedomiť, že táto funkcia definuje násobenie ako $m$-krát pripočítanie $n$ k nule.
$$m * n = n + n + ... + n + 0 \quad \quad \quad (m \text{ krát prirátané} n \text{ k nule})$$
Poznámka
Pre definíciu nových funkcií je možné využiť už existujúce funkcie. Napríklad v tomto prípade pri definícii funkcie $times$ bola využitá už pred tým definovaná funkcia $plus$.
Príklad
Majme daný následujúci term: $$times\ \ 1\ \ 2$$ Nájdite jeho normálnu formu.
Riešenie
$$ \begin{array}{lcl} times\ \ 1\ \ 2 & = & (\lambda m.\lambda n.\ m\ (plus\ n)\ 0)\ \ 1\ \ 2 \to \\ & & (\lambda n.\ 1\ (plus\ n)\ 0)\ \ 2 \to \\ & & 1\ (plus\ 2)\ 0 = \\ & & 1\ (\underline{(\lambda m.\lambda n.\lambda s.\lambda z.\ m\ s\ (n\ s\ z))\ 2})\ 0 \to \\ & & 1\ (\lambda n.\lambda s.\lambda z.\ 2\ s\ (n\ s\ z))\ 0 = \\ & & 1\ (\lambda n.\lambda s.\lambda z.\ \underline{(\lambda s. \lambda z.\ s\ (s\ z))\ s}\ (n\ s\ z))\ 0 \to \\ & & 1\ (\lambda n.\lambda s.\lambda z.\ \underline{(\lambda z.\ s\ (s\ z))\ (n\ s\ z)})\ 0 \to \\ & & \underline{1\ (\lambda n.\lambda s.\lambda z.\ s\ (s\ (n\ s\ z)))}\ 0 = \\ & & \underline{(\lambda s. \lambda z.\ s\ z)\ (\lambda n.\lambda s.\lambda z.\ s\ (s\ (n\ s\ z)))}\ 0 \to \\ & & \underline{(\lambda z.\ (\lambda n.\lambda s.\lambda z.\ s\ (s\ (n\ s\ z)))\ z)\ \ 0} \to \\ & & \underline{(\lambda n.\lambda s.\lambda z.\ s\ (s\ (n\ s\ z)))\ 0 } \to \\ & & \lambda s.\lambda z.\ s\ (s\ (0\ s\ z)) = \\ & & \lambda s.\lambda z.\ s\ (s\ (\underline{(\lambda s. \lambda z. z)\ s}\ z)) \to \\ & & \lambda s.\lambda z.\ s\ (s\ (\underline{(\lambda z. z)\ z})) \to \\ & & \lambda s.\lambda z.\ s\ (s\ z) = 2 \\ \end{array} $$
Ďalšie funkcie
Funkcia nasledovníka (successor): $$ succ = \lambda n . \lambda s . \lambda z. s\ (n\ s\ z) $$
Funkcia predchodcu (predecessor): $$ pred = \lambda m . f\ st\ (m\ ss\ zz) $$ pričom $$ zz = pair\ 0\ 0 $$ $$ ss = \lambda p . pair\ (snd\ p)\ (plus\ 0\ (snd\ p)) $$
Funkcia iszero testu na nulu: $$ iszero = \lambda m . m\ (\lambda x.\ false)\ true $$
Funkcia pre test, či sú dve čísla rovnaké: $$ equal = \lambda m . \lambda n . and\ (iszero\ (m\ pred\ n))\ (iszero\ (n\ pred\ m)) $$
Príklad
Majme daný následujúci term: $$iszero\ \ 1$$ Nájdite jeho normálnu formu.
Riešenie
$$ \begin{array}{lcl} iszero\ \ 1 & = & (\lambda m . m\ (\lambda x.\ false)\ true)\ \ 1 \to \\ & & 1\ (\lambda x.\ false)\ true = \\ & & (\lambda s. \lambda z.\ s\ z)\ (\lambda x.\ false)\ true \to \\ & & (\lambda z.\ (\lambda x.\ false)\ z)\ \ true \to \\ & & (\lambda x.\ false)\ \ true \to \\ & & false \end{array} $$
Poznámka
Z dôvodu, že jazyk OCaml je staticky a silne typovaný, nie je možné v ňom jednoducho demonštrovať definíciu Churchových čísel ako $\lambda$-termov.
Rekurzia v $\lambda$-kalkule
Možnosť definovať rekurzívne funkcie je dnes štandardnou súčasťou populárnych programovacích jazykov. Umožňujú výrazne skrátiť text programu, zlepšiť jeho prehľadnosť a často aj časovú či algoritmickú zložitosť.
Funkcia môže byť rekurzívna:
- Priamo - ak volá samu seba.
- Nepriamo (z ang. mutually recursive) - ak volá samu seba prostredníctvom inej funkcie, ktorá ju volá.
Poznámka
Ak rekurzívne funkcie:
- poskytnú výsledok - konvergujú,
- neposkytnú výsledok - divergujú.
Príklad
Rekurzívna definícia funkcie faktoriál v programovacom jazyku OCaml (priama rekurzia):
let rec factorial n =
if n = 0 then 1 (* Základný prípad: n=0 *)
else n * factorial (n - 1) (* Rekurzívny prípad: n >= 0, rekurzívne volanie *)
Príklad
Rekurzívna definícia funkcií pre overenie či je číslo parne, resp. nepárnev programovacom jazyku OCaml (nepriama rekurzia):
(* Funkcia na určenie, či je číslo párne *)
let rec is_even n =
if n = 0 then true (* Základný prípad: 0 je párne *)
else is_odd (n - 1) (* Nepriame rekurzívne volanie *)
(* Funkcia na určenie, či je číslo nepárne *)
and is_odd n =
if n = 0 then false (* Základný prípad: 0 nie je nepárne *)
else is_even (n - 1) (* Nepriame rekurzívne volanie *)
Poznámka
Pri definícii rekurzívnej funkcie musí byť v jazyku OCaml explicitne uvedené, že sa jedná o rekurzívnu funkciu - konštrukcia let rec.
Rekurzívne funkcie a fixné body
Rekurzívne funkcie poskytnú výsledok, ak majú fixný bod.
- Fixný bod vypočítame použitím kombinátora fixného bodu.
- Postupujeme tak, že definujeme pomocnú nerekurzívnu funkciu vyššieho rádu $g$, ktorá má rekurzívnu funkciu $f$ ako parameter a vypočítame fixný bod funkcie $g$.
- Hodnotu rekurzívnej funkcie $f$ získame aplikovaním kombinátora fixného bodu na funkciu $g$.
Fixný bod funkcie
Fixný bod funkcie označuje prvok definičného oboru funkcie, ktorý sa zobrazí v obore hodnôt sám do seba.
Formálne, $c$ je fixným bodom funkcie $f$ ak $c$ patrí do definičného oboru aj oboru hodnôt $f$ a platí $$f(c)=c,$$ z čoho je možné odvodiť zaujímavú vlastnosť pri uvažovaní o výpočte rekurzívnych funkcií: $$f(\ f(... f(c)))=c$$
Príklad
Funkcia: $$f(x)=x*x$$ má dva fixné body: $0$ a $1$.
Problém rekurzívnej definície funkcie
Problémom rekurzívnych funkcií je, že sú definované same sebou.
Napríklad majme rekurzívne definovanú funkciu $fakt$ pre výpočet faktoriálu následovne: $$fakt = \lambda n. test\ (iszero\ n)\ 1\ (times\ n\ (fakt\ (pred\ n)))$$
Využitím "čitateľnejšej" notácie jazyka NBL, je možné v infixnej forme prepísať predchádzajúci term následovne: $$fakt = \lambda n.\ if\ n=0\ then\ 1\ else\ n*fakt\ (n-1).$$ Problémom je, že funkcia $fakt$ sa objavuje na pravej aj ľavej strane, čiže sa nejedná o definíciu funkcie ale o rekurzívnu rovnicu.
Odstránenie rekurzie
Problém rekurzívnej definície je možné "obísť" jednoduchým trikom:
Majme rekurzívnu funkciu $f$ aplikovanú na argument $a$. Aplikáciu $f\ a$ je možné prepísať následovne: $$(\lambda g.g\ a)\ f.$$
- Pôvodná rekurzívna funkcia $f$ sa stáva argumentom novej funkcie vyššieho rádu $g$.
- Využitím $g$ namiesto $f$ v definícii rekurzívnej funkcie, je možné nahradiť rekurzívne volanie novou funkciou, ktorá nie je rekurzívna.
Kombinátor fixného bodu
Existuje niekoľko rôznych kombinátorov fixného bodu.
Alan Turing definoval kombinátor fixného bodu ako $\lambda$-term: $$ \Theta = (\lambda x.\lambda y.(y\ (x\ x\ y)))\ (\lambda x.\lambda y.(y\ (x\ x\ y))) $$
Pre netypovaný $\lambda$-kalkul sa najčastejšie používa kombinátor fixného bodu $Y$, ktorý definoval Haskell Curry: $$ Y = \lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x)) $$
Poznámka
Tento kombinátor sa používa pre metódu volania menom (call-by-name), pre metódu volania hodnotou je nevhodný, pretože term $Y\ g$ diverguje pre ľubovoľné $g$.
Z tohto dôvodu budeme využívať zovšeobecnený kombinátor fixného bodu: $$ fix = \lambda f.(\lambda x.f\ (\lambda y.x\ x\ y))\ (\lambda x.f\ (\lambda y.x\ x\ y)), $$ ktorý je vhodný pre redukčnú stratégiu volania hodnotou (call-by-value).
Príklad: rekurzívna funkcia pre výpočet faktoriálu
Pre výpočet rekurzívnej funkcie je potrebné ju vyjadriť ako fixný bod nejakej inej funkcie vyššieho rádu a následne nájsť fixný bod danej funkcie.
Majme opäť funkciu faktoriálu, ktorú opisuje následujúca rekurzívna definícia: $$ faktorial(n)= \begin{cases} 1 \quad \text{ak}~n=0,\\ ~ \\ n*faktorial(n-1) \end{cases} $$ kde $n \in \mathbf{N}$.
Túto rekurzívnu rovnicu je možné definovať ako nasledujúci term (využitím notácie jazyka NBL, kvôli čitateľnosti): $$faktorial = \lambda n.\ if\ n=0\ then\ 1\ else\ n*faktorial\ (n-1).$$
Funkcia faktorial je fixným bodom nasledujúcej funkcie vyššieho rádu: $$g=\lambda fact. \lambda n.\ if\ n=0\ then\ 1\ else\ n*fact\ (n-1)$$
Poznámka
Je potrebné si uvedomiť, že ak $h$ je fixným bodom funkcie $g$, potom $g\ h = h$.
Ak existuje spôsob ako nájsť fixný bod funkcie $g$, potom existuje spôsob ako definovať funkciu $faktorial$. Tento problém riešia kombinátory fixného bodu. To znamená, aplikáciou kombinátora fixného bodu na danú funkciu vyššieho rádu je možné definovať funkciu faktoriálu nasledovne: $$fakt = fix\ \ g.$$
Pre výpočet faktoriálu čísla $n \in \mathbf{N}$, stačí aplikovať funkciu $fakt$ na dané číslo
Príklad
Vypočítajte faktoriál čísla $3$ využitím vyššie definovanej rekurzívnej funkcie.
Riešenie
Funkciu nazveme $fakt$ a aplikujeme ju na argument $3$.
$$ \begin{array}{lcl} fakt\ 3 & = & fix\ g\ 3 = \\ & & \underline{\textcolor{blue}{(\lambda f.(\lambda x.f\ (\lambda y.x\ x\ y))\ (\lambda x.f\ (\lambda y.x\ x\ y)))}\ \ \textcolor{red}{g}}\ \ 3 \to \\ & & (\lambda x.g\ (\lambda y.x\ x\ y))\ \underbrace{(\lambda x.g\ (\lambda y.x\ x\ y))}_{h}\ \ 3 \to \\ & & g\ \underbrace{(\lambda y.h\ h\ y)}_{f}\ \ 3 = \\ & & g\ f\ \ 3 = \\ & & \underline{\textcolor{blue}{(\lambda fact. \lambda n.\ if\ n=0\ then\ 1\ else\ n*fact\ (n-1))}\ \ \textcolor{red}{f}}\ \ 3 \to \\ & & \underline{\textcolor{blue}{(\lambda n.\ if\ n=0\ then\ 1\ else\ n*\textcolor{red}{f}\ (n-1))}\ \ 3} \to \\ & & (if\ 3=0\ then\ 1\ else\ 3*f\ (3-1)) \to \\ & & (if\ false\ then\ 1\ else\ 3*f\ 2) \to \\ & & 3*~~ f\ 2 = \\ & & 3*~~ (\lambda y.h\ h\ y)\ 2 \to \\ & & 3*~~ h\ h\ 2 = \\ & & 3*~~ (\lambda x.g\ (\lambda y.x\ x\ y))\ h\ 2 = \\ & & 3*~~ g\ \underbrace{(\lambda y.h\ h\ y)}_{f}\ 2 = 3*~~ g\ \ f\ \ 2 =\\ & & 3*~~ (\lambda fact. \lambda n.\ if\ n=0\ then\ 1\ else\ n*fact\ (n-1))\ \ f \ \ 2 \to \\ & & 3*~~ (\lambda n.\ if\ n=0\ then\ 1\ else\ n*f\ (n-1)) \ \ 2 \to \\ & & 3*~~ if\ 2=0\ then\ 1\ else\ 2*f\ (2-1) \to \\ & & 3*~~ if\ false\ then\ 1\ else\ 2*f\ 1 \to \\ & & 3*2*~~ f\ \ 1 = \\ & & 3*2*~~ (\lambda y.h\ h\ y)\ 1 \to \\ & & 3*2*~~ h\ h\ 1 = \\ & & 3*2*~~ (\lambda x.g\ (\lambda y.x\ x\ y))\ h\ 1 = \\ & & 3*2*~~ g\ \underbrace{(\lambda y.h\ h\ y)}_{f}\ 1 = 3*2*~~ g\ \ f\ \ 1 =\\ & & 3*2*~~ (\lambda fact. \lambda n.\ if\ n=0\ then\ 1\ else\ n*fact\ (n-1))\ \ f \ \ 1 \to \\ & & 3*2*~~ (\lambda n.\ if\ n=0\ then\ 1\ else\ n*f\ (n-1)) \ \ 1 \to \\ & & 3*2*~~ if\ 1=0\ then\ 1\ else\ 1*f\ (1-1) \to \\ & & 3*2*~~ if\ false\ then\ 1\ else\ 1*f\ 0 \to \\ & & 3*2*1*~~ f\ 0 \to \\ & & 3*2*1*~~ (\lambda y.h\ h\ y)\ 0 \to \\ & & 3*2*1*~~ h\ h\ 0 = \\ & & 3*2*1*~~ (\lambda x.g\ (\lambda y.x\ x\ y))\ h\ 0 = \\ & & 3*2*1*~~ g\ \underbrace{(\lambda y.h\ h\ y)}_{f}\ 0 = 3*2*1*~~ g\ \ f\ \ 0 =\\ & & 3*2*1*~~ (\lambda fact. \lambda n.\ if\ n=0\ then\ 1\ else\ n*fact\ (n-1))\ \ f \ \ 0 \to \\ & & 3*2*1*~~ (\lambda n.\ if\ n=0\ then\ 1\ else\ n*f\ (n-1)) \ \ 0 \to \\ & & 3*2*1*~~ if\ 0=0\ then\ 1\ else\ 1*f\ (0-1) \to \\ & & 3*2*1*~~ if\ true\ then\ 1\ else\ 1*f\ 0 \to \\ & & 3*2*1*1 = 6 \\ \end{array} $$
Poznámka
Term získaný v tretom kroku vyhodnotenia: $$f = \lambda y.h\ h\ y,$$ je fixným bodom funkcie $g$, t.j.: $$g\ f = f.$$ Následne aplikácia $f$ na argument $n$ sa vyhodnotí na $g\ f\ n$: $$f\ n \to^* g\ f\ n.$$ Týmto trikom je získaná rekurzia, ktorá sa ukončí v prípade, že funkcia $g$ ma v sebe podmienku na základe ktorej je možné "vyskočiť" z rekurzie.
Zdroje
- Pierce, Benjamin C. Types and programming languages. MIT press, Cambridge, 2001 (Перевод на русский язык: Бенджамин Пирс. Типы в языках программирования. — Добросвет, 2012. — ISBN 978-5-7913-0082-9)
- Pierce, Benjamin C et al.: Software Foundations, Electronic textbook, 2024
- Lecture notes, CS 152: Programming Languages, Harvard University, 2024
- Lecture notes, CS242: Programming Languages, Stanford University, 2024
- Valerie Novitzká, Daniel Mihályi: Teória typov, TU Košice, 2015