Teória typov

$\lambda$-kalkul: Churchove kódovanie, Rekurzia

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.

Haskell Curry

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

Pomocou už definovaných Churchových čísel a kombinátorov je možné definovať ďalšie funkcie nad prirodzenými číslami. Pri ich definícii je možné využívať už existujúce kombinátory a skladať z nich zložitejšie operácie.

Funkcia nasledovníka (successor) pre Churchovo číslo $n$ vráti Churchovo číslo $n+1$:

$$ succ = \lambda n . \lambda s . \lambda z. s\ (n\ s\ z) $$

  • Churchovo číslo $n$ aplikuje funkciu $s$ práve $n$-krát na hodnotu $z$.
  • Funkcia $succ$ pridá ešte jednu aplikáciu funkcie $s$.
  • Výsledkom je preto Churchovo číslo reprezentujúce hodnotu $n+1$.

Napríklad: $$ succ\ 2 \to^* \lambda s.\lambda z.\ s\ (s\ (s\ z)) = 3 $$

Funkcia predchodcu (predecessor) pre Churchovo číslo $m$ vráti jeho predchodcu:

$$ pred = \lambda m .\ fst\ (m\ ss\ zz) $$

Definícia funkcie $pred$ využíva dva pomocné kombinátory $zz$ a $ss$.

Počiatočná hodnota $zz$ je dvojica núl:

$$ zz = pair\ 0\ 0 $$

Pomocná funkcia $ss$ transformuje dvojicu tak, že jej druhá hodnota sa stane prvou hodnotou novej dvojice a druhá hodnota sa zvýši o jedna:

$$ ss = \lambda p .\ pair\ (snd\ p)\ (succ\ (snd\ p)) $$

To znamená, že postupnou aplikáciou $ss$ dostávame:

$$ pair\ 0\ 0 \to pair\ 0\ 1 \to pair\ 1\ 2 \to pair\ 2\ 3 \to \ldots $$

Churchovo číslo $m$ vo výraze

$$ m\ ss\ zz $$

spôsobí $m$-násobnú aplikáciu funkcie $ss$ na počiatočnú hodnotu $zz$.

Napríklad pre $m=3$:

$$ 3\ ss\ zz \to^* pair\ 2\ 3 $$

Funkcia $fst$ následne vyberie prvú hodnotu dvojice:

$$ fst\ (pair\ 2\ 3) \to^* 2 $$

a teda:

$$ pred\ 3 \to^* 2 $$

Týmto spôsobom je možné získať predchodcu bez potreby priameho "odstránenia" jednej aplikácie nasledovníka z Churchovho čísla.

Funkcia iszero pre test na nulu je definovaná následovne:

$$ iszero = \lambda m . m\ (\lambda x.\ false)\ true $$

  • Churchovo číslo $m$ určuje počet aplikácií funkcie $(\lambda x.false)$ na počiatočnú hodnotu $true$.
  • Ak $m=0$, funkcia sa neaplikuje ani raz a výsledkom zostane $true$.
  • Ak $m>0$, funkcia sa aplikuje aspoň raz a výsledkom bude $false$.

Preto platí:

$$ iszero\ 0 \to^* true $$

a pre každé $n>0$:

$$ iszero\ n \to^* false $$

Funkciu pre test, či sú dve čísla rovnaké je možné definovať využitím už definovaných kombinátorov $pred$, $iszero$ a $and$:

$$ equal = \lambda m . \lambda n . and\ (iszero\ (m\ pred\ n))\ (iszero\ (n\ pred\ m)) $$

V tomto prípade je opäť využitá vlastnosť Churchových čísel, že číslo $m$ je možné interpretovať ako $m$-násobnú aplikáciu funkcie.

Výraz

$$ m\ pred\ n $$

preto znamená, že funkcia $pred$ je aplikovaná $m$-krát na číslo $n$.

Analogicky:

$$ n\ pred\ m $$

aplikuje funkciu $pred$ $n$-krát na číslo $m$.

Ak sú čísla $m$ a $n$ rovnaké, v oboch prípadoch dostaneme $0$:

$$ m\ pred\ n \to^* 0 $$

$$ n\ pred\ m \to^* 0 $$

Obidve aplikácie funkcie $iszero$ sa preto redukujú na $true$ a následne:

$$ and\ true\ true \to^* true $$

Ak sa čísla nerovnajú, aspoň jeden z uvedených výrazov sa nezredukuje na $0$, a preto výsledkom funkcie $equal$ bude $false$.

Poznámka

Pri definícii uvedených funkcií je využitá dôležitá vlastnosť Churchových čísel. Churchovo číslo $n$ je možné interpretovať nielen ako reprezentáciu prirodzeného čísla, ale aj ako funkciu, ktorá zabezpečí $n$-násobnú aplikáciu inej funkcie na počiatočnú hodnotu.

Napríklad výraz $$n\ f\ x$$ aplikuje funkciu $f$ na hodnotu $x$ práve $n$-krát.

Táto vlastnosť je využitá napríklad vo výrazoch $m\ ss\ zz$ pri definícii predchodcu a $m\ pred\ n$ pri definícii testu rovnosti.

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árne v 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 definície fixného bodu $f(c)=c$ vyplýva, že opakovaná aplikácia funkcie $f$ na jej fixný bod $c$ už hodnotu nemení:

$$ f(c)=c, $$

$$ f(f(c))=f(c)=c, $$

a všeobecne:

$$ f(f(\ldots f(c)))=c. $$

To znamená, že ak sa pri výpočte dostaneme do fixného bodu $c$, každá ďalšia aplikácia funkcie $f$ poskytne opäť tú istú hodnotu $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

Kombinátor $Y$ sa používa pre redukčnú stratégiu volania menom (call-by-name). Pre metódu volania hodnotou (call-by-value) je nevhodný, pretože pred aplikovaním funkcie na argument je potrebné najskôr vyhodnotiť samotný argument. V prípade termu $Y\ g$ toto vedie k nekonečnej redukcii.

Príklad

Majme kombinátor: $$ Y = \lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x)) $$ a aplikujme ho na ľubovoľnú funkciu $g$: $$ Y\ g. $$ Po dosadení definície kombinátora $Y$ dostávame: $$ \begin{array}{lcl} Y\ g &=& (\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x)))\ g \to \\ && (\lambda x.g\ (x\ x))\ (\lambda x.g\ (x\ x)) \to \\ && g\ ((\lambda x.g\ (x\ x))\ (\lambda x.g\ (x\ x))). \end{array} $$

Všimnime si, že argument funkcie $g$ je opäť term: $$ (\lambda x.g\ (x\ x))\ (\lambda x.g\ (x\ x)), $$ ktorý sa redukuje rovnakým spôsobom: $$ g\ ((\lambda x.g\ (x\ x))\ (\lambda x.g\ (x\ x))) \to g\ (g\ ((\lambda x.g\ (x\ x))\ (\lambda x.g\ (x\ x)))) \to \ldots $$

Pri volaní hodnotou je pred aplikáciou $g$ potrebné najskôr vyhodnotiť jej argument. Vyhodnotenie argumentu však vytvorí ďalšiu aplikáciu $g$ s argumentom, ktorý je opäť potrebné vyhodnotiť: $$ g\ (\underline{g\ (\underline{g\ (\ldots)})}). $$ Výpočet sa preto nikdy nedostane k samotnej aplikácii funkcie $g$ a term diverguje.

Pri volaní menom nie je potrebné argument funkcie $g$ vyhodnotiť pred jej aplikáciou. Preto je možné získať: $$ Y\ g \to^* g\ (Y\ g), $$ čo je požadovaná vlastnosť fixného bodu.

Z tohto dôvodu budeme pre redukčnú stratégiu volania hodnotou používať upravený kombinátor $fix$, v ktorom je rekurzívne volanie zabalené do ďalšej $\lambda$-abstrakcie a jeho vyhodnotenie je tým odložené.

Zovšeobecnený kombinátor fixného bodu je vhodný pre redukčnú stratégiu volania hodnotou (call-by-value): $$ fix = \lambda f.(\lambda x.f\ (\lambda y.x\ x\ y))\ (\lambda x.f\ (\lambda y.x\ x\ y)). $$

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

  1. Pierce, Benjamin C. Types and programming languages. MIT press, Cambridge, 2001 (Перевод на русский язык: Бенджамин Пирс. Типы в языках программирования. — Добросвет, 2012. — ISBN 978-5-7913-0082-9)
  2. Pierce, Benjamin C et al.: Software Foundations, Electronic textbook, 2024
  3. Lecture notes, CS 152: Programming Languages, Harvard University, 2024
  4. Lecture notes, CS242: Programming Languages, Stanford University, 2024
  5. Valerie Novitzká, Daniel Mihályi: Teória typov, TU Košice, 2015

Y combinator function. What is it?
© Copyright 2026 KPI FEI TUKE