Úvod, jazyk NBL, $\lambda$-kalkul

Základné pojmy

Teória typov

• Zaoberá sa štúdiom princípov a vlastností typových systémov.
• Je formálna reprezentácia určitého typového systému.

Typový systém

v informatike je formálny mechanizmus, ktorý určuje typové pravidlá a typové úsudky pre

• zavedenie základných, preddefinovaných typov jazyka a ich operácií,
• popis konštrukcie jednoduchých a zložených typov a ich vlastností,
• formuláciu pravidiel, ktoré priraďujú typy výrazom a hodnotám,
• kontrolu, či program spĺňa dané typové pravidlá (type checking).

Ak má typový systém dokázanú zodpovedajúcu vlastnosť korektnosti (type safety), potom dobre typované programy nevykazujú tie triedy chybného správania, ktoré táto vlastnosť pokrýva. Samotná typová kontrola však nie je dôkazom všeobecnej korektnosti programu.

Typ

• súbor hodnôt, ktoré môžu byť reprezentované v počítači spolu s
• množinou operácií, ktoré sa na nich môžu vykonávať.

Staticky vs dynamicky typované jazyky

• Staticky typované jazyky: typová kontrola sa vykonáva pred spustením programu, zvyčajne počas kompilácie. Typy výrazov a funkcií sa teda overujú bez vykonania programu, čo poskytuje skorú spätnú väzbu a zachytí triedy chýb pokryté daným typovým systémom.

• Dynamicky typované jazyky: informácia o type a kontrola prípustnosti operácií sa viaže predovšetkým na hodnoty počas behu programu. Premenná môže v závislosti od jazyka v rozličných okamihoch obsahovať hodnoty rozličných typov. Takéto typovanie poskytuje flexibilitu, ale niektoré typové chyby sa prejavia až pri behu programu.

Silno vs slabo typované jazyky

• Pojmy silné typovanie a slabé typovanie nemajú jedinú všeobecne prijatú formálnu definíciu. Ide o neformálne klasifikácie a ich presný význam sa medzi autormi líši. Zvyčajne opisujú, do akej miery jazyk bráni miešaniu nekompatibilných hodnôt alebo obchádzaniu typových pravidiel.

• Implicitné konverzie (coercions) s touto diskusiou súvisia a niektorí autori ich považujú za prejav slabšieho typovania. Samy osebe však nepredstavujú presnú definíciu slabého typovania.

Toto delenie je nezávislé od delenia na statické a dynamické typovanie: prvé neformálne charakterizuje prísnosť typových pravidiel, druhé určuje, kedy a nad čím sa typová kontrola vykonáva.

Implicitne vs explicitne typované jazyky

• Implicitne typované jazyky: umožňujú prekladaču odvodzovať typy bez nutnosti, aby ich programátor vyjadroval explicitne.

• Explicitne typované jazyky: naopak vyžadujú, aby programátor určil typy premenných jasne, čím sa zvyšuje čitateľnosť kódu, ale aj zložitosť jeho písania.

Úvod do teórie typov a výpočtových modelov

Teória typov nevznikla iba ako súčasť programovacích jazykov. Jej korene siahajú k otázkam o základoch matematiky: ktoré výrazy sú zmysluplné, ako možno bezpečne vytvárať množiny a ako zabrániť vzniku logických kontradikcií.

Začneme Russellovým paradoxom, ktorý priamo ukazuje, čo sa môže stať pri neobmedzenom vytváraní množín. Následne vysvetlíme, ako typová hierarchia zabráni vytvoreniu problematického výrazu. V druhej časti úvodu prejdeme od otázky, ktoré výrazy sú prípustné, k otázke, ktoré funkcie a problémy sú algoritmicky vypočítateľné.

Naivné vytváranie množín

V naivnej teórii množín sa predpokladalo, že každá dostatočne opísaná vlastnosť $P(x)$ určuje množinu všetkých objektov, ktoré túto vlastnosť spĺňajú: $$ \{x\mid P(x)\}. $$

Zápis $x\in A$ znamená, že objekt $x$ patrí do množiny $A$; zápis $x\notin A$ znamená, že do nej nepatrí.

Takéto vytváranie množín pôsobí prirodzene. Problém vznikne, keď vlastnosť $P(x)$ hovorí o tom, či objekt $x$ patrí do seba samého.

Russellov paradox

Definícia (Russellova množina): Uvažujme kolekciu všetkých množín, ktoré nie sú prvkami seba samých: $$ R=\{x\mid x\notin x\}. $$

Ak by naivné pravidlo vytvárania množín platilo bez obmedzení, potom by aj $R$ bola množinou. Položme preto otázku, či platí $R\in R$, a rozoberieme obe možnosti:

1. Ak $R\in R$, potom je $R$ prvkom množiny $R$. Podľa definície však do $R$ patria iba množiny, ktoré nie sú prvkami seba samých. Musí teda platiť $R\notin R$.
2. Ak $R\notin R$, potom $R$ spĺňa podmienku vstupu do množiny $R$. Musí teda platiť $R\in R$.

V oboch prípadoch predpoklad vedie k svojmu opaku: $$ R\in R\iff R\notin R. $$ Symbol $\iff$ čítame „práve vtedy, keď“. Uvedená ekvivalencia je kontradikciou: tvrdenie $R\in R$ by muselo byť súčasne pravdivé aj nepravdivé.

Russellovo riešenie: teória typov

Definícia (typová hierarchia): Typová hierarchia rozdeľuje objekty do úrovní:

1. na najnižšej úrovni sú jednotlivé objekty,
2. na vyššej úrovni sú množiny týchto objektov,
3. na ďalšej úrovni sú množiny takýchto množín,
4. podobne možno pokračovať do ďalších úrovní.

Množina môže obsahovať iba objekty vhodného, nižšieho typu. Ak má objekt $x$ typ $\tau$, potom množina $A$, do ktorej môže patriť, má typ množiny prvkov typu $\tau$. Tento typ označíme $\operatorname{Set}(\tau)$: $$ x:\tau,\qquad A:\operatorname{Set}(\tau). $$ Výraz $x\in A$ je korektný iba vtedy, keď typy $x$ a $A$ zodpovedajú tomuto pravidlu.

Súvislosti s programovacími jazykmi

Rovnakú ochrannú úlohu majú typové systémy programovacích jazykov. Ak sa program pokúsi použiť hodnotu v operácii, ktorá nie je pre jej typ definovaná, typová kontrola môže program odmietnuť ešte pred jeho spustením.

Historická poznámka

Bertrand Russell objavil paradox, ktorý dnes nesie jeho meno, v roku 1901 pri práci na knihe The Principles of Mathematics. Kniha vyšla v roku 1903 a v prílohe B s názvom The Doctrine of Types Russell predstavil svoju prvú verziu teórie typov.

Russell teóriu ďalej rozvinul, okrem iného v článku Mathematical Logic as Based on the Theory of Types z roku 1908. Spolu s Alfredom Northom Whiteheadom potom vytvoril rozsiahle dielo Principia Mathematica. Jeho tri zväzky vyšli postupne v rokoch 1910, 1912 a 1913. Cieľom diela bolo vybudovať veľkú časť matematiky na presnom logickom základe; autori v ňom použili rozvinutejšiu, rozvetvenú teóriu typov.

Od základov matematiky k otázke vypočítateľnosti

Russellov paradox ukázal, že pri budovaní matematiky nestačí iba intuitívne pracovať s množinami. Je potrebné presne určiť, ktoré výrazy sú prípustné a podľa akých pravidiel možno z daných predpokladov odvodzovať nové tvrdenia. Teória typov bola jedným zo spôsobov, ako takéto obmedzenia zaviesť.

Keď sú však jazyk a pravidlá formálneho systému presne určené, vzniká ďalšia otázka: možno postup dokazovania úplne mechanizovať? Inými slovami, môže existovať algoritmus, ktorý dostane logickú formulu a vždy rozhodne, či je platná?

Práve túto otázku vyjadruje Entscheidungsproblem. Jeho skúmanie viedlo k potrebe matematicky definovať pojem algoritmu a následne k vzniku formálnych výpočtových modelov, ako sú Turingov stroj, rekurzívne funkcie a $\lambda$-kalkul.

Entscheidungsproblem

Entscheidungsproblem (problém rozhodnuteľnosti) sa pýta, či existuje algoritmus, ktorý pre ľubovoľnú formulu logiky prvého rádu v konečnom čase rozhodne, či je logicky platná. Tento problém bol formulovaný v roku 1928 Davidom Hilbertom a Wilhelmom Ackermannom, vychádzajúc z práce Bertranda Russella.

Výpočtové modely

Predtým, ako bolo možné odpovedať na otázku, ktorú formuloval Entscheidungsproblem, bolo potrebné formálne definovať, čo je vypočítateľná funkcia, algoritmus a výpočtový model, ktorý by vedel daný algoritmus aplikovať na matematické tvrdenia.

Výpočtový model je formálny model, ktorý slúži na opis toho, ako je možné vykonať výpočet, to znamená ako je vypočítaný výstup danej matematickej funkcie vzhľadom na daný vstup. Ide o matematickú abstrakciu, ktorá nám umožňuje skúmať rôzne aspekty výpočtov, ako sú rýchlosť, efektivita, zložitosť a limity toho, čo je možné vypočítať.

Čo znamená, že funkcia $$f: \mathbb{N} \to \mathbb{N}$$ je vypočítateľná?

Neformálne, funkcia je vypočitateľná, ak je možné za pomoci pera a papiera vypočítať $f(n)$, pre akékoľvek $n\in \mathbb{N}$.

V 30. rokoch 20. storočia prišli traja výskumníci s tromi rozdielnymi výpočtovými modelmi.

Turingov stroj

V roku 1936 Alan Turing definoval počítač ako Turingov stroj.

• Funkcia je vypočítateľná ak môže byť vypočítaná Turingovým strojom.
• Je to matematický model výpočtu, ktorý pozostáva z:
• nekonečne dlhej pásky rozdelenej na bunky, ktoré môžu obsahovať symboly z určitej abecedy,
• hlavy, ktorá môže čítať alebo zapisovať symboly na páske a pohybovať sa po nej doľava alebo doprava,
• riadiacej jednotky so súborom stavov, ktoré určujú správanie stroja.

Výpočet prebieha podľa prechodovej funkcie, ktorá na základe aktuálneho stavu a prečítaného symbolu určuje nový stav, zápis na pásku a pohyb hlavy.

V roku 1936 Alan Turing dokázal nerozhodnuteľnosť Entscheidungsproblemu prostredníctvom dôkazu problému zastavenia (halting problem).

Čiastočne rekurzívne funkcie

Kurt Gödel významne prispel k formalizácii rekurzívnych funkcií vo svojej práci v oblasti teórie formálnych systémov. Trieda čiastočne rekurzívnych funkcií sa v 30. rokoch sformovala v prácach Herbranda, Gödela a Kleena.

Čiastočne rekurzívne funkcie sú trieda funkcií, ktoré sú definované na prirodzených číslach. Tieto funkcie zahŕňajú tri základné typy operácií:

• Primárna rekurzia - funkcie sú definované rekurzívnym spôsobom, pričom sú založené na jednoducho definovaných funkciách ako napríklad funkcia nuly (vždy vráti nulu) a funkcia nasledovníka (inkrementácia o 1).

• Kompozícia - nové funkcie sú vytvárané zložením iných funkcií.

• Minimizácia (hľadanie minima) - umožňuje definovať funkcie vyhľadávaním najmenšej hodnoty, pre ktorú platí určitá podmienka.

Jedným z cieľov Hilbertovho programu bolo formalizovať matematiku a dokázať konzistentnosť jej formálnych systémov pomocou presne vymedzených, finitných metód. Gödelove vety o neúplnosti z roku 1931 ukázali obmedzenia tohto zámeru v jeho pôvodnej podobe.

• Prvá veta o neúplnosti: Každý konzistentný a efektívne axiomatizovaný formálny systém, ktorý je dostatočne silný na vyjadrenie základnej aritmetiky, je neúplný. Existuje v ňom tvrdenie, pre ktoré v danom systéme nemožno dokázať ani toto tvrdenie, ani jeho negáciu.

• Druhá veta o neúplnosti: Takýto systém, ak je konzistentný, nemôže v rámci vlastných pravidiel dokázať tvrdenie vyjadrujúce jeho vlastnú konzistentnosť.

$\lambda$-kalkul

V rokoch 1929 až 1932 Alonzo Church definoval $\lambda$-kalkul ako formálny systém pre matematickú logiku. Formuloval Churchovu tézu, podľa ktorej sa intuitívne vypočítateľné funkcie zhodujú s funkciami definovateľnými v $\lambda$-kalkule.

Church použil $\lambda$-kalkul na presné vyjadrenie pojmu efektívneho výpočtu. V roku 1936 dokázal, že neexistuje algoritmus, ktorý by pre každú formulu logiky prvého rádu rozhodol, či je logicky platná. Tým podal negatívne riešenie Entscheidungsproblemu. Nejde iba o dôsledok existencie nekonečných výpočtov v $\lambda$-kalkule, ale o výsledok formálneho dôkazu nerozhodnuteľnosti.

Zhrnutie a prechod k formálnym jazykom

Predchádzajúci historický vývoj spája dve základné otázky:

1. Ktoré výrazy sú zmysluplné? Russellov paradox ukázal, že neobmedzené vytváranie množín vedie ku kontradikcii. Teória typov preto zavádza pravidlá, ktoré určujú, ktoré objekty možno navzájom kombinovať a ktoré výrazy sú neprípustné.
2. Čo možno vypočítať algoritmom? Entscheidungsproblem viedol k potrebe presne definovať pojem výpočtu. Rekurzívne funkcie, Turingove stroje a $\lambda$-kalkul poskytli rôzne formálne modely výpočtu, zatiaľ čo výsledky Gödela, Churcha a Turinga ukázali hranice formálneho dokazovania a algoritmického rozhodovania.

Z týchto myšlienok sa postupne vyvinula moderná teória typov. Russellova typová hierarchia priniesla základnú myšlienku, že nie všetky výrazy majú byť prípustné. Neskoršie práce Churcha, Curryho a ďalších prepojili typy s $\lambda$-kalkulom, logikou a programovacími jazykmi. Typové systémy dnes slúžia nielen na zabraňovanie paradoxom, ale aj na opis dát, kontrolu programov a vyjadrovanie vlastností výpočtov.

V ďalšej časti preto začneme jednoduchým netypovaným jazykom NBL. Najskôr na ňom oddelene vysvetlíme syntax, termy, hodnoty a pravidlá vyhodnocovania. Následne prejdeme k netypovanému $\lambda$-kalkulu, v ktorom možno výpočty vyjadrovať pomocou funkcií, ich definovania a aplikácie. Tým si pripravíme základ na neskoršie zavedenie typov, pri ktorom presne ukážeme, ktoré chybné výrazy typový systém vylúči a prečo.

Netypovaný jazyk prirodzených čísel a booleovských hodnôt (NBL)

Pre demonštratívne účely začneme s definíciou jednoduchého netypovaného jazyka prirodzených čísel a booleovských hodnôt (NBL). Tento jazyk obsahuje iba niekoľko syntaktických prvkov, avšak poslúži ako vhodný úvod do netriviálnych konceptov definície programovacích jazykov, ako je abstraktná syntax, induktívne definície, dôkazy, sémantika (vyhodnotenie) a pod.

Dynamickú sémantiku NBL definujeme dvoma spôsobmi. Sémantika malých krokov opisuje jeden elementárny krok výpočtu a zachytáva všetky medzitermy. Sémantika veľkých krokov spája počiatočný term priamo s výslednou hodnotou a medzikroky nezaznamenáva. Na rovnakom príklade ukážeme oba pohľady a neskôr sformulujeme vetu, že pre ukončené vyhodnotenie dávajú rovnaký výsledok.

Základné syntaktické konštrukcie tohto jazyka sú termy.

Term je syntaktická fráza, ktorá reprezentuje výpočet.

Formálna definícia jazyka pozostáva z definície:

• formálnej syntaxe,
• formálnej sémantiky.

Formálna (abstraktná) syntax môže byť definovaná rôznymi spôsobmi, napríklad:

• gramatikou v Backus-Naurovej forme,
• induktívne,
• odvodzovacími pravidlami.

Syntax NBL

Množinu legálnych termov $t$ jazyka nazveme $t \in Term$.

Induktívna definícia syntaxe NBL

Syntax NBL je možné definovať ako najmenšiu množinu $Term$ následovne:

1. $\{true, false, 0 \} \subset Term$,
2. ak $t_1 \in Term$ potom $\{succ\ t_1, pred\ t_1, iszero\ t_1 \} \subset Term$,
3. ak $t_1, t_2, t_3 \in Term$ potom $if\ t_1\ then\ t_2\ else\ t_3 \in Term$.

Slovo najmenšia znamená, že term jazyka NBL nie je možné skonštruovať inak ako pomocou pravidiel 1-3.

Backus–Naurova forma (BNF)

BNF používa na opis syntaxe produkčné pravidlá:

$$t::=\ true\ |\ false\ |\ if\ t\ then\ t\ else\ t\ |\ 0\ |\ succ\ t\ |\ pred\ t\ |\ iszero\ t$$

• $t$ na ľavej strane znamená, že definujeme syntax termov, ktoré všeobecne označujeme $t$,
• $::=$ oddeľuje ľavú a pravú stranu produkčného pravidla
• $|$ oddeľuje alternatívne syntaktické tvary (syntaktické frázy)
• $t$ na pravej strane je metapremenná, t.j.
  – premenná, pretože za ňu možno dosadiť ľubovoľný term a
  – meta, pretože nie je premennou jazyka NBL, ale metajazyka, ktorý popisuje NBL.

Gramatika v tvare odvodzovacích pravidiel

Odvodzovacie pravidlo má všeobecný tvar:

• Predpoklady aj záver sú tvrdenia; ak sú všetky predpoklady pravdivé, potom je pravdivý aj záver.
• Záver je len jeden.
• Názov pravidla je zvyčajne skratka, ktorá identifikuje pravidlo.
• Ak odvodzovacie pravidlo nemá predpoklady, nazýva sa axióma.
• Odvodzovacie pravidlo môže obsahovať aj podmienku, ktorá definuje kedy je možné dané pravidlo aplikovať.

Syntax jazyka NBL je možné definovať prostredníctvom nasledujúcich odvodzovacích pravidiel:

Funkcie na termoch NBL

Je možné definovať viacero funkcií, ktoré umožňujú skúmať rôzne vlastnosti termov v jazyku NBL.

Funkciu poskytujúcu veľkosť termu (počet uzlov v syntaktickom strome) je možné špecifikovať ako: $$size : Term \to \mathbb{N}$$ a definovať induktívne: $$ \begin{aligned} size(true) &= 1 \\ size(false) &= 1 \\ size(0) &= 1 \\ size(succ \, t_1) &= size(t_1) + 1 \\ size(pred \, t_1) &= size(t_1) + 1 \\ size(iszero \, t_1) &= size(t_1) + 1 \\ size(if \, t_1 \, \text{then} \, t_2 \, \text{else} \, t_3) &= size(t_1) + size(t_2) + size(t_3) + 1 \end{aligned} $$

Funkciu poskytujúcu hĺbku termu (počet uzlov v najdlhšej vetve syntaktického stromu) je možné špecifikovať ako:

$$depth : Term \to \mathbb{N}$$

a definovať induktívne:

$$ \begin{aligned} depth(true) &= 1 \\ depth(false) &= 1 \\ depth(0) &= 1 \\ depth(succ \, t_1) &= depth(t_1) + 1 \\ depth(pred \, t_1) &= depth(t_1) + 1 \\ depth(iszero \, t_1) &= depth(t_1) + 1 \\ depth(if \, t_1 \, \text{then} \, t_2 \, \text{else} \, t_3) &= max(depth(t_1),\ depth(t_2),\ depth(t_3)) + 1 \end{aligned} $$

Funkciu poskytujúcu množinu konštánt $Con(t)$ v terme $t$ je možné špecifikovať ako:

$$Con : Term \to P(\{0, true, false\})$$ a definovať induktívne:

$$ \begin{aligned} Con(true) &= \{true\} \\ Con(false) &= \{false\} \\ Con(0) &= \{0\} \\ Con(succ \, t_1) &= Con(t_1) \\ Con(pred \, t_1) &= Con(t_1) \\ Con(iszero \, t_1) &= Con(t_1) \\ Con(if \, t_1 \, \text{then} \, t_2 \, \text{else} \, t_3) &= Con(t_1) \cup Con(t_2) \cup Con(t_3) \end{aligned} $$

Využitím vyššie definovaných funkcií je možné formulovať množstvo zaujímavých vlastností prostredníctvom ktorých, je možné matematicky dokázať korektnosť našej formálnej definície.

Veta: Počet rozličných konštánt v terme $t$ nie je väčší ako veľkosť termu $t$. $$ \forall t.(\ |Con(t)| \leq size(t)\ )$$

Veta: Hĺbka termu $t$ nie je väčšia ako jeho veľkosť. $$ \forall t.(\ depth(t) \leq size(t)\ )$$

Sémantika NBL

Výpočet termov NBL opíšeme pomocou operačnej sémantiky, teda formálnych vyhodnocovacích pravidiel. Použijeme jej dve podoby:

• Sémantika malých krokov opisuje jeden elementárny krok výpočtu. Celé vyhodnotenie vzniká skladaním krokov, takže vidíme jednotlivé medzitermy aj poradie vyhodnotenia.
• Sémantika veľkých krokov spája počiatočný term priamo s výslednou hodnotou. Medzitermy nezaznamenáva; odvodzovací strom obsahuje iba úplné vyhodnotenia podtermov potrebných na získanie výsledku.

Obe podoby používajú rovnakú definíciu hodnôt a pre ukončené vyhodnotenie NBL určujú rovnaký výsledok.

Hodnota je term, ktorý považujeme za konečný výsledok výpočtu. Produkčné pravidlá pre hodnoty $v$ sú: $$ \begin{align*} & v ::= true \,|\, false \,|\, nv \\ & nv ::= 0 \,|\, succ \,~ nv \end{align*} $$

Metapremenná $v$ označuje ľubovoľnú hodnotu a $nv$ iba číselnú hodnotu. Číselné hodnoty $0,succ\ 0,succ(succ\ 0),\ldots$ stotožňujeme s prirodzenými číslami $0,1,2,\ldots$.

Sémantika malých krokov NBL

Sémantika malých krokov je definovaná ako vyhodnocovacia relácia:

$$\boxed{t \to t'}$$

Čítame: term $t$ sa vyhodnotí na term $t'$ v jednom kroku.

Malé kroky špecifikujú čiastočne definovanú sémantickú funkciu $$S_{\mathrm{NBL}}^{\to}:Term \rightharpoonup \{true, false\} \cup \mathbb{N},$$ ktorá je definovaná vzťahom $$ S_{\mathrm{NBL}}^{\to}[|\ t\ |] = v \quad \Longleftrightarrow \quad t \to^* v. $$

Správanie sa vyhodnocovacej relácie opisujú nasledujúce vyhodnocovacie pravidlá:

Sémantika veľkých krokov NBL

Sémantika malých krokov zachytáva jednotlivé medzistavy výpočtu. Sémantika veľkých krokov (z ang. big-step semantics) namiesto toho spája počiatočný term priamo s jeho výslednou hodnotou. Je definovaná vyhodnocovacou reláciou

$$ \boxed{t \Downarrow v} $$

a čítame ju: term $t$ sa vyhodnotí na hodnotu $v$ v sémantike veľkých krokov. Premisy pravidla opisujú úplné vyhodnotenie potrebných podtermov; nevybraná vetva podmieneného výrazu sa nevyhodnocuje.

Hodnoty sa vyhodnotia samy na seba:

$$ \frac{}{true \Downarrow true}\;(\mathrm{B\text{-}True}) $$

$$ \frac{}{false \Downarrow false}\;(\mathrm{B\text{-}False}) $$

$$ \frac{}{0 \Downarrow 0}\;(\mathrm{B\text{-}Zero}) $$

Podmienený výraz vyhodnotí iba vetvu určenú hodnotou podmienky:

$$ \frac{t_1 \Downarrow true \qquad t_2 \Downarrow v} {if\ t_1\ then\ t_2\ else\ t_3 \Downarrow v} \;(\mathrm{B\text{-}IfTrue}) $$

$$ \frac{t_1 \Downarrow false \qquad t_3 \Downarrow v} {if\ t_1\ then\ t_2\ else\ t_3 \Downarrow v} \;(\mathrm{B\text{-}IfFalse}) $$

Pravidlá pre operácie nad prirodzenými číslami najprv úplne vyhodnotia svoj argument:

$$ \frac{t \Downarrow nv}{succ\ t \Downarrow succ\ nv} \;(\mathrm{B\text{-}Succ}) $$

$$ \frac{t \Downarrow 0}{pred\ t \Downarrow 0} \;(\mathrm{B\text{-}PredZero}) $$

$$ \frac{t \Downarrow succ\ nv}{pred\ t \Downarrow nv} \;(\mathrm{B\text{-}PredSucc}) $$

$$ \frac{t \Downarrow 0}{iszero\ t \Downarrow true} \;(\mathrm{B\text{-}IszeroZero}) $$

$$ \frac{t \Downarrow succ\ nv}{iszero\ t \Downarrow false} \;(\mathrm{B\text{-}IszeroSucc}) $$

Veľké kroky poskytujú druhú špecifikáciu sémantickej funkcie:

$$ S_{\mathrm{NBL}}^{\Downarrow}:Term \rightharpoonup \{true,false\}\cup\mathbb{N}, \qquad S_{\mathrm{NBL}}^{\Downarrow}[|\ t\ |]=v \quad \Longleftrightarrow \quad t\Downarrow v. $$

Vetva $succ(succ\ 0)$ sa v strome nenachádza, pretože podmienka sa vyhodnotila na $true$ a pravidlo B-IfTrue vyhodnocuje iba vybranú vetvu.

Výsledkom vyhodnotenia veľkými krokmi je teda rovnaká hodnota ako pri vyhodnotení malými krokmi:

$$ S_{\mathrm{NBL}}^{\Downarrow}[|\ t\ |]=succ\ 0. $$

Vlastnosti sémantiky NBL

Nasledujúce tvrdenia uvádzame bez dôkazov. Ich formálne dôkazy budú vytvorené v dokazovacom systéme Rocq.

Lema (jeden malý krok zmenší term): Pre všetky $t,t'\in Term$ platí

$$ t\to t' \quad\Longrightarrow\quad size(t')\lt size(t). $$

Dôsledok (NBL nediverguje): V NBL neexistuje nekonečná postupnosť malých krokov

$$ t_0\to t_1\to t_2\to\cdots. $$

Veta (determinizmus sémantiky malých krokov): Pre všetky $t,t_1,t_2\in Term$ platí

$$ t\to t_1 \land t\to t_2 \quad\Longrightarrow\quad t_1=t_2. $$

Lema (hodnoty NBL): Pre každú hodnotu $v$ platí

$$ v\Downarrow v \qquad\text{a}\qquad \neg(\exists t'\in Term)(v\to t'). $$

Lema (kompatibilita malého a veľkého kroku): Pre všetky $t,t'\in Term$ a každú hodnotu $v$ platí

$$ t\to t' \land t'\Downarrow v \quad\Longrightarrow\quad t\Downarrow v. $$

Veta (ekvivalencia sémantiky malých a veľkých krokov): Pre každý $t\in Term$ a každú hodnotu $v$ platí

$$ t\Downarrow v \quad\Longleftrightarrow\quad t\to^*v. $$

Preto obe špecifikácie určujú rovnakú čiastočne definovanú sémantickú funkciu:

$$ S_{\mathrm{NBL}}^{\to}=S_{\mathrm{NBL}}^{\Downarrow}. $$

Dôsledok (determinizmus sémantiky veľkých krokov): Pre každý $t\in Term$ a hodnoty $v_1,v_2$ platí

$$ t\Downarrow v_1 \land t\Downarrow v_2 \quad\Longrightarrow\quad v_1=v_2. $$

Zaseknuté termy

Takto definovaný netypovaný jazyk NBL umožňuje konštruovanie syntakticky správnych termov, ktoré sa pri vyhodnocovaní zaseknú, ako napríklad:

$$succ(true).$$

Je možné jednoducho dokázať, že $succ(true) \in Term$, avšak pri pokuse o jeho vyhodnotenie nie je možné aplikovať žiadne pravidlo a vyhodnotenie sa zasekne (z ang. stuck). Term nie je hodnotou: neexistuje ani malý krok $succ(true)\to t'$, ani odvodenie $succ(true)\Downarrow v$. Funkcie $S_{\mathrm{NBL}}^{\to}$ a $S_{\mathrm{NBL}}^{\Downarrow}$ preto na tomto terme nie sú definované.

$\lambda$-kalkul

Je univerzálny formálny výpočtový model, ktorý dokáže simulovať akýkoľvek Turingov stroj (a vice versa). $\lambda$-kalkul má široké využitie v informatike, medzi ktoré patrí špecifikácia čŕt programovacích jazykov, návrh jazykov, implementácia jazykov a štúdium typových systémov, pričom jeho definícia je základom programovacích jazykov funkcionálnej paradigmy.

Dôležitosť $\lambda$-kalkulu spočíva v tom, že ho možno súčasne chápať ako:

• najjednoduchší univerzálny Turingovsky úplný programovací jazyk,
• matematický objekt, o ktorom možno dokázať dôležité vlastnosti.

$\lambda$-kalkul pozostáva z jedného pravidla redukcie (nahradenie premenných) a jedného tvaru definície funkcie. $\lambda$-kalkul je univerzálny v tom zmysle, že akúkoľvek vypočítateľnú funkciu možno vyjadriť a vyhodnotiť pomocou tohto modelu. Je teda ekvivalentný s Turingovými strojmi. Avšak $\lambda$-kalkul kladie dôraz na použitie redukčných pravidiel a nezaujíma sa o samotný stroj, ktorý ich implementuje. Je to prístup viac súvisiaci so softvérom než s hardvérom.

Základným konceptom v $\lambda$-kalkule je "Všetko je funkcia!". V $\lambda$-kalkule je funkcia definovaná ako $\lambda$-abstrakcia: $$\lambda x.t,$$ kde:

• $\lambda$ je syntaktický symbol označujúci začiatok abstrakcie,
• $x$ je parameter funkcie,
• $t$ je telo funkcie.

Syntax $\lambda$-kalkulu

Nech $Var$ je spočítateľne nekonečná množina mien premenných. Množina $\lambda$-termov $\Lambda$ je najmenšia množina spĺňajúca tieto podmienky:

1. Ak $x\in Var$, potom $x\in\Lambda$.
2. Ak $x\in Var$ a $t\in\Lambda$, potom $\lambda x.t\in\Lambda$.
3. Ak $t_1,t_2\in\Lambda$, potom $t_1\ t_2\in\Lambda$.

Slovo „najmenšia“ znamená, že do $\Lambda$ patria iba konečné termy zostrojené týmito pravidlami. Induktívna definícia, Backus–Naurova forma a nižšie uvedené odvodzovacie pravidlá sú tri zápisy tej istej syntaxe.

Syntax netypovaného čistého (pure) $\lambda$-kalkulu teda môžeme ekvivalentne zapísať produkčným pravidlom v Backus–Naurovej forme: $$t::= x\ |\ \lambda x.t\ |\ t\ t$$ kde:

• $t$ označuje $\lambda$-term,
• $x$ označuje ľubovoľnú premennú
• $\lambda x.t$ je $\lambda$-abstrakcia, definícia funkcie s parametrom $x$ a telom funkcie $t$.
• $\ t\ t$ je aplikácia funkcie $t$ na argument $t$ (prvé $t$ je aplikované na druhé $t$).

Metapremenné $x,y,z$ označujú prvky $Var$ a $t,s,u$ označujú ľubovoľné termy. Term $t$ je správne skonštruovaný, ak $t \in \Lambda$.

Konvencie syntaxe $\lambda$-kalkulu

Pre doplnenie definície abstraktnej syntaxe $\lambda$-kalkulu, budeme využívať nasledujúce konvencie:

• Vynechávame vonkajšie zátvorky: $$(t\ u) = t\ u $$

• Aplikácia je ľavo asociatívna: $$t\ u\ v = (t\ u)\ v$$ Pričom abstraktný syntaktický strom termu $t\ u\ v$ je zobrazený na nasledujúcom obrázku:

  
  

• Telo abstrakcie siaha čo najviac doprava.

Napríklad: \begin{align*} \lambda x. t\ u & = \lambda x. (t\ u) \newline \lambda x.\lambda y. x\ y\ z & = \lambda x.(\lambda y.(\ (x\ y)\ z)\ ) \end{align*} Pričom abstraktný syntaktický strom termu $\lambda x.\lambda y. x\ y\ z$ je zobrazený na nasledujúcom obrázku:

• Zápis viacnásobnej abstrakcie je možné skrátiť: $$\lambda x.\lambda y.\lambda z.t = \lambda x\ y\ z.t$$

Syntax v tvare odvodzovacích pravidiel

Syntax $\lambda$-kalkulu je možné definovať aj prostredníctvom odvodzovacích pravidiel:

Funkcia viacerých premenných

Z predchádzajúcich sekcií je zrejmé, že syntax $\lambda$-kalkulu umožňuje definíciu funkcií s viacerými parametrami. Napríklad funkciu: $$f(x,y)=x-y,$$ je možné definovať v $\lambda$-kalkule ako: $$\lambda x. \lambda y. x - y$$

Voľné a viazané premenné

Pred definíciou sémantiky λ-kalkulu musíme definovať pojmy výskytu voľnej a viazanej premennej.

• Výskyt premennej $x$ je viazaný, ak sa nachádza v tele abstrakcie s parametrom $x$. Viaže ho najbližšia takáto obklopujúca abstrakcia; vnorená abstrakcia s rovnakým parametrom tieni vonkajšiu.
• Výskyt premennej $x$ je voľný, ak sa nachádza v pozícii, kde nie je viazaná abstrakciou.

Napríklad, v $\lambda$-termoch:

• $x\ y$
• $\lambda y.x\ y$

sú výskyty premennej $x$ voľné, ale v termoch:

• $\lambda x.x$
• $\lambda z.\lambda x.\lambda y.x(y\ z)$

sú výskyty $x$ viazané.

Formálne je možné definovať pojem voľnej premennej ako funkciu $FV$, ktorá vráti množinu všetkých voľných premenných nasledovne: $$ \begin{aligned} FV(x) &= \{x\},\\ FV(\lambda x.t) &= FV(t)\setminus\{x\},\\ FV(t_1\ t_2) &= FV(t_1)\cup FV(t_2). \end{aligned} $$

Kombinátor

Term bez voľných premenných sa nazýva uzavretý. Uzavreté termy sa nazývajú kombinátory.

Štandardné (často používané) kombinátory sa zvyknú označovať: \begin{align*} I & = \lambda x.x \newline K & = \lambda x.\lambda y.x \newline S & = \lambda f.\lambda g.\lambda x.f \ x \ (g \ x) \newline D & = \lambda x.x \ x \newline Y & = \lambda f.((\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))) \end{align*}

Každý kombinátor sa dá vyjadriť použitím kombinátorov S, K a I.

$\alpha$-ekvivalencia a $\alpha$-konverzia

$\lambda$-kalkul používa statický rozsah viditeľnosti (static scoping). To znamená, že $$(\lambda \textcolor{blue}{x}. \textcolor{blue}{x}) (\lambda \textcolor{red}{x}. \textcolor{red}{x})$$ je ekvivalentné $$(\lambda \textcolor{blue}{x}. \textcolor{blue}{x}) (\lambda \textcolor{red}{y}. \textcolor{red}{y})$$

Dva termy sú $\alpha$-ekvivalentné, zapisujeme $t=_\alpha u$, ak majú rovnakú syntaktickú štruktúru a líšia sa iba menami viazaných premenných tak, že každý viazaný výskyt zostáva viazaný zodpovedajúcou abstrakciou. Mená voľných výskytov sa nemenia a žiadny voľný výskyt sa nesmie stať viazaným.

Takéto korektné premenovanie sa nazýva $\alpha$-konverzia alebo $\alpha$-premenovanie; nejde o výpočtovú redukciu. Napríklad: $$\lambda x.x\ y =_\alpha \lambda z.z\ y.$$ Voľnú premennú však nemožno premenovať: $$\lambda x.x\ y \not=_\alpha \lambda x.x\ z.$$ Nesmieme zmeniť ani abstrakciu, ktorá výskyt viaže: $$\lambda x.\lambda y.x \not=_\alpha \lambda y.\lambda y.y.$$ Vľavo je výskyt v tele viazaný vonkajšou abstrakciou, vpravo vnútornou.

Substitúcia

Pre definovanie sémantiky netypovaného $\lambda$-kalkulu je potrebné definovať funkciu substitúcie na termoch.

Zavedieme označenie: $$ [x \mapsto t_2 ]t_1, $$ ktoré znamená, že v $\lambda$-terme $t_1$ nahradíme všetky voľné výskyty premennej $ x$ termom $ t_2 $.

Substitúciu špecifikujeme ako úplnú funkciu na syntaxi s explicitnými menami: $$subst:Var\times\Lambda\times\Lambda\to\Lambda,\qquad subst(x,s,t)=[x\mapsto s]t.$$ Aby bol aj pri premenovaní výsledok jednoznačný, zavedieme množinu všetkých mien premenných termu: $$ \begin{aligned} Vars(x)&=\{x\},\\ Vars(\lambda x.t)&=\{x\}\cup Vars(t),\\ Vars(t_1\ t_2)&=Vars(t_1)\cup Vars(t_2). \end{aligned} $$ Pevne zvolíme postupnosť navzájom rôznych mien $x_0,x_1,x_2,\ldots$ z $Var$. Pre konečnú množinu $A\subseteq Var$ definujeme čerstvé meno: $$fresh(A)=x_k,\qquad k=\min\{n\in\mathbb N\mid x_n\notin A\}.$$ Keďže $A$ je konečná, také meno vždy existuje a je určené jednoznačne.

Substitúciu definujeme rekurziou podľa veľkosti spracúvaného termu, pričom $x,y,z$ označujú premenné a $s,t,t_1,t_2$ označujú $\lambda$-termy: $$ \begin{aligned} {}[x \mapsto s]x &= s, \\ [x \mapsto s]y &= y && \text{ak } x \neq y, \\ [x \mapsto s](t_1\ t_2) &= ([x \mapsto s]t_1)\ ([x \mapsto s]t_2), \\ [x \mapsto s](\lambda x.t) &= \lambda x.t, \\ [x \mapsto s](\lambda y.t) &= \lambda y.[x \mapsto s]t && \text{ak } y \neq x \text{ a } y \notin FV(s), \\ [x \mapsto s](\lambda y.t) &= \lambda z.[x \mapsto s]([y \mapsto z]t) && \text{ak } y \neq x \text{ a } y \in FV(s), \end{aligned} $$ pričom v poslednom prípade je meno $z$ určené rovnosťou $$z=fresh(Vars(t)\cup Vars(s)\cup\{x,y\}).$$ Iné vhodné čerstvé meno by dalo $\alpha$-ekvivalentný výsledok. Pevná funkcia $fresh$ však určuje jediný syntaktický výsledok.

Veľkosť termu je počet uzlov jeho abstraktného syntaktického stromu, analogicky ako pri NBL: $$ \begin{aligned} size(x)&=1,\\ size(\lambda x.t)&=1+size(t),\\ size(t_1\ t_2)&=1+size(t_1)+size(t_2). \end{aligned} $$ Rekurzívne volania spracúvajú menšie termy. V kolíznom prípade premenovanie $[y\mapsto z]t$ nemení veľkosť tela, takže aj následné volanie pracuje s termom menším než pôvodná abstrakcia. Substitúcia sa preto vždy skončí.

Pravidlo $[x \mapsto s](\lambda x.t)=\lambda x.t$ vyjadruje, že abstrakcia $\lambda x.t$ viaže premennú $x$, a preto sa substitúcia za $x$ v jej tele nevykoná. Ak by parameter $y$ abstrakcie $\lambda y.t$ zachytil voľnú premennú zo substituovaného termu $s$, musíme ho najskôr $\alpha$-premenovať na čerstvú premennú $z$. Takáto substitúcia sa nazýva substitúcia zabraňujúca zachyteniu premenných (capture-avoiding substitution).

Pri vnorených substitúciách používame zátvorky na určenie poradia. Napríklad $[y \mapsto u]([x \mapsto s]t)$ znamená, že najskôr vykonáme substitúciu $[x \mapsto s]t$ a potom substitúciu $[y \mapsto u]$. Nejde o pravidlo asociativity ani o všeobecný zákon skladania substitúcií.

Príklad zachytenia: Pri substitúcii do $\lambda\textcolor{red}{y}.x\ \textcolor{red}{y}$ by obyčajná textová náhrada dala nesprávny výsledok: $$[x\mapsto\textcolor{blue}{y}](\lambda\textcolor{red}{y}.x\ \textcolor{red}{y})\mathrel{\overset{\text{nesprávne}}{=}}\lambda\textcolor{red}{y}.\textcolor{blue}{y}\ \textcolor{red}{y}.$$ Modrý výskyt musí zostať voľný. Najskôr preto premenujeme parameter a jeho viazaný výskyt; pri $fresh(\{x,y\})=x_0$ dostaneme správne $$[x\mapsto\textcolor{blue}{y}](\lambda\textcolor{red}{y}.x\ \textcolor{red}{y})=\lambda\textcolor{red}{x_0}.\textcolor{blue}{y}\ \textcolor{red}{x_0}.$$

Sémantika $\lambda$-kalkulu

Sémantiku $\lambda$-kalkulu definujeme prostredníctvom sémantickej metódy nazývanej štrukturálna operačná sémantika (sémantika malých krokov).

$\beta$-redukcia je proces vyhodnotenia $\lambda$-termov postupným "vkladaním argumentov do funkcií".

Majme term: $$(\lambda x. t_1)\ t_2$$ kde:

• $x$ je parameter funkcie,
• $t_1$ je telo funkcie,
• $t_2$ je argument funkcie.

Všeobecná $\beta$-redukcia

$\beta$-redex je term tvaru $(\lambda x.t)\ s$. Kontrakcia redexu vykoná aplikáciu funkcie: voľné výskyty parametra $x$ v tele $t$ nahradí argumentom $s$ pomocou substitúcie zabraňujúcej zachyteniu. Veľkosť termu pritom nemusí klesnúť; argument sa môže aj skopírovať.

Redex sa môže nachádzať kdekoľvek v terme. Všeobecná $\beta$-redukcia $\to_\beta$ je najmenšia relácia na $\Lambda$ generovaná pravidlami:

$$\frac{}{(\lambda x.t)\ s\to_\beta[x\mapsto s]t}\quad(\beta)$$ $$\frac{t\to_\beta t'}{\lambda x.t\to_\beta\lambda x.t'}\quad(\beta\text{-Abs})$$ $$\frac{t_1\to_\beta t_1'}{t_1\ t_2\to_\beta t_1'\ t_2}\quad(\beta\text{-App1})$$ $$\frac{t_2\to_\beta t_2'}{t_1\ t_2\to_\beta t_1\ t_2'}\quad(\beta\text{-App2})$$

Prvé pravidlo kontrahuje redex; ostatné umožňujú vykonať jeden krok v tele abstrakcie a v oboch častiach aplikácie. Term bez $\beta$-redexu je v $\beta$-normálnej forme. Označenie $\to_\beta$ budeme odlišovať od $\to$, ktoré neskôr vyhradíme pre konkrétnu sémantiku volania hodnotou.

V nasledujúcich príkladoch sú $x,y,z,f,u,v$ navzájom rôzne premenné; najmä $y\notin FV(u)$. Ak by sme za $u$ dosadili term s voľným výskytom $y$, vnútorný parameter by sa musel najskôr premenovať. Pri ľubovoľných termoch musíme výsledok vždy určiť podľa definície substitúcie. Napríklad: \begin{align*} & (\lambda x. x)\ y \to_\beta [x \mapsto y] x = y \newline & (\lambda x. y)\ z \to_\beta [x \mapsto z]y = y \newline & (\lambda x. (f\ x))\ y \to_\beta [x \mapsto y] f\ x = f\ y \newline & (\lambda x. \lambda y. f \ x \ y)\ u\ v \to_\beta ([x \mapsto u] \lambda y. f \ x \ y)\ v = (\lambda y. f \ u \ y)\ v \to_\beta [y \mapsto v] f \ u \ y = f \ u \ v \end{align*}

Príklad s premenovaním: Substitúcia z predchádzajúcej sekcie sa použije pri kroku $$(\lambda x.\lambda\textcolor{red}{y}.x\ \textcolor{red}{y})\ \textcolor{blue}{y}\to_\beta\lambda\textcolor{red}{x_0}.\textcolor{blue}{y}\ \textcolor{red}{x_0}.$$ Voľný modrý výskyt $y$ zostal voľný; červený parameter a jeho viazaný výskyt dostali čerstvé meno $x_0$.

Viackroková redukcia a $\beta$-ekvivalencia

Viackroková $\beta$-redukcia $\to_\beta^*$ je reflexívny a tranzitívny uzáver $\to_\beta$. Zápis $t\to_\beta^*u$ znamená, že z $t$ dostaneme $u$ konečnou postupnosťou nula alebo viacerých $\beta$-krokov. Osobitne $t\to_\beta^*t$.

Pri porovnávaní termov pomocou $\beta$-ekvivalencie považujeme $\alpha$-ekvivalentné termy za reprezentácie toho istého termu. Na týchto triedach je $=_\beta$ reflexívny, symetrický a tranzitívny uzáver všeobecnej $\beta$-redukcie. Na pomenovaných termoch to znamená konečnú postupnosť $\beta$-krokov použitých v oboch smeroch a prípustných $\alpha$-premenovaní.

Redukcia je orientovaná, ekvivalencia je symetrická: $$t\to_\beta^*u\quad\Longrightarrow\quad t=_\beta u.$$ Opačná implikácia všeobecne neplatí. Napríklad $$y=_\beta(\lambda x.x)y,\qquad y\not\to_\beta^*(\lambda x.x)y.$$ Samotnú substitúciu a jednotlivé kroky naďalej počítame na pomenovanej syntaxi pomocou pevnej funkcie $fresh$.

Normálne formy v $\lambda$-kalkule

V $\lambda$-kalkule je koncept normálnych foriem kľúčový pre pochopenie toho, ako sa termy (výrazy) môžu redukovať alebo zjednodušovať. Pri každej normálnej forme treba uviesť, vzhľadom na ktoré redukčné pravidlá ju chápeme. Keďže nasledujúce redukčné stratégie pracujú s $\beta$-redukciou, bez ďalšieho spresnenia budeme hovoriť o $\beta$-normálnej forme.

$\beta$-normálna forma (NF)

$\lambda$-term je v $\beta$-normálnej forme, ak neobsahuje žiadny $\beta$-redex. V $\beta\eta$-normálnej forme je vtedy, ak neobsahuje ani $\beta$-redex, ani $\eta$-redex. Napríklad term $z\ y$ je v oboch týchto normálnych formách.

Weak head normal form (WHNF)

$\lambda$-term je vo WHNF (weak head normal form), ak má tvar $\lambda x.t$ alebo $x\ t_1\ldots t_n$ pre $n \geq 0$. Na jeho najvrchnejšej pozícii teda nie je $\beta$-redex, hoci telo abstrakcie alebo argumenty môžu obsahovať redexy. WHNF sa preto od plnej $\beta$-normálnej formy odlišuje.

Táto forma je dôležitá pri slabých a nestriktných stratégiách vyhodnotenia, ktoré neredukujú vnútri abstrakcií.

Striktná vs nestriktná stratégia vyhodnotenia

Striktná stratégia

(ang. Eager Evaluation) vyžaduje, aby sa argument funkcie v príslušnom operačnom zmysle vyhodnotil pred aplikáciou funkcie. Preto môže vyhodnotiť aj argument, ktorý telo funkcie nepoužije.

Nestriktná stratégia

nevyžaduje vyhodnotenie argumentu pred vstupom do tela funkcie. Volanie menom (call by name) je nestriktné a pri každom použití môže argument vyhodnocovať znova. Volanie podľa potreby (call by need) je jeho zdieľajúca, memoizujúca úprava a bežne sa spája s lenivým vyhodnotením (lazy evaluation). Pojmy „nestriktné“ a „call by need“ preto nie sú synonymá.

Ani jedna z týchto stratégií preto nie je univerzálne pamäťovo efektívnejšia.

Redukčné stratégie

Vo všeobecnosti môže konkrétny $\lambda$-term obsahovať viacero $\beta$-redexov. Redukčná stratégia určuje, ktorý z nich sa má redukovať ako ďalší. Samotná relácia plnej $\beta$-redukcie tento výber neurčuje, a preto je nedeterministická; praktické programovacie jazyky používajú konkrétne pravidlá vyhodnocovania.

Majme term: $$(\lambda x.x)\ ((\lambda x.x)\ (\lambda z.(\lambda x.x)\ z))$$ Nech $id=(\lambda x.x)$, potom predchádzajúci term je možné prepísať ako: $$id\ (id\ (\lambda z.id\ z))$$ V danom terme sa vyskytujú tri redexy:

1. $\underline{id\ (id\ (\lambda z.id\ z))}$
2. $id\ (\underline{id\ (\lambda z.id\ z)})$
3. $id\ (id\ (\lambda z.\underline{id\ z}))$

Existuje niekoľko rôznych redukčných a vyhodnocovacích stratégií, ktoré sa skúmajú pri návrhu programovacích jazykov. Uvedieme štyri dôležité prístupy; plná $\beta$-redukcia bez dodatočného pravidla výberu nie je deterministickou stratégiou.

Úplná $\beta$-redukcia

Úplná (neobmedzená) $\beta$-redukcia povoľuje v každom kroku zvoliť ľubovoľný redex, a to aj pod $\lambda$-abstrakciou. Nie je preto striktnou/eager stratégiou a bez dodatočného pravidla výberu redexu nie je deterministická: $$id\ (id\ (\lambda z.\underline{id\ z})) \to_\beta id\ (\underline{id\ (\lambda z. z)}) \to_\beta \underline{id\ (\lambda z. z)} \to_\beta (\lambda z. z) $$

Normálna $\beta$-redukcia

Normálne poradie (normal order) v každom kroku volí najľavejší vonkajší redex. Nevyžaduje vyhodnotenie argumentu pred aplikáciou funkcie, teda nie je striktné, a pri hľadaní plnej $\beta$-normálnej formy redukuje aj pod $\lambda$-abstrakciami. Ak $\beta$-normálna forma existuje, normálne poradie ju nájde: $$\underline{id\ (id\ (\lambda z.id\ z))} \to_\beta \underline{id\ (\lambda z.id\ z)}\to_\beta \lambda z.\underline{id\ z} \to_\beta \lambda z.z$$

Stratégia volania menom (z ang. call by name)

Volanie menom je slabé najľavejšie vonkajšie vyhodnocovanie: je nestriktné a neredukuje vnútri abstrakcií. Preto sa od normálneho poradia líši tým, že môže skončiť vo WHNF, ktorá ešte nie je $\beta$-normálnou formou: $$\underline{id\ (id\ (\lambda z.id\ z))} \to_\beta \underline{id\ (\lambda z.id\ z)}\to_\beta \lambda z.id\ z$$

Stratégia volania hodnotou (z ang. call by value)

Volanie hodnotou je striktná, slabá stratégia: neredukuje vnútri abstrakcií a argument najskôr vyhodnotí na hodnotu, až potom aplikuje funkciu:

$$id\ \underline{(id\ (\lambda z.id\ z))} \to \underline{id\ (\lambda z.id\ z)}\to \lambda z.id\ z$$

Výsledok je hodnotou, ale nemusí byť v $\beta$-normálnej forme, pretože telo abstrakcie môže obsahovať redex. Je teda aspoň vo WHNF.

Sémantika malých krokov pre volanie hodnotou

Relácia $t\to t'$ znamená jeden krok volania hodnotou. Najskôr definujeme hodnoty: $$v ::= \lambda x.t.$$ Ich množinu označíme $Val$. Hodnota sa definuje nezávisle od $\beta$-normálnej formy: telo abstrakcie sa pri slabom vyhodnotení neredukuje a môže obsahovať redex. Pravidlá definujeme na všetkých termoch vrátane otvorených; samotné premenné medzi hodnoty nezaraďujeme.

Vyhodnocovacia relácia je najmenšia relácia generovaná pravidlami:

$$\frac{t_1\to t_1'}{t_1\ t_2\to t_1'\ t_2}\quad(\text{E-App1})$$ $$\frac{t_2\to t_2'}{v_1\ t_2\to v_1\ t_2'}\quad(\text{E-App2})$$ $$\frac{}{(\lambda x.t)\ v\to[x\mapsto v]t}\quad(\text{E-AppAbs})$$

Metapremenné $v,v_1$ označujú iba hodnoty. Pravidlá tak určujú poradie: najskôr funkčná časť, potom argument a napokon substitúcia. Poradie, v akom sú schémy vypísané, samo osebe neurčuje ich použitie. Žiadne pravidlo nepovoľuje krok pod abstrakciou.

Viackrokové volanie hodnotou $\to^*$ je reflexívny a tranzitívny uzáver tejto relácie $\to$. Odlišujeme ho od $\to_\beta^*$.

Sémantickú funkciu špecifikujeme ako čiastočne definovanú funkciu $$S_\lambda:\Lambda\rightharpoonup Val,\qquad S_\lambda(t)=v\iff t\to^*v.$$ Ak sa z $t$ nedosiahne žiadna hodnota, funkcia na $t$ nie je definovaná. Príčinou môže byť zaseknutie (výpočet skončí na terme, ktorý nie je hodnotou a nemá ďalší krok) alebo divergencia (nekonečný výpočet).

Príklad použitia pravidiel

Nech $I=\lambda a.a$. Vyhodnoťme term $((\lambda f.f)I)((\lambda g.g)I)$:

$$ \begin{aligned} ((\lambda f.f)I)((\lambda g.g)I) &\to I((\lambda g.g)I) &&\text{E-App1},\\ &\to I\ I &&\text{E-App2},\\ &\to I &&\text{E-AppAbs}. \end{aligned} $$ Premisou prvého kroku je $(\lambda f.f)I\to I$, odvodené pravidlom E-AppAbs. Premisou druhého kroku je $(\lambda g.g)I\to I$, opäť podľa E-AppAbs. Tretí krok priamo dosadí hodnotu $I$ do tela identity. Výsledok $I$ je hodnotou, takže $S_\lambda(((\lambda f.f)I)((\lambda g.g)I))=I$.

Vlastnosti volania hodnotou

Veta: Každý krok volania hodnotou je $\beta$-krokom. Pre všetky $t,t'\in\Lambda$ platí $$t\to t'\quad\Longrightarrow\quad t\to_\beta t'.$$

Veta: Determinizmus volania hodnotou. Pre všetky $t,u_1,u_2\in\Lambda$ platí $$t\to u_1\land t\to u_2\quad\Longrightarrow\quad u_1=u_2.$$ Rovnosť výsledkov je tu doslovná syntaktická rovnosť: substitúcia používa pevný výber čerstvého mena. Determinizmus zaručuje aj jednoznačnosť dosiahnutej hodnoty v špecifikácii $S_\lambda$. Nezaručuje však existenciu kroku ani ukončenie výpočtu.

Dôkazy oboch tvrdení vykonáme v Rocq.

Teoréma Churcha-Rossera

Churchova–Rosserova veta vyjadruje konfluenciu všeobecnej $\beta$-redukcie. Pri pomenovaných termoch ju formulujeme až na $\alpha$-ekvivalenciu:

Ak $t\to_\beta^*t_1$ a $t\to_\beta^*t_2$, potom existujú termy $u_1,u_2\in\Lambda$ také, že $$t_1\to_\beta^*u_1,\qquad t_2\to_\beta^*u_2,\qquad u_1=_\alpha u_2.$$ Ak stotožníme $\alpha$-ekvivalentné reprezentácie, obe cesty teda možno predĺžiť do spoločného termu. Pevný výber $fresh$ sám osebe nezaručuje, že rôzne redukčné cesty zvolia rovnaké mená viazaných premenných.

Dôsledkom je, že ak $\beta$-normálna forma existuje, je jedinečná až na $\alpha$-ekvivalenciu. Teoréma však netvrdí, že každá redukčná postupnosť skončí alebo že každý term má normálnu formu. Týka sa $\to_\beta^*$, nie iba konkrétneho volania hodnotou $\to^*$.

Neterminácia a možná neterminácia

Niektoré termy nemajú $\beta$-normálnu formu.

Majme nasledujúci term: $$\omega = \lambda x.x\ x.$$ Majme term $\Omega$, ktorý je aplikáciou termu $\omega$ na $\omega$, potom ak sa pokúsime vyhodnotiť tento term, tak sa dostaneme do nasledujúcej situácie: $$\Omega = \omega\ \omega = (\lambda x.x\ x)\ (\lambda x.x\ x) \to_\beta [x \mapsto \lambda x.x\ x]x\ x = (\lambda x.x\ x)\ (\lambda x.x\ x) \to_\beta (\lambda x.x\ x)\ (\lambda x.x\ x) \to_\beta ... $$ Hovoríme, že takýto term diverguje vzhľadom na $\to_\beta$: existuje nekonečná postupnosť krokov. Uvedené kroky sú zároveň krokmi volania hodnotou, takže $\Omega$ diverguje aj vzhľadom na $\to$. Divergenciu vždy posudzujeme vzhľadom na zvolenú reláciu.

Iné termy $\beta$-normálnu formu majú, ale nie každá vyhodnocovacia stratégia ju musí dosiahnuť.

Majme term: $$(\lambda x. y)\ \Omega.$$ Pri využití normálneho poradia je možné term redukovať na jeho $\beta$-normálnu formu bez vyhodnotenia argumentu $\Omega$: $$(\lambda x. y)\ \Omega \to_\beta y$$ Tento príklad ukazuje, že normálne poradie nie je striktné. Rovnaký prvý krok vykoná aj volanie menom, ktoré sa však na rozdiel od normálneho poradia zastavuje bez redukcie pod abstrakciami. Pri volaní hodnotou je funkcia $(\lambda x.y)$ už hodnotou, ale pred jej aplikáciou sa musí na hodnotu vyhodnotiť argument $\Omega$. Ako ukazuje predchádzajúci príklad, toto vyhodnotenie diverguje: $$(\lambda x. y)\ \Omega \to (\lambda x. y)\ ((\lambda x.x\ x)\ (\lambda x.x\ x)) \to (\lambda x. y)\ ((\lambda x.x\ x)\ (\lambda x.x\ x)) \to ...$$

Normalizácia

Normalizačné vlastnosti termov definujeme vzhľadom na všetky možné postupnosti všeobecnej $\beta$-redukcie $\to_\beta$:

• Slabá normalizácia: Term je slabo normalizujúci, ak existuje aspoň jedna konečná postupnosť $\beta$-redukcií, ktorá vedie k $\beta$-normálnej forme.
• Silná normalizácia: Term je silno normalizujúci, ak každá postupnosť $\beta$-redukcií, ktorá sa v ňom začína, skončí.

Každý silno normalizujúci term je aj slabo normalizujúci, opačné tvrdenie však neplatí.

$\eta$-redukcia

Doplnkovým pravidlom na porovnávanie funkcií je $\eta$-redukcia. Ak máme term v tvare $$\lambda \textcolor{red}{x}.\ t\ \textcolor{red}{x}$$ je možné ho ďalej redukovať prostredníctvom $\eta$-redukcie: $$\lambda \textcolor{red}{x}.\ t\ \textcolor{red}{x} \to_\eta t \quad \quad \text{ak }\ x \notin FV(t)$$ za podmienky, že term $t$ neobsahuje žiadnu voľnú premennú $x$.

Táto relácia nie je súčasťou uvedenej operačnej sémantiky volania hodnotou.

Príklad s premenovaním zo sekcie o všeobecnej $\beta$-redukcii je možné redukovať na jeho $\beta\eta$-normálnu formu nasledovne: $$(\lambda x. \lambda \textcolor{red}{y}.\ x\ \textcolor{red}{y})\ \textcolor{blue}{y} =_\alpha (\lambda x. \lambda \textcolor{red}{z}.\ x\ \textcolor{red}{z})\ \textcolor{blue}{y} \to_\beta \lambda \textcolor{red}{z}.\ y\ \textcolor{red}{z} \to_\eta y $$

Zdroje

1. Pierce, Benjamin C.: Types and programming languages. MIT press, Cambridge, 2001 (Перевод на русский язык: Бенджамин Пирс. Типы в языках программирования. — Добросвет, 2012. — 680 с. — ISBN 978-5-7913-0082-9)
2. Pierce, Benjamin C et al.: Software Foundations, Electronic textbook, 2024
3. Sestoft, Peter.: "Demonstrating lambda calculus reduction." The essence of computation: complexity, analysis, transformation (2002): 420-435.
4. Selinger, Peter.: "Lecture notes on the lambda calculus." arXiv preprint arXiv:0804.3434 (2008).
5. Valerie Novitzká, Daniel Mihályi: Teória typov, TU Košice, 2015