λ-kalkul: Churchove kódovanie, rekurzia

Programovanie v $\lambda$-kalkule

Netypovaný $\lambda$-kalkul je univerzálny výpočtový model: pri vhodnom kódovaní dokáže vyjadriť každú vypočítateľnú funkciu. Obsahuje iba premenné, abstrakciu a aplikáciu. Ako pomocou týchto troch syntaktických foriem reprezentovať údaje, operácie a rekurziu?

Základnou technikou je Churchovo kódovanie, pri ktorom údaj reprezentujeme jeho správaním pri použití:

• booleovská hodnota vyberie jednu z dvoch možností;
• dvojica odovzdá svoje zložky funkcii, ktorá ich spracuje;
• prirodzené číslo opakuje funkciu daný počet ráz.

Postupne zavedieme funkcie vyššieho rádu, Churchove booleovské hodnoty, dvojice, prirodzené čísla a operácie nad nimi. Na záver vyjadríme rekurziu pomocou Curryho kombinátora $Y$. Všetky tieto konštrukcie zostavíme bez rozšírenia základnej syntaxe $\lambda$-kalkulu.

let id = fun x -> x;;
let id x = x;;

Funkcie vyššieho rádu

Abstrakcia v čistom $\lambda$-kalkule viaže jednu premennú; viacargumentové funkcie preto zapisujeme pomocou vnorených abstrakcií. Funkciu viacerých argumentov môžeme vyjadriť postupnosťou funkcií, z ktorých každá prijme jeden argument a vráti funkciu čakajúcu na ďalší. Funkcia vyššieho rádu prijíma funkciu ako argument alebo vracia funkciu ako výsledok.

Majme term $t$, ktorý môže obsahovať voľné premenné $x$ a $y$. Namiesto dvojargumentového zápisu $\lambda(x,y).t$ použijeme:

$$ f=\lambda x.\lambda y.t. $$

Prvá aplikácia dosadí argument za $x$ a vráti novú funkciu s parametrom $y$. Druhá aplikácia dosadí ďalší argument za $y$. Keďže aplikácia viaže doľava, $f\,u\,v$ znamená $(f\,u)\,v$:

$$ ((\lambda x.\lambda y.t)\,u)\,v \to_\beta (\lambda y.[x\mapsto u]t)\,v \to_\beta [y\mapsto v][x\mapsto u]t. $$

Substitúcia musí zabraňovať zachyteniu voľných premenných. V uvedenom zápise predpokladáme $y\notin FV(u)$; ak to neplatí, najprv vhodne premenujeme viazanú premennú $y$ pomocou $\alpha$-konverzie.

Táto transformácia viacargumentovej funkcie na postupnosť jednoargumentových funkcií sa nazýva currying, podľa Haskella B. Curryho. Jeho meno nesie aj jazyk Haskell.

Kombinátory a používaná notácia

Kombinátor je uzavretý $\lambda$-term, teda term bez voľných premenných. Kombinátorom budeme prideľovať názvy, napríklad:

$$ I=\lambda x.x. $$

Táto rovnosť zavádza metajazykovú skratku. Symbol $I$ nie je novou konštrukciou jazyka; pri redukcii ho môžeme nahradiť jeho definíciou. Zátvorky zachovávajú štruktúru dosadeného termu:

$$ I\,u=(\lambda x.x)\,u\to_\beta u. $$

V príkladoch rozlišujeme:

• $=$ pri zavedení alebo rozvinutí skratky, prípadne pri doplnení zátvoriek;
• $\to_\beta$ pre jeden krok všeobecnej $\beta$-redukcie;
• $\to_\beta^*$ pre nula alebo viac takýchto krokov;
• $=_\beta$ pre $\beta$-ekvivalenciu, ktorá pripúšťa redukcie aj ich opačné kroky; termy porovnávame až na premenovanie viazaných premenných.

Predchádzajúca prednáška zaviedla sémantiku volania hodnotou. Tu pri odvodeniach používame všeobecnú $\beta$-redukciu, ktorá dovoľuje redukovať aj pod abstrakciami. Uvedené kroky preto nie sú automaticky krokmi volania hodnotou ani presným sledom normálneho poradia.

Normálne poradie v každom kroku vyberie najľavejší vonkajší redex, argument pred substitúciou nevyhodnotí a pokračuje aj pod abstrakciami. Ak $\beta$-normálna forma existuje, nájde ju. Volanie menom je tiež nestriktné, ale pod abstrakcie nevstupuje. Preto môže skončiť na abstrakcii, ktorej telo ešte obsahuje redexy. Pri získavaní úplného normálneho tvaru Churchových výsledkov môžeme použiť normálne poradie.

Churchove booleovské hodnoty ako kombinátory

V čistom $\lambda$-kalkule nie sú vstavané pravdivostné konštanty. Ich základným použitím je výber medzi dvoma možnosťami. Pravdu preto reprezentujeme funkciou, ktorá vráti prvý argument, a nepravdu funkciou, ktorá vráti druhý:

$$ \begin{aligned} true &=\lambda x.\lambda y.x,\\ false&=\lambda x.\lambda y.y. \end{aligned} $$

Ide o kombinátory s charakteristickým správaním:

$$ true\,u\,v\to_\beta^*u, \qquad false\,u\,v\to_\beta^*v. $$

Podmienené vetvenie vyjadríme kombinátorom:

$$ test=\lambda b.\lambda t.\lambda e.b\,t\,e. $$

Kombinátor $test$ odovzdá obe možnosti booleovskej hodnote $b$. Samotná hodnota následne vyberie prvú alebo druhú možnosť. Zamýšľané správanie platí pre Churchove booleovské hodnoty; ľubovoľný iný term nemusí byť zmysluplnou podmienkou.

let tru  = fun x -> fun y -> x;;
let fls  = fun x -> fun y -> y;;
let test = fun b -> fun t -> fun e -> b t e;;

Booleovské operácie

Konjunkciu, disjunkciu a negáciu definujeme pomocou výberového správania Churchových hodnôt:

$$ \begin{aligned} and&=\lambda b.\lambda c.b\,c\,false,\\ or &=\lambda b.\lambda c.b\,true\,c,\\ not&=\lambda b.b\,false\,true. \end{aligned} $$

Pri konjunkcii pravdivé $b$ vyberie hodnotu $c$, zatiaľ čo nepravdivé $b$ vyberie $false$. Pri disjunkcii pravdivé $b$ vyberie $true$ a nepravdivé $b$ vyberie $c$. Negácia vymení poradie oboch možností.

Napríklad:

$$ and\,false\,true\to_\beta^*false, \qquad not\,true\to_\beta^*false. $$

V OCaml použijeme názvy, ktoré sa neprekrývajú s kľúčovými slovami:

let andb = fun a -> fun b -> a b fls;;
let orb  = fun a -> fun b -> a tru b;;
let negb = fun a -> a fls tru;;

Churchove dvojice

Dvojicu reprezentujeme funkciou, ktorá uchová dve zložky a odovzdá ich prijatému selektoru. Ako selektory na získanie zložiek použijeme $true$ a $false$:

$$ \begin{aligned} pair&=\lambda a.\lambda b.\lambda s.s\,a\,b,\\ fst &=\lambda p.p\,true,\\ snd &=\lambda p.p\,false. \end{aligned} $$

Aplikácia $pair\,u\,v$ vytvorí reprezentáciu dvojice. Projekcia $fst$ vyberie jej prvú zložku a projekcia $snd$ druhú.

Priame funkcie v OCaml môžeme zapísať takto:

let pair   = fun a -> fun b -> fun s -> s a b;;
let first  = fun p -> p tru;;
let second = fun p -> p fls;;

Churchove čísla ako kombinátory

Prirodzené číslo $n$ reprezentujeme ako iterátor: funkciu, ktorá aplikuje ľubovoľnú funkciu $s$ práve $n$-krát na počiatočnú hodnotu $z$.

Churchove termy odlišujeme tučným zápisom $\mathbf{0},\mathbf{1},\ldots$ od prirodzených čísel metajazyka. Používame $\mathbb{N}$ vrátane nuly:

$$ \begin{aligned} \mathbf{0}&=\lambda s.\lambda z.z,\\ \mathbf{1}&=\lambda s.\lambda z.s\,z,\\ \mathbf{2}&=\lambda s.\lambda z.s\,(s\,z),\\ \mathbf{3}&=\lambda s.\lambda z.s\,(s\,(s\,z)),\\ &\vdots \end{aligned} $$

Všeobecne $\mathbf{n}=\lambda s.\lambda z.s^n(z)$, kde $s^0(z)=z$ a $s^{n+1}(z)=s(s^n(z))$. Zápis $s^n(z)$ je metajazyková skratka za vnorené aplikácie, nie ďalší operátor $\lambda$-kalkulu. Preto:

$$ \mathbf{n}\,s\,z\to_\beta^*s^n(z). $$

Táto vlastnosť nám umožní použiť číslo ako počet krokov výpočtu, napríklad pri násobení alebo pri transformácii dvojice.

Sčítanie Churchových čísel

Sčítanie definujeme kombinátorom:

$$ plus=\lambda m.\lambda n.\lambda s.\lambda z.m\,s\,(n\,s\,z). $$

Parametre $m$ a $n$ očakávajú Churchove čísla. Vnútorný term $n\,s\,z$ vytvorí iterácie podľa čísla $n$; term $m\,s$ pridá ďalšie iterácie. Výsledkom je opäť funkcia parametrov $s$ a $z$:

$$ plus\,\mathbf{m}\,\mathbf{n}\to_\beta^*\mathbf{m+n}. $$

Násobenie Churchových čísel

Násobenie vyjadríme opakovaným sčítaním:

$$ times=\lambda m.\lambda n.m\,(plus\,n)\,\mathbf{0}. $$

Churchovo číslo $m$ aplikuje funkciu $plus\,n$ na Churchovu nulu príslušný počet ráz. Výsledkom je číslo reprezentujúce súčin:

$$ times\,\mathbf{m}\,\mathbf{n}\to_\beta^*\mathbf{mn}. $$

Ďalšie funkcie

Z už zavedených kombinátorov môžeme zostaviť nasledovníka, predchodcu, test na nulu a test rovnosti.

Nasledovník pridá jednu aplikáciu funkcie $s$:

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

Napríklad $succ\,\mathbf{2}\to_\beta^*\mathbf{3}$.

Predchodcu získame iteráciou dvojice, ktorá uchováva aktuálne číslo a číslo o jeden krok pozadu. Zavedieme počiatočnú dvojicu a krok jej transformácie:

$$ \begin{aligned} zz&=pair\,\mathbf{0}\,\mathbf{0},\\ ss&=\lambda p.pair\,(snd\,p)\,(succ\,(snd\,p)),\\ pred&=\lambda n.fst\,(n\,ss\,zz). \end{aligned} $$

Funkcia $ss$ presunie druhú zložku na prvú pozíciu a na druhú pozíciu vloží jej nasledovníka. Každý ďalší stav preto vzniká novou aplikáciou $ss$:

$$ \begin{aligned} zz&=pair\,\mathbf{0}\,\mathbf{0},\\ ss\,zz&\to_\beta^*pair\,\mathbf{0}\,\mathbf{1},\\ ss\,(ss\,zz)&\to_\beta^*pair\,\mathbf{1}\,\mathbf{2},\\ ss\,(ss\,(ss\,zz))&\to_\beta^*pair\,\mathbf{2}\,\mathbf{3}. \end{aligned} $$

Samotná dvojica sa na ďalší stav nemení redukciou; potrebujeme na ňu aplikovať $ss$. Churchovo číslo určí počet takýchto aplikácií. Napríklad:

$$ \begin{aligned} pred\,\mathbf{3} &\to_\beta fst\,(\mathbf{3}\,ss\,zz)\\ &\to_\beta^*fst\,(ss\,(ss\,(ss\,zz)))\\ &\to_\beta^*fst\,(pair\,\mathbf{2}\,\mathbf{3})\\ &\to_\beta^*\mathbf{2}. \end{aligned} $$

Na nule je predchodca orezaný: výsledkom zostáva nula, nie záporné číslo. Bez vykonania kroku $ss$ projekcia vyberie prvú nulu:

$$ pred\,\mathbf{0} \to_\beta^*fst\,zz =fst\,(pair\,\mathbf{0}\,\mathbf{0}) \to_\beta^*\mathbf{0}. $$

Všeobecne $pred\,\mathbf{n}\to_\beta^*\mathbf{\max(n-1,0)}$.

Test na nulu využije rozdiel medzi nulovým a kladným počtom iterácií:

$$ iszero=\lambda n.n\,(\lambda x.false)\,true. $$

Nula funkciu $\lambda x.false$ nepoužije a ponechá počiatočnú hodnotu $true$. Kladné číslo ju použije aspoň raz, takže výsledkom je $false$:

$$ iszero\,\mathbf{0}\to_\beta^*true, \qquad iszero\,\mathbf{n}\to_\beta^*false\quad\text{pre }n>0. $$

Rovnosť overíme orezaným odčítaním v oboch smeroch:

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

Výraz $m\,pred\,n$ opakuje predchodcu podľa čísla $m$, začínajúc číslom $n$. Pre Churchove vstupy tak reprezentuje $\max(n-m,0)$. Druhý výraz reprezentuje $\max(m-n,0)$. Oba výsledky sú nulové práve vtedy, keď sú vstupy rovnaké.

Napríklad:

$$ \begin{aligned} equal\,\mathbf{2}\,\mathbf{2} &\to_\beta^*and\,(iszero\,\mathbf{0})\,(iszero\,\mathbf{0})\\ &\to_\beta^*and\,true\,true\\ &\to_\beta^*true. \end{aligned} $$

Pri vstupoch $\mathbf{2}$ a $\mathbf{3}$ prvé odčítanie poskytne $\mathbf{1}$ a druhé $\mathbf{0}$, preto $equal\,\mathbf{2}\,\mathbf{3}\to_\beta^*false$.

Churchove čísla v OCaml

Základné Churchove čísla aj sčítanie možno zapísať priamo ako funkcie OCaml:

let zero s z = z;;
let one s z = s z;;
let two s z = s (s z);;
let plus m n s z = m s (n s z);;
let to_int n = n (fun x -> x + 1) 0;;

to_int (plus one two);;  (* Výsledok: 3 *)

Základné Churchove kódovania možno v OCaml zapísať priamo ako funkcie. Pri dekódovaní v uvedenom príklade používame aritmetiku OCaml.

Nie každý term netypovaného $\lambda$-kalkulu však možno takto priamo preniesť: niektoré termy nie sú typovateľné v typovom systéme OCaml. Volanie hodnotou môže navyše viesť k inému priebehu vyhodnotenia než nestriktné stratégie $\lambda$-kalkulu.

Rekurzia v $\lambda$-kalkule

Churchovo číslo umožňuje iterovať funkciu vopred určený počet ráz. Pri všeobecnej rekurzii sa však telo funkcie odvoláva na funkciu samotnú. V OCaml takýto odkaz umožňuje konštrukcia let rec:

let rec factorial n =
  if n = 0 then 1
  else n * factorial (n - 1);;

Príklad predpokladá nezáporný vstup. Priama rekurzia volá tú istú funkciu; vzájomná rekurzia vedie cez ďalšie funkcie späť k pôvodnej. V čistom $\lambda$-kalkule nemáme let rec ani mená funkcií, ktoré by automaticky odkazovali na vlastnú definíciu. Rekurziu preto musíme zostaviť iba pomocou abstrakcie a aplikácie.

Oddelíme telo výpočtu od mechanizmu rekurzie: najprv nahradíme rekurzívny odkaz parametrom funkcie vyššieho rádu a potom jej poskytneme vhodný fixný bod.

Fixný bod funkcie

Nech $F:A\to A$ je funkcia. Prvok $c\in A$ je jej fixným bodom, ak:

$$ F(c)=c. $$

Napríklad funkcia $F(x)=x^2$ na reálnych číslach má fixné body $0$ a $1$. Ďalšia aplikácia na fixný bod nemení výsledok: $F(F(c))=F(c)=c$.

V $\lambda$-kalkule rovnosť vyjadríme pomocou $\beta$-ekvivalencie. Term $p$ je fixným bodom termu $G$, ak:

$$ G\,p=_\beta p. $$

Fixný bod umožňuje vyjadriť rekurzívny odkaz. Nezaručuje ukončenie výpočtu: konvergencia alebo divergencia závisí aj od tela funkcie, vstupu a redukčnej stratégie.

Od rekurzívnej rovnice k nerekurzívnemu telu

Bežná matematická definícia faktoriálu pre $n\in\mathbb{N}$ je:

$$ \operatorname{fact}(n)= \begin{cases} 1,&n=0,\\ n\cdot\operatorname{fact}(n-1),&n>0. \end{cases} $$

Je to špecifikácia požadovaného správania. Pomocou Churchových kombinátorov by sme ju mohli zapísať ako rekurzívnu rovnicu:

$$ fact=_\beta\lambda n. test\,(iszero\,n)\,\mathbf{1}\, (times\,n\,(fact\,(pred\,n))). $$

Tento zápis ešte nedefinuje uzavretý $\lambda$-term: meno $fact$ na pravej strane nie je viazané. Rovnica teda neurčuje metajazykovú skratku, ktorú by sme mohli konečným rozvinutím nahradiť termom bez vlastného mena.

Budúce rekurzívne volanie nahradíme parametrom $f$ a získame:

$$ G=\lambda f.\lambda n. test\,(iszero\,n)\,\mathbf{1}\, (times\,n\,(f\,(pred\,n))). $$

Po rozvinutí už definovaných Churchových kombinátorov je $G$ uzavretý term. Nie je rekurzívny: neodkazuje na vlastné meno. Parameter $f$ zastupuje funkciu použitú pri ďalšom volaní. Hľadáme term $p$, pre ktorý $G\,p=_\beta p$; ten bude spĺňať požadovanú rekurzívnu rovnicu.

Curryho kombinátor Y

Kombinátor fixného bodu je uzavretý $\lambda$-term $\Phi$, pre ktorý pre každý term $g$ platí:

$$ \Phi\,g=_\beta g\,(\Phi\,g). $$

Term $\Phi\,g$ je teda fixným bodom termu $g$. Konkrétnym príkladom je Curryho kombinátor $Y$:

$$ Y=\lambda f.(\lambda x.f\,(x\,x))(\lambda x.f\,(x\,x)). $$

Je uzavretý a pre každý term $g$ platí:

$$ Y\,g=_\beta g\,(Y\,g). $$

Faktoriál pomocou Y kombinátora

Definícia faktoriálu už nepotrebuje priamy odkaz na vlastné meno:

$$ fact=Y\,G. $$

Po rozvinutí skratiek dostaneme uzavretý $\lambda$-term. Z vlastnosti $Y$ vyplýva $fact=_\beta G\,fact$, teda požadovaná rekurzívna rovnica.

Pre prehľadnosť zaveďme dve metajazykové skratky:

$$ h=\lambda x.G\,(x\,x), \qquad r=h\,h. $$

Skratka $r$ označuje celú sebaaplikáciu, nie novú konštrukciu jazyka. Platí:

$$ fact=Y\,G\to_\beta h\,h=r, \qquad r\,u=(h\,h)\,u\to_\beta G\,(h\,h)\,u=G\,r\,u. $$

Každé použitie $r$ na argument tak znovu vytvorí aplikáciu $G\,r$. Nestriktná stratégia dovolí dosadiť $r$ za parameter $f$ bez nekonečného vyhodnotenia $r$ vopred.

Nasledujúce odvodenia sú didakticky zvolené postupnosti všeobecnej $\beta$-redukcie. Pri rekurzívnych volaniach zvýrazňujeme telo $G$ a nechávame niektoré vonkajšie aritmetické redexy dočasne nerozvinuté. Nejde o presný sled normálneho poradia. Úplný výsledok možno nezávisle získať normalizáciou celého termu normálnym poradím.

Stratégia a ukončenie rekurzie

Volanie menom aj normálne poradie sú nestriktné: umožňujú dosadiť rekurzívny argument bez jeho predchádzajúceho výpočtu a zahodiť nepoužitú vetvu. Volanie menom sa však zastaví na abstrakcii. Na získanie kanonického Churchovho výsledku potrebujeme aj redukciu jej tela, napríklad normálnym poradím. Tento faktoriál s $Y$ preto nevyhodnocujeme volaním hodnotou.

Pre Churchov numerál $\mathbf{n}$ sa pri zvolenej nestriktnej redukcii rekurzívny argument postupne mení na jeho predchodcu. Keďže pre každé $k\in\mathbb{N}$ platí

$$ pred\,\mathbf{k+1}\to_\beta^*\mathbf{k}, $$

po konečnom počte rekurzívnych volaní dosiahneme Churchovu nulu. Vtedy $test$ vyberie základný prípad $\mathbf{1}$ a ďalšie rekurzívne volanie sa zahodí. Zostávajúce Churchove násobenia majú pre tieto konečné numerály normálny tvar.

Samotná prítomnosť základného prípadu však nestačí: rekurzívne volania k nemu musia skutočne smerovať. Kombinátor $Y$ poskytuje mechanizmus rekurzie, nie dôkaz ukončenia.

Pri volaní hodnotou má táto konštrukcia dva problémy: Curryho $Y$ sa rozvíja bez konca a Churchov $test$ by navyše vyhodnotil aj vetvu, ktorá sa napokon nepoužije. Striktná implementácia preto potrebuje kombinátor fixného bodu vhodný pre volanie hodnotou a odložené vetvy, prípadne vstavané if, ktoré vyhodnotí iba vybranú vetvu.

Doplňujúce video: Y combinator function. What is it?

Zdroje

1. Pierce, Benjamin C.: Types and Programming Languages. MIT Press, Cambridge, 2002
2. Pierce, Benjamin C et al.: Software Foundations, Electronic textbook, 2024
3. Lecture notes, CS 152: Programming Languages, Harvard University, jar 2022
4. Lecture notes, CS242: Programming Languages, Stanford University, jeseň 2019
5. Valerie Novitzká, Daniel Mihályi: Teória typov, TU Košice, 2015