Typovaný NBL, Jednoducho typovaný $\lambda$-kalkul

Typovaný jazyk s prirodzenými číslami a booleovskými hodnotami

NBL obsahuje iba pevne dané konštruktory pre prirodzené čísla a booleovské hodnoty. Typový systém preto môžeme zaviesť bez otázok spojených s premennými a funkciami. Potrebujeme rozlíšiť dva druhy výsledkov a pri každom konštruktore určiť, ktoré typy jeho argumentov sú prípustné.

Formálny opis typovaného NBL pozostáva z abstraktnej syntaxe, statickej sémantiky a dynamickej sémantiky. Oproti netypovanému NBL pridáme samostatnú syntaktickú kategóriu typov a typovaciu reláciu. Syntax vykonávaných termov ani ich vyhodnocovacie pravidlá sa nemenia.

Typová kontrola overuje, či argumenty jednotlivých konštrukcií majú požadovaný typ. Nasledovník napríklad vyžaduje prirodzené číslo. Porovnajme tri syntakticky správne termy:

Hodnotu určuje gramatika výsledkov jazyka. Redukovateľný term môže podľa vyhodnocovacích pravidiel vykonať ďalší krok. Zaseknutý term nie je hodnotou a zároveň nemá ďalší krok. Neprítomnosť kroku preto sama osebe neznamená chybu: pri hodnote je očakávaným ukončením výpočtu.

Syntax a typy

Abstraktná syntax má nasledujúcu Backusovu–Naurovu formu:

$$ \begin{aligned} t::={}&\ \mathsf{true}\mid\mathsf{false}\mid\mathsf{if}\ t\ \mathsf{then}\ t\ \mathsf{else}\ t\mid 0\mid\mathsf{succ}\ t\mid\mathsf{pred}\ t\mid\mathsf{iszero}\ t,\\ v::={}&\ \mathsf{true}\mid\mathsf{false}\mid nv,\\ nv::={}&\ 0\mid\mathsf{succ}\ nv,\\ T::={}&\ \mathsf{Bool}\mid\mathsf{Nat}. \end{aligned} $$

Metapremenná $t$ označuje ľubovoľný term, $v$ hodnotu, $nv$ numerickú hodnotu a $T$ typ. Typ $\mathsf{Bool}$ je základný typ booleovských hodnôt, $\mathsf{Nat}$ základný typ prirodzených čísel vrátane nuly. Numerické hodnoty $0$, $\mathsf{succ}\ 0$, $\mathsf{succ}\;(\mathsf{succ}\ 0),\ldots$ reprezentujú čísla $0,1,2,\ldots$.

Konštruktory majú pevný počet podtermov. Zátvorkami v konkrétnom zápise vyznačíme ich rozsah, napríklad $\mathsf{succ}\;(\mathsf{pred}\ 0)$. Typy nie sú termami: pridanie riadka pre $T$ nemení abstraktný syntaktický strom programu.

Typovacia relácia a typovací úsudok

Typovacia relácia spája termy s typmi. Je definovaná ako najmenšia relácia uzavretá vzhľadom na nižšie uvedené typovacie pravidlá. Konkrétne tvrdenie o členstve v tejto relácii zapisujeme ako typovací úsudok:

$$\boxed{t:T}$$

Čítame ho „term $t$ má typ $T$“. Term je typovateľný, ak existuje typ $T$, pre ktorý možno úsudok $t:T$ odvodiť typovacími pravidlami. Vtedy tiež hovoríme, že term je správne typovaný. Ak taký typ neexistuje, term je netypovateľný.

Zápis $t:T$ patrí do metajazyka, ktorým opisujeme NBL. Nie je súčasťou syntaxe termu. Typová anotácia naproti tomu uvádza typ priamo v syntaxi programu. NBL typové anotácie nemá; stretneme sa s nimi až pri parametroch typovaných $\lambda$-abstrakcií.

Nasledujúce zápisy sú typovacie úsudky:

$$ \begin{aligned} 0&:\mathsf{Nat},\\ \mathsf{succ}\;(\mathsf{succ}\ 0)&:\mathsf{Nat},\\ \mathsf{iszero}\;(\mathsf{succ}\ 0)&:\mathsf{Bool},\\ \mathsf{if}\ \mathsf{true}\ \mathsf{then}\ \mathsf{succ}\ 0\ \mathsf{else}\ 0 &:\mathsf{Nat}. \end{aligned} $$

Typová kontrola dostane term a očakávaný typ a rozhodne, či je zodpovedajúci úsudok odvoditeľný. Odvodenie typu, nazývané aj typová inferencia, dostane term a jeho typ hľadá. Neúspešná kontrola konkrétneho typu ešte nemusí znamenať, že term nemá žiadny typ: napríklad $0:\mathsf{Bool}$ neplatí, ale $0:\mathsf{Nat}$ platí.

Typovacie pravidlá NBL

Pravidlá sú schémy. Dosadením konkrétnych termov a typov za metapremenné získame ich inštancie. Nad čiarou sú premisy, pod čiarou záver a napravo názov pravidla. Pravidlo bez premís je axióma.

$$ \frac{}{\mathsf{true}:\mathsf{Bool}}\quad{\small (\text{T-True})} \qquad \frac{}{\mathsf{false}:\mathsf{Bool}}\quad{\small (\text{T-False})} $$

$$\frac{}{0:\mathsf{Nat}}\quad{\small (\text{T-Zero})}$$

$$ \frac{t:\mathsf{Nat}}{\mathsf{succ}\ t:\mathsf{Nat}}\quad{\small (\text{T-Succ})} \qquad \frac{t:\mathsf{Nat}}{\mathsf{pred}\ t:\mathsf{Nat}}\quad{\small (\text{T-Pred})} $$

$$\frac{t:\mathsf{Nat}}{\mathsf{iszero}\ t:\mathsf{Bool}}\quad{\small (\text{T-IsZero})}$$

$$ \frac{t_1:\mathsf{Bool}\qquad t_2:T\qquad t_3:T} {\mathsf{if}\ t_1\ \mathsf{then}\ t_2\ \mathsf{else}\ t_3:T} \quad{\small (\text{T-If})} $$

Nasledovník a predchodca vyžadujú argument typu $\mathsf{Nat}$ a ich výsledok má tiež typ $\mathsf{Nat}$. Test $\mathsf{iszero}$ prijíma prirodzené číslo, ale vracia booleovský výsledok. V podmienenom výraze musí mať podmienka typ $\mathsf{Bool}$ a obe vetvy ten istý typ $T$. Požiadavka na vetvy platí aj vtedy, keď je podmienka syntakticky $\mathsf{true}$: typovacie pravidlo kontroluje obe vetvy, hoci dynamická sémantika vyhodnotí iba vybranú.

Pravidlá môžeme pri kontrole čítať zdola nahor. Najvrchnejší konštruktor termu určí jediné možné posledné pravidlo. Napríklad pri $\mathsf{succ}\ t:\mathsf{Nat}$ musíme použiť T-Succ a skontrolovať premisu $t:\mathsf{Nat}$. Týmto postupom zostrojíme typovací strom:

1. V koreni je celý kontrolovaný typovací úsudok.
2. Vyberieme pravidlo, ktorého záver sa zhoduje s úsudkom, a nad ním vytvoríme požadované premisy.
3. Každú premisu overíme rovnakým spôsobom.
4. Derivácia je úplná, keď sa všetky vetvy skončia axiómami.

Otvorená vetva s neodvoditeľnou premisou znamená neúspešný pokus o deriváciu. Taký strom nie je platným odvodením úsudku v koreni.

Príklady typovacích stromov

Prvý term poznáme už z prvej prednášky. Teraz overíme jeho typ, bez vykonania programu:

$$ \mathsf{succ}\bigl(\mathsf{pred}\;( \mathsf{if}\ \mathsf{iszero}\;(\mathsf{pred}\ 0) \ \mathsf{then}\ \mathsf{succ}\ 0 \ \mathsf{else}\ \mathsf{succ}\;(\mathsf{succ}\ 0))\bigr):\mathsf{Nat}. $$

Úplný strom obsahuje všetky požadované premisy:

V druhom príklade kontrolujeme úsudok:

$$ \mathsf{succ}\;(\mathsf{if}\ \mathsf{iszero}\;(\mathsf{pred}\ 0) \ \mathsf{then}\ \mathsf{true}\ \mathsf{else}\ \mathsf{false}):\mathsf{Nat}. $$

Nasledujúci zápis je nedokončený pokus o typovaciu deriváciu. Červené úsudky sú požiadavky, ktoré nemožno odvodiť:

Dynamická sémantika NBL

Typová kontrola nemení spôsob výpočtu. Preberáme malokrokovú vyhodnocovaciu reláciu z prvej prednášky:

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

Úsudok znamená, že term $t$ vykoná jeden krok na term $t'$. Zápis $t\to^*t'$ označuje nula alebo viac krokov, teda reflexívny a tranzitívny uzáver relácie $\to$.

Všetkých desať vyhodnocovacích pravidiel NBL má tvar:

$$ \frac{}{\mathsf{if}\ \mathsf{true}\ \mathsf{then}\ t_2\ \mathsf{else}\ t_3\to t_2} \quad{\small (\text{E-IfTrue})} $$

$$ \frac{}{\mathsf{if}\ \mathsf{false}\ \mathsf{then}\ t_2\ \mathsf{else}\ t_3\to t_3} \quad{\small (\text{E-IfFalse})} $$

$$ \frac{t_1\to t_1'} {\mathsf{if}\ t_1\ \mathsf{then}\ t_2\ \mathsf{else}\ t_3 \to\mathsf{if}\ t_1'\ \mathsf{then}\ t_2\ \mathsf{else}\ t_3} \quad{\small (\text{E-If})} $$

$$\frac{t\to t'}{\mathsf{succ}\ t\to\mathsf{succ}\ t'}\quad{\small (\text{E-Succ})}$$

$$ \frac{}{\mathsf{pred}\ 0\to 0}\quad{\small (\text{E-PredZero})} \qquad \frac{}{\mathsf{pred}\;(\mathsf{succ}\ nv)\to nv}\quad{\small (\text{E-PredSucc})} $$

$$\frac{t\to t'}{\mathsf{pred}\ t\to\mathsf{pred}\ t'}\quad{\small (\text{E-Pred})}$$

$$ \frac{}{\mathsf{iszero}\ 0\to\mathsf{true}}\quad{\small (\text{E-IsZeroZero})} \qquad \frac{}{\mathsf{iszero}\;(\mathsf{succ}\ nv)\to\mathsf{false}}\quad{\small (\text{E-IsZeroSucc})} $$

$$\frac{t\to t'}{\mathsf{iszero}\ t\to\mathsf{iszero}\ t'}\quad{\small (\text{E-IsZero})}$$

Metapremenná $nv$ smie zastupovať iba numerickú hodnotu. Napríklad E-PredSucc možno priamo použiť na $\mathsf{pred}\;(\mathsf{succ}\;(\mathsf{succ}\ 0))$, ale nie na $\mathsf{pred}\;(\mathsf{succ}\;(\mathsf{pred}\ 0))$. V druhom prípade sa najprv vyhodnotí vnútorný predchodca.

Výpočtové pravidlá vykonajú samotnú operáciu, napríklad E-PredZero. Kongruenčné pravidlá určujú, v ktorom podterme sa výpočet vykoná, napríklad E-Pred a E-Succ. Pri podmienenom výraze najprv vyhodnotíme podmienku a potom vyberieme jednu vetvu. Druhá vetva sa nevyhodnotí.

Vlastnosti typovaného NBL

Typový systém skúmame z hľadiska jednoznačnosti a bezpečnosti. Bezpečnosť spája dve vlastnosti:

• Progres: správne typovaný term je hodnotou alebo môže vykonať krok.
• Stabilita typov: vyhodnocovací krok zachováva typ termu.

Inverzia typovania a kanonické tvary hodnôt opisujú predpoklady, ktoré pri týchto vlastnostiach používame. Predikát $\operatorname{isvalue}(t)$ vyjadruje, že term $t$ je hodnotou podľa gramatiky jazyka.

Inverzia typovania

Pri typovej kontrole čítame pravidlá od požadovaného záveru k premisám. Inverzia typovania presne vyjadruje, aké informácie o typoch podtermov získame, keď už vieme, že celý úsudok je odvoditeľný.

Teoréma: O inverzii typovania NBL.

Nasledujúce tvrdenia platia pre všetky termy $t,t_1,t_2,t_3$ jazyka NBL a každý typ $R$:

1. Ak $\mathsf{true}:R$ alebo $\mathsf{false}:R$, potom $R=\mathsf{Bool}$.
2. Ak $\mathsf{if}\ t_1\ \mathsf{then}\ t_2\ \mathsf{else}\ t_3:R$, potom $t_1:\mathsf{Bool}$, $t_2:R$ a $t_3:R$.
3. Ak $0:R$, potom $R=\mathsf{Nat}$.
4. Ak $\mathsf{succ}\ t:R$ alebo $\mathsf{pred}\ t:R$, potom $R=\mathsf{Nat}$ a $t:\mathsf{Nat}$.
5. Ak $\mathsf{iszero}\ t:R$, potom $R=\mathsf{Bool}$ a $t:\mathsf{Nat}$.

Napríklad z typovania $\mathsf{iszero}\;(\mathsf{pred}\ 0):R$ získame, že $R=\mathsf{Bool}$ a $\mathsf{pred}\ 0:\mathsf{Nat}$. Inverzia tak spája typ celého termu s požiadavkami na jeho časti. Je užitočná pri typovej kontrole aj pri formulovaní ďalších vlastností typovania.

Jednoznačnosť typov

Pri typovateľnom terme chceme dostať jednoznačnú statickú informáciu. Musíme preto vylúčiť, že tomu istému termu pravidlá priradia dva rôzne typy.

Teoréma: O jednoznačnosti typov NBL.

Pre každý term $t$ a typy $T_1,T_2$ platí:

$$ (\forall t,T_1,T_2)\bigl(t:T_1\land t:T_2\ \Longrightarrow\ T_1=T_2\bigr). $$

Každý typovateľný term NBL má teda práve jeden typ. Nie každý syntakticky správny term je typovateľný, ako ukázal druhý typovací príklad. Teoréma porovnáva typy; jej záverom nie je tvrdenie o jedinečnosti typovacích stromov. Inverzia opisuje možné typovanie jednotlivých tvarov a jednoznačnosť vylučuje rozdielne výsledné typy.

Kanonické tvary hodnôt

Typová informácia je užitočná aj pri výbere vyhodnocovacieho pravidla. Ak podterm už je hodnotou, potrebujeme vedieť, aký syntaktický tvar môže pri danom type mať.

Lema: O kanonických tvaroch NBL.

Ak $v$ je hodnota, potom:

$$ \begin{aligned} (\forall v)\bigl(v:\mathsf{Bool}&\ \Longrightarrow\ v=\mathsf{true}\lor v=\mathsf{false}\bigr),\\ (\forall v)\bigl(v:\mathsf{Nat}&\ \Longrightarrow\ v\text{ je numerická hodnota}\bigr). \end{aligned} $$

Lema charakterizuje možné tvary hodnôt, nie jedinú hodnotu každého typu. Typ $\mathsf{Nat}$ má napríklad hodnoty $0$ aj $\mathsf{succ}\ 0$. Vzťah medzi typom a tvarom hodnoty je podstatný pre progres: booleovská hodnota v podmienke umožní vybrať vetvu a numerická hodnota umožní vykonať príslušnú číselnú operáciu.

Progres

Typová kontrola má vylúčiť situáciu, keď term ešte nie je výsledkom, ale výpočet už nemôže pokračovať.

Teoréma: O progrese NBL.

Pre každý term $t$ a typ $T$ platí:

$$ (\forall t,T)\bigl(t:T\ \Longrightarrow\ \operatorname{isvalue}(t)\lor(\exists t')(t\to t')\bigr). $$

NBL neobsahuje premenné, takže všetky jeho termy sú uzavreté. Progres hovorí o možnosti kroku celého termu; ten nemusí byť výpočtovým redexom na najvyššej úrovni. Napríklad:

$$\mathsf{succ}\;(\mathsf{pred}\ 0)\to\mathsf{succ}\ 0.$$

Celý krok vznikne pravidlom E-Succ z podkroku $\mathsf{pred}\ 0\to 0$ podľa E-PredZero. Výsledok už je hodnotou. Kanonické tvary vysvetľujú, prečo správny typ hodnotového argumentu zodpovedá tvaru, ktorý vyhodnocovacie pravidlá očakávajú.

Stabilita typov

Progres sa vzťahuje na správne typovaný stav. Aby typová informácia zostala použiteľná aj po výpočtovom kroku, musí ju dynamická sémantika rešpektovať.

Teoréma: O stabilite typu NBL.

Pre termy $t,t'$ a typ $T$ platí:

$$ (\forall t,t',T)\bigl(t:T\land t\to t'\ \Longrightarrow\ t':T\bigr). $$

Vyhodnotenie teda nemení typ termu. Napríklad $\mathsf{pred}\;(\mathsf{succ}\ 0):\mathsf{Nat}$ a po kroku máme $0:\mathsf{Nat}$. Stabilita umožňuje spojiť statickú informáciu získanú pred spustením s ďalšími stavmi programu.

Typová bezpečnosť

Progres vylučuje zaseknutie správne typovaného aktuálneho stavu a stabilita typov zabezpečuje správny typ po kroku. Typová bezpečnosť vyjadruje ich spoločný význam pre celý výpočet.

Dôsledok: Bezpečnosť typovaného NBL.

Ak $t:T$ a $t\to^*t'$, potom $t'$ je hodnota alebo existuje $t''$ také, že $t'\to t''$:

$$ (\forall t,t',T)\bigl(t:T\land t\to^*t'\ \Longrightarrow\ \operatorname{isvalue}(t')\lor(\exists t'')(t'\to t'')\bigr). $$

Žiadny dosiahnutý stav správne typovaného programu sa teda nezasekne. Ide o záruku voči definovaným vyhodnocovacím pravidlám, nie o záruku výsledku zamýšľaného programátorom. Progres a stabilita samy osebe tiež nie sú všeobecným tvrdením o ukončení výpočtu.

Jednoducho typovaný $\lambda$-kalkul

NBL umožňuje skúmať typy základných údajov, ale neobsahuje premenné ani používateľom definované funkcie. Netypovaný $\lambda$-kalkul z prednášok 1 a 2 poskytuje premenné, abstrakcie a aplikácie. Teraz k nim pridáme typovú informáciu, aby sme mohli určiť, aké argumenty funkcia prijíma a aký výsledok vracia.

Jednoducho typovaný $\lambda$-kalkul označujeme $\lambda_{\to}$ alebo skratkou STLC (simply typed lambda calculus). Jeho jediným typovým konštruktorom je $\to$. Najprv definujeme čistý kalkul bez vstavaných základných typov a ich operácií. Neskôr ho rozšírime o $\mathsf{Bool}$ a $\mathsf{Nat}$.

Typový konštruktor, funkčný typ a jednoduché typy

Typový konštruktor je syntaktická operácia, ktorá z typov vytvára nový typ. Nie je termom ani funkciou vykonávanou počas výpočtu programu. Konštruktor $\to$ je binárny: z typov $T_1$ a $T_2$ vytvorí funkčný typ:

$$T_1\to T_2.$$

Tento typ opisuje funkcie prijímajúce argument typu $T_1$ a vracajúce výsledok typu $T_2$. Typ $T_1$ nazývame doménou a $T_2$ kodoménou funkčného typu. Aj doména a kodoména môžu byť funkčnými typmi, takže dokážeme opísať funkcie vyššieho rádu z druhej prednášky.

Nech:

$$\mathcal{A}=\{A,B,C,\ldots\}$$

je neprázdna množina atómových typových konštánt. Jej prvky sú neinterpretované atómové typy: každý je pevný syntaktický symbol, pre ktorý čistý kalkul nezavádza vlastné hodnoty ani primitívne operácie.

Nech $\mathcal{B}$ označuje množinu vstavaných základných typov. Pre každý taký typ jazyk určuje hodnoty, primitívne operácie a ich sémantiku. Všeobecná gramatika jednoduchých typov je:

$$T::=a\mid b\mid T\to T, \qquad a\in\mathcal{A},\quad b\in\mathcal{B}.$$

Použité symboly majú odlišné úlohy:

• $A,B,C$ sú konkrétne atómové typové konštanty z $\mathcal{A}$.
• $a$ je metapremenná pre ľubovoľnú atómovú typovú konštantu.
• $b$ je metapremenná pre ľubovoľný vstavaný základný typ.
• $T,S,R$ a ich indexované varianty sú metapremenné pre ľubovoľný jednoduchý typ.

Obe skupiny atómových typov nemajú vnútornú typovú štruktúru; odlišujú sa svojou úlohou v jazyku. Funkčné typy vznikajú konečným použitím konštruktora $\to$. Symboly $a,b,T$ používame v metajazyku. Nie sú typovými premennými polymorfného jazyka. V STLC nezavádzame abstrakciu nad typmi ani polymorfizmus.

V čistom STLC je prázdna iba množina vstavaných základných typov:

$$\mathcal{B}=\emptyset.$$

Množina $\mathcal{A}$ zostáva neprázdna a gramatika čistých jednoduchých typov je:

$$T::=a\mid T\to T,\qquad a\in\mathcal{A}.$$

Môžeme teda používať typy $A$, $A\to A$, $A\to B$ aj $(A\to B)\to C$ bez zavedenia $\mathsf{Bool}$ či $\mathsf{Nat}$. Napríklad typ $(A\to B)\to C$ opisuje funkciu prijímajúcu funkciu, kým $A\to(B\to C)$ opisuje funkciu, ktorá po prijatí argumentu typu $A$ vráti ďalšiu funkciu.

Šípka funkčného typu je podľa konvencie zápisu pravo asociatívna:

$$T_1\to T_2\to T_3=T_1\to(T_2\to T_3).$$

Nejde o rovnosť dvoch rôzne zostrojených typov, ale o dohodu, ako čítať zápis bez zátvoriek. Typ $(T_1\to T_2)\to T_3$ má inú štruktúru a jeho ľavé zátvorky nemožno vynechať. Pravá asociativita prirodzene zodpovedá curried funkciám: funkcia s typom $A\to B\to C$ prijíma argumenty postupne.

Typy chápeme ako syntaktické stromy. Rovnosť funkčných typov preto znamená rovnosť ich zodpovedajúcich zložiek:

$$T_1\to T_2=S_1\to S_2 \quad\Longleftrightarrow\quad T_1=S_1\ \land\ T_2=S_2.$$

Túto vlastnosť nazývame injektívnosťou typového konštruktora $\to$.

Explicitné typovanie

Oproti netypovanému kalkulu sa mení abstrakcia: jej parameter obsahuje typovú anotáciu $T$. Premenné a aplikácie majú rovnaký tvar ako predtým. Ako v prvej prednáške, aplikácia je ľavo asociatívna a telo abstrakcie siaha čo najviac doprava:

$$ t_1\ t_2\ t_3=(t_1\ t_2)\ t_3, \qquad \lambda x:T.t_1\ t_2=\lambda x:T.(t_1\ t_2). $$

Hodnotami čistého kalkulu pri volaní hodnotou sú abstrakcie. Ich telá môžu obsahovať redexy; zvolená stratégia pod abstrakciou neredukuje. Premenná sama nie je hodnotou.

V Churchovom štýle typovania sú typy parametrov explicitnou súčasťou syntaxe: $\lambda x:T.t$. V Curryho štýle má abstrakcia tvar $\lambda x.t$ a typ parametra nie je zapísaný v terme. V tejto prednáške používame Churchov štýl. Nemusíme anotovať celú abstrakciu: jej výsledný typ určia typovacie pravidlá z anotácie parametra a typu tela.

Odvodenie typu sa používa aj v explicitne typovanom kalkule. Chýbajúce anotácie v Curryho štýle si vyžadujú ďalšiu analýzu použitia premenných, ale odvodzovanie typov samo osebe nevyžaduje polymorfizmus. Podrobné algoritmy typovej rekonštrukcie budú témou neskorších prednášok.

Typový kontext a typovacie pravidlá STLC

Pri NBL sme typ určovali bez ďalších predpokladov. Pri premenných však potrebujeme vedieť, aké typy majú. Uvažujme vnorenú abstrakciu:

$$\lambda f:A\to B.\lambda x:A.f\ x.$$

Vonkajšia abstrakcia prijíma funkciu $f$ typu $A\to B$. Jej telom je vnútorná abstrakcia $\lambda x:A.f\ x$, ktorá prijíma argument $x$ typu $A$ a aplikuje naň funkciu $f$.

Pri typovej kontrole však musíme postupne prejsť od abstrakcií k ich telám. Keď sa sústredíme iba na najvnútornejšie telo $f\ x$, zápisy $\lambda f:A\to B$ a $\lambda x:A$ už nie sú súčasťou skúmaného podtermu. Zo samotného zápisu $f\ x$ preto nevieme, aké typy majú premenné $f$ a $x$. Ak by sme pri prechode do tela zabudli anotácie parametrov, nevedeli by sme overiť typ aplikácie.

Informáciu z anotácií si preto potrebujeme niekde uložiť a preniesť ju do typovej kontroly tela. Na to zavádzame typový kontext: zoznam deklarácií premenných a ich typov. Pred prechodom do tela abstrakcie doň pridáme deklaráciu jej parametra; pri typovej kontrole výskytu premennej v ňom vyhľadáme jej typ.

Pri prechode do tiel postupne pridávame typové predpoklady:

1. Pred vonkajšou abstrakciou nepotrebujeme žiadne deklarácie: celý term je uzavretý.
2. V tele vonkajšej abstrakcie máme k dispozícii $f:A\to B$. Tento predpoklad platí aj vo vnorenej abstrakcii.
3. V tele vnútornej abstrakcie, teda pri typovej kontrole $f\ x$, máme oba predpoklady: $f:A\to B$ a $x:A$. Typ argumentu zodpovedá doméne funkcie, preto má aplikácia $f\ x$ typ $B$.

Pri návrate z tiel určujeme typy abstrakcií. Vnútorná abstrakcia viaže $x$ a má typ $A\to B$; pri jej typovej kontrole ešte potrebujeme predpoklad o $f$. Vonkajšia abstrakcia viaže aj $f$, takže celý term má typ:

$$(A\to B)\to(A\to B).$$

Typ podtermu teda určujeme vzhľadom na predpoklady uložené v kontexte. Samotný úsudok $t:T$ už nestačí: pri aplikácii $f\ x$ musíme zaznamenať aj deklarácie oboch premenných.

Typový kontext, otvorené a uzavreté termy

Typový kontext $\Gamma$ je konečná postupnosť deklarácií premenných, v ktorej má každá premenná najviac jednu deklaráciu:

$$\Gamma::=\epsilon\mid\Gamma,x:T, \qquad x\notin\operatorname{dom}(\Gamma).$$

Symbol $\epsilon$ označuje prázdny kontext. Množina $\operatorname{dom}(\Gamma)$ obsahuje mená premenných deklarovaných v kontexte, pričom $\operatorname{dom}(\epsilon)=\emptyset$. Podmienka čerstvosti zaručuje, že deklarácia premennej má jednoznačný typ.

Typovací úsudok STLC má tvar:

$$\boxed{\Gamma\vdash t:T}$$

Čítame ho „v kontexte $\Gamma$ má term $t$ typ $T$“. Predpoklady sú naľavo od $\vdash$ a tvrdenie o type termu napravo. Symbol $\vdash$ patrí do metajazyka. Tento tvar úsudku sa niekedy nazýva aj sekvent. Typovacia relácia teraz spája kontext, term a typ.

Pripomeňme si viazanie premenných z prvej prednášky. Výskyt premennej je viazaný, ak patrí do rozsahu abstrakcie s príslušným parametrom; inak je voľný. Term je uzavretý, ak nemá voľné premenné, teda $FV(t)=\emptyset$. V opačnom prípade je otvorený. V uvedenom príklade má samostatný podterm $f\ x$ dve voľné premenné. V terme $\lambda x:A.f\ x$ je voľná už iba $f$; celý term $\lambda f:A\to B.\lambda x:A.f\ x$ je uzavretý.

Pri prázdnom kontexte používame skrátený zápis:

$$\vdash t:T.$$

Odvoditeľnosť takého úsudku zaručuje, že term je uzavretý. Uzavretosť však sama nezaručuje typovateľnosť. Kontext navyše môže obsahovať aj deklarácie, ktoré daný term nevyužije; nie je automaticky presným zoznamom jeho voľných premenných.

Syntax čistého STLC

Úplná abstraktná syntax čistého kalkulu zahŕňa termy, hodnoty, typy a kontexty:

$$ \begin{aligned} t&::=x\mid\lambda x:T.t\mid t\ t,\\ v&::=\lambda x:T.t,\\ T&::=a\mid T\to T,\qquad a\in\mathcal{A},\\ \Gamma&::=\epsilon\mid\Gamma,x:T,\qquad x\notin\operatorname{dom}(\Gamma). \end{aligned} $$

• Termy sú premenné, abstrakcie a aplikácie.
• Hodnoty sú abstrakcie; pri volaní hodnotou ich telá nevyhodnocujeme.
• Typy vznikajú z atómových typových konštánt použitím konštruktora $\to$.
• Kontexty sú konečné postupnosti deklarácií s jedinečnými menami premenných.

$\alpha$-ekvivalencia a tienenie mien

Pri formálnej typovej kontrole pracujeme s termami až na $\alpha$-ekvivalenciu. Pred rozšírením kontextu preto môžeme viazaný parameter vhodne premenovať, aby bol čerstvý vzhľadom na aktuálny kontext.

Opakované meno parametra nie je syntaktickou chybou. Vo výraze:

$$\lambda x:A.\lambda x:A.x$$

vnútorná abstrakcia tieni vonkajšie viazanie. Posledné $x$ označuje vnútorný parameter. Term má napríklad $\alpha$-ekvivalentný zápis:

$$\lambda x:A.\lambda y:A.y.$$

Pri typovej kontrole tohto reprezentanta vytvoríme kontext $x:A,y:A$, ktorý spĺňa jedinečnosť deklarácií. Premenovanie nemení štruktúru viazania ani typ termu $A\to A\to A$. Podmienka jedinečnosti mien v kontexte teda neznamená všeobecný zákaz lexikálneho tienenia v syntaxi.

Pravidlá pre premennú, abstrakciu a aplikáciu

Statickú sémantiku čistého STLC určujú tri pravidlá:

$$\frac{x:T\in\Gamma}{\Gamma\vdash x:T}\quad{\small (\text{T-Var})}$$

$$ \frac{\Gamma,x:T_1\vdash t_2:T_2} {\Gamma\vdash\lambda x:T_1.t_2:T_1\to T_2} \quad{\small (\text{T-Abs})} $$

$$ \frac{\Gamma\vdash t_1:T_1\to T_2\qquad\Gamma\vdash t_2:T_1} {\Gamma\vdash t_1\ t_2:T_2} \quad{\small (\text{T-App})} $$

V T-Abs musí byť $\Gamma,x:T_1$ platným kontextom, teda $x\notin\operatorname{dom}(\Gamma)$; v prípade konfliktu najprv použijeme $\alpha$-konverziu.

• T-Var použije existujúcu deklaráciu. Premenná nedostáva ľubovoľný typ: má presne typ uvedený pri jej mene v kontexte. Listom tejto vetvy je overená podmienka $x:T\in\Gamma$.

• T-Abs dočasne rozšíri kontext o anotovaný parameter. Ak telo v rozšírenom kontexte má typ $T_2$, celá abstrakcia má typ $T_1\to T_2$. V závere sa vrátime k pôvodnému kontextu $\Gamma$, pretože parameter je už viazaný abstrakciou. Typ tela určujeme statickou analýzou; nepotrebujeme abstrakciu aplikovať ani jej telo vykonať.

• T-App vyžaduje funkčný typ ľavého termu a presnú zhodu typu argumentu s doménou tohto typu. Výsledkom aplikácie je kodoména $T_2$. Typová kontrola oboch podtermov používa rovnaký kontext. Funkčná časť môže byť abstrakciou, premennou funkčného typu alebo ďalším zloženým termom; pravidlo rozhoduje podľa typu.

Úplná derivácia identity

Pri identite $\lambda x:A.x$ najprv zavedieme predpoklad $x:A$. T-Var potom určí typ tela a T-Abs vytvorí funkčný typ:

Curried aplikácia

Uvažujme náročnejší príklad s tromi vnorenými abstrakciami. Nech $A,B,C\in\mathcal{A}$. Overíme úsudok:

$$ \vdash\lambda x:A\to B\to C.\lambda y:A.\lambda z:B.x\ y\ z: (A\to B\to C)\to A\to B\to C. $$

Pre prehľadnosť pomenujeme priebežné kontexty:

$$ \begin{aligned} \Gamma_1&=x:A\to B\to C,\\ \Gamma_2&=\Gamma_1,y:A,\\ \Gamma_3&=\Gamma_2,z:B. \end{aligned} $$

Telo je podľa ľavej asociativity $(x\ y)\ z$. Typ $x$ je $A\to(B\to C)$: prvá aplikácia prijme $y:A$ a vráti term typu $B\to C$, druhá prijme $z:B$ a vráti term typu $C$. Úplný strom je:

Dynamická sémantika čistého STLC

Typová kontrola overuje prípustné použitie funkcií. Samotné vykonanie aplikácie však naďalej opisujeme malými krokmi, ktoré ukazujú presnú zmenu termu. Ako v prvej prednáške používame volanie hodnotou (call-by-value).

Vyhodnocovacie pravidlá

Relácia $t\to t'$ označuje jeden krok a jej reflexívny a tranzitívny uzáver $t\to^*t'$ nula alebo viac krokov. Hodnotami čistého STLC sú termy tvaru $\lambda x:T.t$. Pravidlá sú:

$$\frac{t_1\to t_1'}{t_1\ t_2\to t_1'\ t_2}\quad{\small (\text{E-App1})}$$

$$\frac{t_2\to t_2'}{v_1\ t_2\to v_1\ t_2'}\quad{\small (\text{E-App2})}$$

$$ \frac{}{(\lambda x:T.t_{12})\ v_2\to[x\mapsto v_2]t_{12}} \quad{\small (\text{E-AppAbs})} $$

Metapremenné $v_1,v_2$ zastupujú iba hodnoty. E-App1 vyhodnotí najprv funkčnú časť aplikácie. Keď je hodnotou, E-App2 umožní vyhodnotiť argument. E-AppAbs vykoná $\beta$-redukciu až vtedy, keď je funkčná časť abstrakciou a argument hodnotou. Žiadne pravidlo nepovoľuje vyhodnotenie tela pod abstrakciou.

Substitúcia a úloha anotácie

Zápis:

$$[x\mapsto s]t$$

označuje substitúciu termu $s$ za voľné výskyty premennej $x$ v terme $t$. Používame substitúciu zabraňujúcu zachyteniu voľných premenných, zavedenú v prvej prednáške. Pod abstrakciou viažucou $x$ sa jej viazané výskyty nenahrádzajú. Ak by iný parameter zachytil voľnú premennú termu $s$, najprv ho premenujeme pomocou $\alpha$-konverzie.

Typové anotácie vnorených abstrakcií zostávajú zachované. Napríklad:

$$[x\mapsto s](\lambda y:A.x)=\lambda z:A.s,$$

ak $y\in FV(s)$, $x\ne y$ a $z$ zvolíme čerstvé vzhľadom na všetky mená v zúčastnených termoch. Bez premenovania by sa voľné $y$ v $s$ zachytilo.

Anotácia parametra sa pri E-AppAbs znovu nekontroluje. Zhodu typu argumentu s typom parametra zabezpečuje T-App ešte pred výpočtom. Anotácia aplikovanej abstrakcie zanikne spolu s touto abstrakciou; anotácie vnorených abstrakcií zostávajú súčasťou výsledného termu.

Príklad vyhodnotenia identity

Uvažujme uzavretý term:

$$ (\lambda x:A\to A.x)\; \bigl((\lambda y:A\to A.y)\;(\lambda z:A.z)\bigr). $$

Jeho typ je $A\to A$. Funkčná časť vonkajšej aplikácie je už hodnotou, ale argument ešte obsahuje aplikáciu. Preto:

$$ \begin{aligned} &(\lambda x:A\to A.x)\; \bigl((\lambda y:A\to A.y)\;(\lambda z:A.z)\bigr)\\ &\to(\lambda x:A\to A.x)\;(\lambda z:A.z) &&{\small (\text{E-App2 s premisou E-AppAbs})}\\ &\to\lambda z:A.z &&{\small (\text{E-AppAbs})}. \end{aligned} $$

Prvý krok vyhodnotí argument dosadením $\lambda z:A.z$ za $y$. Druhý dosadí túto hodnotu za $x$ do tela vonkajšej identity. Výsledok je abstrakciou, teda hodnotou. Výpočet sa tu skončí, aj keby jej telo obsahovalo ďalší redex.

Príklad ilustruje oddelenie statickej a dynamickej sémantiky: vyhodnocovacie pravidlá neodvodzujú typy. Vlastnosť, podľa ktorej zostáva typ počas výpočtu rovnaký, neskôr sformulujeme ako stabilitu typov.

Typová kontrola, odvodenie typu a obývanie typu

Typovací úsudok $\Gamma\vdash t:T$ obsahuje tri zložky. Podľa toho, ktoré z nich poznáme a ktorú hľadáme, vzniknú tri rôzne úlohy:

Pri typovej kontrole napríklad dostaneme kontext $\Gamma=g:A\to B,z:A$, term $g\ z$ a očakávaný typ $B$. Overíme, že funkčná časť má typ $A\to B$ a argument typ $A$, takže $\Gamma\vdash g\ z:B$ platí. Ak ako očakávaný typ zadáme $A$ a $A\ne B$, kontrola bude neúspešná.

Pri odvodení typu dostaneme ten istý kontext a term, ale výsledný typ nepoznáme:

$$\Gamma\vdash g\ z:\ ?$$

Zo známych typov funkcie a argumentu odvodíme $B$. Otáznik je iba didaktický symbol hľadanej zložky, nie súčasť syntaxe kalkulu ani formálneho úsudku.

V explicitne typovanom STLC ide o syntézu výsledného typu zo syntaxe termu, kontextu a existujúcich anotácií. Typy parametrov sú už uvedené v abstrakciách. Typová kontrola ani inferencia preto nie sú vyhradené výlučne explicitne, resp. implicitne typovaným jazykom.

Pri obývaní typu ešte nemáme term. Hľadáme napríklad uzavretého obyvateľa typu $A\to A$:

$$\vdash\ ? :A\to A.$$

Riešením je identita:

$$\lambda x:A.x,$$

pre ktorú sme už zostrojili úplný typovací strom. Obývanie možno chápať ako hľadanie programu podľa typovej špecifikácie. Súvisí aj s Curryho–Howardovou korešpondenciou, ktorá spája typy s logickými výrokmi a typované termy s ich dôkazmi. Jej podrobnému výkladu sa budeme venovať neskôr.

Rozšírenie STLC o $\mathsf{Bool}$ a $\mathsf{Nat}$

Čistý kalkul zachytáva typované funkcie bez vstavaných údajových hodnôt. Teraz pridáme booleovské hodnoty, prirodzené čísla a všetky základné konštruktory NBL. Funkcie tak môžu priamo spracúvať tieto údaje. V druhej prednáške sme ich reprezentovali Churchovými kódovaniami; tu ide o vstavané konštrukcie s vlastnými pravidlami, nie o skratky za Churchove termy.

Množina $\mathcal{A}$ zostáva zachovaná. Mení sa množina vstavaných základných typov:

$$\mathcal{B}=\{\mathsf{Bool},\mathsf{Nat}\}.$$

Syntax rozšíreného jazyka

Úplná gramatika termov, hodnôt, typov a kontextov je:

$$ \begin{aligned} t::={}&\ x\mid\lambda x:T.t\mid t\ t \mid\mathsf{true}\mid\mathsf{false}\\ &\mid\mathsf{if}\ t\ \mathsf{then}\ t\ \mathsf{else}\ t \mid 0\mid\mathsf{succ}\ t\mid\mathsf{pred}\ t\mid\mathsf{iszero}\ t,\\ v::={}&\ \lambda x:T.t\mid\mathsf{true}\mid\mathsf{false}\mid nv,\\ nv::={}&\ 0\mid\mathsf{succ}\ nv,\\ T::={}&\ a\mid b\mid T\to T, \qquad a\in\mathcal{A},\quad b\in\mathcal{B},\\ b::={}&\ \mathsf{Bool}\mid\mathsf{Nat},\\ \Gamma::={}&\ \epsilon\mid\Gamma,x:T, \qquad x\notin\operatorname{dom}(\Gamma). \end{aligned} $$

Zachovávame ľavú asociativitu aplikácie, pravú asociativitu funkčného typu a maximálny rozsah tela abstrakcie doprava. Argumenty prefixných konštruktorov a vetvy podmieneného výrazu v zložitejších termoch ohraničíme zátvorkami. Napríklad $f\;(\mathsf{succ}\ x)$ je aplikácia $f$ na term $\mathsf{succ}\ x$.

Typovacie pravidlá rozšíreného STLC

Statickú sémantiku rozšíreného STLC tvorí desať pravidiel: tri pravidlá pre premennú, abstrakciu a aplikáciu a sedem pravidiel pre booleovské a číselné konštruktory.

$$\frac{x:T\in\Gamma}{\Gamma\vdash x:T}\quad{\small (\text{T-Var})}$$

$$ \frac{\Gamma,x:T_1\vdash t_2:T_2} {\Gamma\vdash\lambda x:T_1.t_2:T_1\to T_2} \quad{\small (\text{T-Abs})} $$

$$ \frac{\Gamma\vdash t_1:T_1\to T_2\qquad\Gamma\vdash t_2:T_1} {\Gamma\vdash t_1\ t_2:T_2} \quad{\small (\text{T-App})} $$

$$ \frac{}{\Gamma\vdash\mathsf{true}:\mathsf{Bool}}\quad{\small (\text{T-True})} \qquad \frac{}{\Gamma\vdash\mathsf{false}:\mathsf{Bool}}\quad{\small (\text{T-False})} $$

$$\frac{}{\Gamma\vdash 0:\mathsf{Nat}}\quad{\small (\text{T-Zero})}$$

$$ \frac{\Gamma\vdash t:\mathsf{Nat}} {\Gamma\vdash\mathsf{succ}\ t:\mathsf{Nat}}\quad{\small (\text{T-Succ})} \qquad \frac{\Gamma\vdash t:\mathsf{Nat}} {\Gamma\vdash\mathsf{pred}\ t:\mathsf{Nat}}\quad{\small (\text{T-Pred})} $$

$$ \frac{\Gamma\vdash t:\mathsf{Nat}} {\Gamma\vdash\mathsf{iszero}\ t:\mathsf{Bool}}\quad{\small (\text{T-IsZero})} $$

$$ \frac{\Gamma\vdash t_1:\mathsf{Bool}\qquad \Gamma\vdash t_2:T\qquad\Gamma\vdash t_3:T} {\Gamma\vdash\mathsf{if}\ t_1\ \mathsf{then}\ t_2\ \mathsf{else}\ t_3:T} \quad{\small (\text{T-If})} $$

Spolu ide o desať typovacích pravidiel. Kontext umožňuje použiť v číselných operáciách aj premenné, napríklad $x:\mathsf{Nat}\vdash\mathsf{succ}\ x:\mathsf{Nat}$. Konštanty nepotrebujú žiadny predpoklad o premenných a ich typ možno overiť v ľubovoľnom platnom kontexte.

T-If má rovnakú požiadavku na zhodu typov vetiev ako v NBL. V rozšírenom STLC však $T$ môže byť aj funkčný typ: obe vetvy môžu napríklad vracať funkciu typu $\mathsf{Nat}\to\mathsf{Nat}$. Podmienka musí naďalej mať typ $\mathsf{Bool}$.

Dynamická sémantika rozšíreného STLC

Vyhodnocovaciu reláciu definujeme na všetkých termoch rozšírenej syntaxe. Pravidlá pre aplikáciu majú rovnaký tvar ako v čistom kalkule, ale metapremenné $v_1,v_2$ teraz zastupujú hodnoty rozšírenej gramatiky:

$$\frac{t_1\to t_1'}{t_1\ t_2\to t_1'\ t_2}\quad{\small (\text{E-App1})}$$

$$\frac{t_2\to t_2'}{v_1\ t_2\to v_1\ t_2'}\quad{\small (\text{E-App2})}$$

$$ \frac{}{(\lambda x:T.t_{12})\ v_2\to[x\mapsto v_2]t_{12}} \quad{\small (\text{E-AppAbs})} $$

Pridáme všetkých desať pravidiel pre booleovské a číselné konštruktory:

$$ \frac{}{\mathsf{if}\ \mathsf{true}\ \mathsf{then}\ t_2\ \mathsf{else}\ t_3\to t_2} \quad{\small (\text{E-IfTrue})} $$

$$ \frac{}{\mathsf{if}\ \mathsf{false}\ \mathsf{then}\ t_2\ \mathsf{else}\ t_3\to t_3} \quad{\small (\text{E-IfFalse})} $$

$$ \frac{t_1\to t_1'} {\mathsf{if}\ t_1\ \mathsf{then}\ t_2\ \mathsf{else}\ t_3 \to\mathsf{if}\ t_1'\ \mathsf{then}\ t_2\ \mathsf{else}\ t_3} \quad{\small (\text{E-If})} $$

$$\frac{t\to t'}{\mathsf{succ}\ t\to\mathsf{succ}\ t'}\quad{\small (\text{E-Succ})}$$

$$ \frac{}{\mathsf{pred}\ 0\to 0}\quad{\small (\text{E-PredZero})} \qquad \frac{}{\mathsf{pred}\;(\mathsf{succ}\ nv)\to nv}\quad{\small (\text{E-PredSucc})} $$

$$\frac{t\to t'}{\mathsf{pred}\ t\to\mathsf{pred}\ t'}\quad{\small (\text{E-Pred})}$$

$$ \frac{}{\mathsf{iszero}\ 0\to\mathsf{true}}\quad{\small (\text{E-IsZeroZero})} \qquad \frac{}{\mathsf{iszero}\;(\mathsf{succ}\ nv)\to\mathsf{false}}\quad{\small (\text{E-IsZeroSucc})} $$

$$\frac{t\to t'}{\mathsf{iszero}\ t\to\mathsf{iszero}\ t'}\quad{\small (\text{E-IsZero})}$$

Týchto trinásť pravidiel úplne určuje dynamickú sémantiku rozšíreného jazyka. Nezavádzame ďalšiu primitívnu operáciu ani pravidlo pre meno používateľskej funkcie. Jej správanie vznikne abstrakciou, aplikáciou a už definovanými pravidlami.

Substitúciu rozšírime na nové konštruktory: konštanty $\mathsf{true}$, $\mathsf{false}$ a $0$ sa nemenia; pri $\mathsf{succ}$, $\mathsf{pred}$ a $\mathsf{iszero}$ substituujeme v argumente a pri $\mathsf{if}$ vo všetkých troch podtermoch. Napríklad:

$$ \begin{aligned} [x\mapsto s](\mathsf{pred}\ t)&=\mathsf{pred}\;([x\mapsto s]t),\\ [x\mapsto s](\mathsf{if}\ t_1\ \mathsf{then}\ t_2\ \mathsf{else}\ t_3) &=\mathsf{if}\ [x\mapsto s]t_1\\ &\quad\mathsf{then}\ [x\mapsto s]t_2\ \mathsf{else}\ [x\mapsto s]t_3. \end{aligned} $$

Použitie funkcie deklarovanej v typovom kontexte

Nech typový kontext obsahuje deklaráciu funkcie:

$$\Gamma=f:\mathsf{Nat}\to\mathsf{Nat}.$$

Vykonáme typovú kontrolu otvoreného termu:

$$ \Gamma\vdash\lambda x:\mathsf{Nat}.f\;(\mathsf{succ}\ x): \mathsf{Nat}\to\mathsf{Nat}. $$

V tele abstrakcie použijeme rozšírený kontext $\Gamma,x:\mathsf{Nat}$. Úplný typovací strom je:

Premenná $f$ zostáva voľná. Jej deklarácia určuje iba typ, nie definíciu funkcie ani výpočtové pravidlo. Celá abstrakcia je hodnotou, ale po jej aplikovaní by sme na vykonanie volania $f$ potrebovali dodať konkrétnu funkciu za $f$. Typový kontext sám takú hodnotu neposkytuje.

Uzavretá funkcia s podmienkou

Uvažujme uzavretú funkciu s podmienkou:

$$ \lambda x:\mathsf{Nat}. \mathsf{if}\ \mathsf{iszero}\ x \ \mathsf{then}\ \mathsf{succ}\ 0 \ \mathsf{else}\ \mathsf{pred}\ x. $$

Parameter $x$ je viazaný abstrakciou, takže celý term je uzavretý. Na nule funkcia vracia jednotku; pri kladnej numerickej hodnote vracia predchodcu.

Overíme, že abstrakcia má typ $\mathsf{Nat}\to\mathsf{Nat}$ v prázdnom kontexte. Označme pre prehľadnosť $\Gamma_x=x:\mathsf{Nat}$. Úplný typovací strom je:

• T-Var priradí parametru $x$ typ $\mathsf{Nat}$. T-IsZero z toho odvodí, že podmienka $\mathsf{iszero}\ x$ má typ $\mathsf{Bool}$.
• Axióma T-Zero a pravidlo T-Succ priradia prvej vetve $\mathsf{succ}\ 0$ typ $\mathsf{Nat}$.
• T-Var a T-Pred priradia druhej vetve $\mathsf{pred}\ x$ tiež typ $\mathsf{Nat}$.

Všetky požiadavky T-If sú splnené, takže telo abstrakcie má typ $\mathsf{Nat}$. T-Abs spojí anotáciu parametra s typom tela: celá funkcia má typ $\mathsf{Nat}\to\mathsf{Nat}$ v prázdnom kontexte.

Typová kontrola aplikácie uzavretej funkcie

Aplikujme funkciu na term:

$$ (\lambda x:\mathsf{Nat}.\mathsf{if}\ \mathsf{iszero}\ x\ \mathsf{then}\ \mathsf{succ}\ 0\ \mathsf{else}\ \mathsf{pred}\ x)\;(\mathsf{pred}\;(\mathsf{succ}\;(\mathsf{succ}\ 0))). $$

Argument ešte nie je hodnotou, ale má typ $\mathsf{Nat}$. Typová kontrola nevyžaduje jeho predchádzajúce vyhodnotenie. Použitím úplnej derivácie abstrakcie z predchádzajúceho stromu získame:

Vyhodnotenie aplikácie pri volaní hodnotou

Ľavý term aplikácie je už abstrakciou. Volanie hodnotou preto najprv vyhodnotí argument:

$$ \begin{aligned} &(\lambda x:\mathsf{Nat}. \mathsf{if}\ \mathsf{iszero}\ x \ \mathsf{then}\ \mathsf{succ}\ 0 \ \mathsf{else}\ \mathsf{pred}\ x)\; (\mathsf{pred}\;(\mathsf{succ}\;(\mathsf{succ}\ 0)))\\ &\to(\lambda x:\mathsf{Nat}. \mathsf{if}\ \mathsf{iszero}\ x \ \mathsf{then}\ \mathsf{succ}\ 0 \ \mathsf{else}\ \mathsf{pred}\ x)\;(\mathsf{succ}\ 0) &&{\small (\text{E-App2})}\\ &\to\mathsf{if}\ \mathsf{iszero}\;(\mathsf{succ}\ 0) \ \mathsf{then}\ \mathsf{succ}\ 0 \ \mathsf{else}\ \mathsf{pred}\;(\mathsf{succ}\ 0) &&{\small (\text{E-AppAbs})}\\ &\to\mathsf{if}\ \mathsf{false} \ \mathsf{then}\ \mathsf{succ}\ 0 \ \mathsf{else}\ \mathsf{pred}\;(\mathsf{succ}\ 0) &&{\small (\text{E-If})}\\ &\to\mathsf{pred}\;(\mathsf{succ}\ 0) &&{\small (\text{E-IfFalse})}\\ &\to 0 &&{\small (\text{E-PredSucc})}. \end{aligned} $$

Prvý krok používa podkrok $\mathsf{pred}\;(\mathsf{succ}\;(\mathsf{succ}\ 0))\to\mathsf{succ}\ 0$, podľa E-PredSucc, kde $nv=\mathsf{succ}\ 0$. Druhý vykoná substitúciu $[x\mapsto\mathsf{succ}\ 0]$ v celom tele abstrakcie. Tretí pomocou E-If a podkroku E-IsZeroSucc vyhodnotí podmienku; štvrtý vyberie druhú vetvu. Posledný vypočíta predchodcu jednotky.

Výsledkom je numerická hodnota $0$. Pôvodný term, všetky medzitermy aj výsledok majú typ $\mathsf{Nat}$. Tento konkrétny výpočet ilustruje vlastnosť, ktorú v metateórii vyjadrí veta o stabilite typu.

Krátky príklad s nasledovníkom

Na jednoduchšom terme môžeme oddelene sledovať vyhodnotenie argumentu a substitúciu:

$$ \begin{aligned} (\lambda x:\mathsf{Nat}.\mathsf{succ}\ x)\; (\mathsf{pred}\;(\mathsf{succ}\ 0)) &\to(\lambda x:\mathsf{Nat}.\mathsf{succ}\ x)\;0 &&{\small (\text{E-App2 s premisou E-PredSucc})}\\ &\to\mathsf{succ}\ 0 &&{\small (\text{E-AppAbs})}. \end{aligned} $$

Až po vyhodnotení argumentu na $0$ dosadíme túto hodnotu za $x$. Term $\mathsf{succ}\ 0$ je už numerickou hodnotou; nepotrebuje ďalšie pravidlo, ktoré by ho menilo na iný číselný zápis. Aj tu má pôvodný term a výsledok typ $\mathsf{Nat}$.

Metateória jednoducho typovaného $\lambda$-kalkulu

Syntax, typovanie a operačná sémantika definujú formálny jazyk. Samotná existencia typovacích pravidiel však ešte negarantuje typovú bezpečnosť: musíme overiť, či prijaté termy zodpovedajú tomu, čo očakávajú vyhodnocovacie pravidlá.

Metateória skúma vlastnosti formálneho systému pre všetky jeho termy. Nasledujúce tvrdenia formulujeme pre celý rozšírený STLC s $\mathsf{Bool}$ a $\mathsf{Nat}$, nie iba pre čistý funkčný fragment. Kontexty sú platné podľa ich gramatiky a konflikty viazaných mien riešime $\alpha$-konverziou.

Jednotlivé výsledky skúmajú tieto vlastnosti:

• Typovanie: inverzia a jednoznačnosť typov.
• Vyhodnocovanie: hodnoty nevykonávajú krok a vyhodnotenie je deterministické.
• Progres: kanonické tvary hodnôt umožňujú použiť príslušné vyhodnocovacie pravidlo.
• Stabilita typov: vlastnosti kontextu a substitúcie zabezpečujú zachovanie typu po kroku.
• Typová bezpečnosť: progres a stabilita vylučujú zaseknutie dosiahnutých stavov.
• Ukončenie a výsledok: normalizácia zaručuje konečný výpočet a deterministickosť jedinú výslednú hodnotu.

Predikát $\operatorname{isvalue}(t)$ teraz používame pre rozšírenú gramatiku hodnôt STLC.

Inverzia typovania

Z typovania celého termu potrebujeme spätne získať informácie o jeho podtermoch. Napríklad pri aplikácii nás zaujíma, aký funkčný typ musí mať ľavý term a aký typ musí mať argument.

Teoréma: O inverzii typovania.

Nech $\Gamma$ je ľubovoľný platný kontext. Nasledujúce tvrdenia platia pre všetky premenné $x$, termy $t,t_1,t_2,t_3$ a jednoduché typy $R,T_1$:

1. Ak $\Gamma\vdash x:R$, potom $x:R\in\Gamma$.
2. Ak $\Gamma\vdash\lambda x:T_1.t_2:R$, potom existuje $R_2$ také, že $R=T_1\to R_2$ a $\Gamma,x:T_1\vdash t_2:R_2$.
3. Ak $\Gamma\vdash t_1\ t_2:R$, potom existuje $T_{11}$ také, že $\Gamma\vdash t_1:T_{11}\to R$ a $\Gamma\vdash t_2:T_{11}$.
4. Ak $\Gamma\vdash\mathsf{true}:R$ alebo $\Gamma\vdash\mathsf{false}:R$, potom $R=\mathsf{Bool}$.
5. Ak $\Gamma\vdash\mathsf{if}\ t_1\ \mathsf{then}\ t_2\ \mathsf{else}\ t_3:R$, potom $\Gamma\vdash t_1:\mathsf{Bool}$, $\Gamma\vdash t_2:R$ a $\Gamma\vdash t_3:R$.
6. Ak $\Gamma\vdash 0:R$, potom $R=\mathsf{Nat}$.
7. Ak $\Gamma\vdash\mathsf{succ}\ t:R$ alebo $\Gamma\vdash\mathsf{pred}\ t:R$, potom $R=\mathsf{Nat}$ a $\Gamma\vdash t:\mathsf{Nat}$.
8. Ak $\Gamma\vdash\mathsf{iszero}\ t:R$, potom $R=\mathsf{Bool}$ a $\Gamma\vdash t:\mathsf{Nat}$.

V prípade abstrakcie volíme reprezentanta s parametrom čerstvým vzhľadom na $\Gamma$, aby bol rozšírený kontext platný. Teoréma opisuje, ktoré pravidlo mohlo viesť k danému úsudku a aké požiadavky boli splnené. Je spoločným základom uvažovania o jednoznačnosti typov, progrese aj stabilite.

Jednoznačnosť typov

Ako v NBL chceme, aby typovateľný term poskytoval jednoznačnú statickú informáciu. V STLC pritom musíme vždy určiť kontext: tá istá voľná premenná môže mať v rôznych kontextoch rôzne deklarácie.

Teoréma: O jednoznačnosti typov.

Nech $\Gamma$ je platný typový kontext, $t$ term a $T_1,T_2$ jednoduché typy. Ak $\Gamma\vdash t:T_1$ a $\Gamma\vdash t:T_2$, potom $T_1=T_2$:

$$ (\forall\Gamma,t,T_1,T_2)\bigl(\Gamma\vdash t:T_1\land\Gamma\vdash t:T_2 \ \Longrightarrow\ T_1=T_2\bigr). $$

Každý typovateľný term má v danom kontexte práve jeden typ. Podmienka jedinečnosti deklarácií je podstatná: T-Var nesmie pre jedno meno nájsť dva rozdielne typy. Teoréma nehovorí o počte typovacích derivácií ani netvrdí, že každý syntakticky správny term je typovateľný. Od jednoznačnosti typov odlíšime aj jednoznačnosť výpočtového kroku, ktorú vyjadruje deterministickosť.

Hodnota nevykonáva krok

Hodnota predstavuje hotový výsledok zvolenej stratégie. Potrebujeme preto výslovne uviesť, že po jej dosiahnutí už vyhodnocovacia relácia nepokračuje.

Lema: Hodnota nevykonáva krok.

Nech $v$ je hodnota rozšíreného STLC a $t$ term. Z hodnoty nemožno vykonať ďalší krok:

$$ (\forall v)\neg(\exists t)(v\to t). $$

Lema sa vzťahuje na gramatiku hodnôt a konkrétnu reláciu volania hodnotou. Napríklad abstrakcia $\lambda x:\mathsf{Nat}.\mathsf{pred}\;(\mathsf{succ}\ x)$ je hodnotou, hoci jej telo môže po dosadení argumentu pokračovať vo výpočte. Lema je dôležitá pri deterministickosti a pri jednoznačnosti dosiahnutej hodnoty.

Deterministickosť vyhodnotenia

Poradie vyhodnotenia má určovať najviac jeden nasledujúci stav. Táto požiadavka sa týka dynamickej sémantiky nezávisle od toho, či je term typovateľný.

Teoréma: Deterministickosť vyhodnotenia.

Nech $t,t_1,t_2$ sú termy rozšíreného STLC. Ak $t\to t_1$ a $t\to t_2$, potom $t_1=t_2$:

$$ (\forall t,t_1,t_2)\bigl(t\to t_1\land t\to t_2\ \Longrightarrow\ t_1=t_2\bigr). $$

Ak krok existuje, jeho výsledok je jednoznačný. Teoréma nezaručuje existenciu kroku ani ukončenie. Napríklad otvorená premenná $x$ nemá krok, čo deterministickosti neodporuje.

Rovnosť výsledkov rešpektuje zvolenú reprezentáciu termov. Pri práci až na $\alpha$-ekvivalenciu porovnávame ich triedy. Pri pomenovanej syntaxi a pevnom výbere čerstvého mena pre substitúciu z prvej prednášky je výsledný term určený aj doslovne. Deterministickosť spolu s tým, že hodnoty nevykonávajú krok, zabezpečuje jednoznačnosť dosiahnutej hodnoty, ak taká hodnota existuje.

Kanonické tvary hodnôt

Pred výpočtom nad už hotovým argumentom potrebujeme poznať jeho tvar. Typ funkčnej hodnoty napríklad musí zaručiť, že ide o abstrakciu, na ktorú možno použiť E-AppAbs.

Teoréma: O kanonických tvaroch hodnôt.

Nech $v$ je ľubovoľná uzavretá správne typovaná hodnota a $T_1,T_2$ jednoduché typy. Potom:

1. Ak $\vdash v:\mathsf{Bool}$, potom $v=\mathsf{true}$ alebo $v=\mathsf{false}$.
2. Ak $\vdash v:\mathsf{Nat}$, potom $v=0$ alebo $v=\mathsf{succ}\ nv$ pre numerickú hodnotu $nv$.
3. Ak $\vdash v:T_1\to T_2$, potom $v=\lambda x:T_1.t_2$ pre nejaké $x$ a $t_2$.

Formálne, s $v$ v kategórii hodnôt:

$$ \begin{aligned} (\forall v)\bigl(\vdash v:\mathsf{Bool}&\ \Longrightarrow\ v=\mathsf{true}\lor v=\mathsf{false}\bigr),\\ (\forall v)\bigl(\vdash v:\mathsf{Nat}&\ \Longrightarrow\ v=0\lor(\exists nv)(v=\mathsf{succ}\ nv)\bigr),\\ (\forall v,T_1,T_2)\bigl(\vdash v:T_1\to T_2&\ \Longrightarrow\ (\exists x,t_2)(v=\lambda x:T_1.t_2)\bigr). \end{aligned} $$

Tvrdenie charakterizuje syntaktické tvary hodnôt jednotlivých typov. Nehovorí, že typ určuje jediný výsledok: $\mathsf{true}$ aj $\mathsf{false}$ majú typ $\mathsf{Bool}$. Kanonické tvary spájajú statické požiadavky s tvarmi očakávanými dynamickou sémantikou a sú podstatné pre progres.

Progres

Pre samostatný správne typovaný program chceme zaručiť, že je hotovým výsledkom alebo môže pokračovať. Voľné premenné by túto záruku narušili, preto tvrdenie formulujeme v prázdnom kontexte.

Teoréma: O progrese.

Nech $t$ je term a $T$ jednoduchý typ. Ak $\vdash t:T$, potom $t$ je hodnota alebo existuje $t'$ také, že $t\to t'$:

$$ (\forall t,T)\bigl(\vdash t:T\ \Longrightarrow\ \operatorname{isvalue}(t)\lor(\exists t')(t\to t')\bigr). $$

Predpoklad uzavretosti je nevyhnutný. Úsudok $x:\mathsf{Nat}\vdash x:\mathsf{Nat}$ platí, ale samotná premenná $x$ nie je hodnotou a nemôže vykonať krok. Tento otvorený term nie je protipríkladom teorémy, pretože nespĺňa jej predpoklad $\vdash t:T$.

Progres vylučuje zaseknutie aktuálneho správne typovaného uzavretého stavu. O tom, či po kroku zostane výsledný term správne typovaný, ešte potrebujeme samostatné tvrdenie o stabilite typov.

Permutácia typového kontextu

Kontext uchováva typové predpoklady o premenných. Pri STLC typy v deklaráciách nezávisia od termových premenných, takže samotné poradie rôznych deklarácií nemá ovplyvniť typovanie.

Lema: O permutácii kontextu.

Nech $\Gamma,\Delta$ sú platné kontexty, $t$ term a $T$ jednoduchý typ. Označme $\operatorname{perm}(\Delta,\Gamma)$ tvrdenie, že $\Delta$ je permutáciou $\Gamma$. Potom:

$$ (\forall\Gamma,\Delta,t,T)\bigl(\Gamma\vdash t:T\land\operatorname{perm}(\Delta,\Gamma) \ \Longrightarrow\ \Delta\vdash t:T\bigr). $$

Permutácia znamená, že $\Delta$ obsahuje presne tie isté deklarácie s rovnakými typmi, iba prípadne v inom poradí. Oba kontexty naďalej spĺňajú jedinečnosť mien. Napríklad $f:A\to B,x:A$ a $x:A,f:A\to B$ umožňujú rovnaké typovanie termu $f\ x:B$.

Táto vlastnosť umožňuje usporiadať dostupné predpoklady podľa potreby. Spolu so zoslabením patrí medzi pomocné vlastnosti kontextu súvisiace so substitučnou lemou.

Zoslabenie

Pri typovej kontrole väčšieho výrazu môže byť dostupných viac deklarácií, než konkrétny podterm využíva. Pridanie nového predpokladu preto nesmie zrušiť už platné typovanie.

Lema: O zoslabení.

Nech $\Gamma$ je platný kontext, $t$ term, $x$ premenná a $T,S$ jednoduché typy. Ak $\Gamma\vdash t:T$ a $x\notin\operatorname{dom}(\Gamma)$, potom pre ľubovoľný jednoduchý typ $S$ platí:

$$ (\forall\Gamma,t,T,x,S)\bigl(\Gamma\vdash t:T\land x\notin\operatorname{dom}(\Gamma) \ \Longrightarrow\ \Gamma,x:S\vdash t:T\bigr). $$

Podmienka sa týka domény kontextu, nie všetkých syntaktických výskytov mena $x$ v terme. Z platného pôvodného typovania už vyplýva, že každá voľná premenná má deklaráciu v $\Gamma$. Viazané výskyty mena $x$ neprekážajú: v prípade konfliktu ich premenujeme pomocou $\alpha$-konverzie.

Napríklad $\vdash\lambda x:A.x:A\to A$ zostáva platným typovaním aj po pridaní deklarácie $x:S$, ak abstrakciu zastúpime $\alpha$-ekvivalentným termom $\lambda y:A.y$ s čerstvým $y$. Zoslabenie nemení typ termu; umožňuje jeho typovanie pri ďalších dostupných predpokladoch a súvisí s prácou pod abstrakciou pri substitúcii.

Substitučná lema

Pri $\beta$-redukcii nahrádzame typový predpoklad o parametri konkrétnym argumentom. Potrebujeme záruku, že pri zhodnom type dosadeného termu zostane typ tela zachovaný.

Lema: O substitúcii.

Nech $\Gamma,x:S$ je platný kontext, $t,s$ termy a $T,S$ jednoduché typy. Ak $\Gamma,x:S\vdash t:T$ a $\Gamma\vdash s:S$, potom:

$$ (\forall\Gamma,x,S,t,s,T)\bigl(\Gamma,x:S\vdash t:T\land\Gamma\vdash s:S \ \Longrightarrow\ \Gamma\vdash[x\mapsto s]t:T\bigr). $$

Kontext $\Gamma,x:S$ musí byť platný, teda $x\notin\operatorname{dom}(\Gamma)$, a substitúcia zabraňuje zachyteniu voľných premenných. Term $s$ nemusí byť hodnotou ani uzavretý: postačuje jeho typovanie v $\Gamma$.

Napríklad z $x:\mathsf{Nat}\vdash\mathsf{succ}\ x:\mathsf{Nat}$ a $\vdash 0:\mathsf{Nat}$ dostaneme typovanie výsledku substitúcie:

$$\vdash[x\mapsto 0](\mathsf{succ}\ x):\mathsf{Nat}, \qquad [x\mapsto 0](\mathsf{succ}\ x)=\mathsf{succ}\ 0.$$

Pri E-AppAbs je dosadzovaný term hodnotou správneho argumentového typu. Lema preto vyjadruje práve typovú vlastnosť potrebnú na spojenie $\beta$-redukcie so stabilitou typov. Permutácia a zoslabenie opisujú potrebnú prácu s kontextmi.

Stabilita typov

Dynamická sémantika term mení. Statická informácia získaná pred spustením však musí zostať platná aj po zmene, aby typová kontrola nebola potrebná po každom kroku.

Teoréma: O stabilite typu.

Nech $\Gamma$ je platný kontext, $t,t'$ termy a $T$ jednoduchý typ. Ak $\Gamma\vdash t:T$ a $t\to t'$, potom $\Gamma\vdash t':T$:

$$ (\forall\Gamma,t,t',T)\bigl(\Gamma\vdash t:T\land t\to t' \ \Longrightarrow\ \Gamma\vdash t':T\bigr). $$

Na rozdiel od progresu je táto formulácia platná aj pre otvorené termy v kontexte $\Gamma$. Po kroku zostáva rovnaký typ v rovnakom kontexte. Pri $\beta$-redukcii zodpovedá tejto požiadavke substitučná lema.

Výpočet aplikácie uzavretej abstrakcie ilustroval stabilitu konkrétnou postupnosťou termov typu $\mathsf{Nat}$. Teoréma má širší význam: vzťahuje sa na každý povolený krok správne typovaného termu rozšíreného jazyka. Sama osebe ešte nevylučuje zaseknutie, pretože jej predpoklad už obsahuje existujúci krok.

Typová bezpečnosť

Správny typ má chrániť program počas celého výpočtu. Bezpečnosť preto formulujeme pre ľubovoľný stav dosiahnutý konečnou postupnosťou krokov.

Dôsledok: Typová bezpečnosť.

Nech $t,t'$ sú termy a $T$ jednoduchý typ. Ak $\vdash t:T$ a $t\to^*t'$, potom:

• $t'$ je hodnota alebo existuje $t''$ také, že $t'\to t''$;
• zároveň platí $\vdash t':T$.

Formálne:

$$ (\forall t,t',T)\bigl(\vdash t:T\land t\to^*t'\ \Longrightarrow\ \vdash t':T\land\bigl(\operatorname{isvalue}(t')\lor(\exists t'')(t'\to t'')\bigr)\bigr). $$

Každý dosiahnutý stav teda má pôvodný typ a nie je zaseknutý. Progres zaručuje možnosť pokračovania pri správne typovanom uzavretom stave a stabilita typov zaručuje súlad typovania s vykonanými krokmi.

Bezpečnosť neznamená ukončenie ani výpočet zamýšľaného výsledku. Aj nekonečný výpočet by mohol spĺňať požiadavku, že každý jeho stav má správny typ a môže pokračovať. V skúmanom STLC nekonečný výpočet vylúči osobitná veta o normalizácii.

Silná normalizácia vzhľadom na volanie hodnotou

Po vylúčení zaseknutia ostáva otázka, či sa výsledku vôbec dočkáme. Táto otázka je od bezpečnosti odlišná a závisí aj od zvolenej vyhodnocovacej relácie.

Term je silne normalizujúci vzhľadom na reláciu $\to$, ak z neho neexistuje nekonečná redukčná postupnosť:

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

Teoréma: Silná normalizácia vzhľadom na volanie hodnotou.

Nech $t$ je term a $T$ jednoduchý typ. Ak $\vdash t:T$, potom je $t$ silne normalizujúci vzhľadom na deterministickú reláciu volania hodnotou $\to$ definovanú v tejto prednáške.

Označme $\operatorname{SN}_{\to}(t)$ tvrdenie, že z termu $t$ neexistuje nekonečná postupnosť krokov relácie $\to$. Potom:

$$ (\forall t,T)\bigl(\vdash t:T\ \Longrightarrow\ \operatorname{SN}_{\to}(t)\bigr). $$

Rozlišujeme tri požiadavky:

• Typová bezpečnosť vylučuje zaseknutie správne typovaného programu.
• Ukončenie znamená, že výpočet po konečnom počte krokov skončí.
• Silná normalizácia vzhľadom na danú reláciu vylučuje každú nekonečnú cestu, ktorú táto relácia povoľuje.

Pri našej deterministickej relácii je pokračovanie jednoznačné. V spojení s typovou bezpečnosťou normalizačný výsledok zaručuje skončenie v hodnote správneho typu. Výsledok sa vzťahuje na jazyk, ktorý sme definovali, bez pridania všeobecnej rekurzie.

Reláciu $\to$ treba odlišovať od úplnej $\beta$-redukcie $\to_\beta$ z predchádzajúcich prednášok. Volanie hodnotou nepovoľuje redukciu pod abstrakciou a vyžaduje hodnotový argument. Uvedená formulácia preto nie je automaticky tvrdením o všetkých postupnostiach úplnej $\beta$-redukcie ani o dosiahnutí úplnej $\beta$-normálnej formy.

Jednoznačný výsledok vyhodnotenia

Z praktického hľadiska chceme vedieť, či má každý prijatý uzavretý program výsledok, či je tento výsledok jediný a či zodpovedá pôvodnému typu.

Dôsledok: Jednoznačný výsledok vyhodnotenia.

Nech $t$ je term a $T$ jednoduchý typ. Ak $\vdash t:T$, potom existuje práve jedna hodnota $v$ taká, že:

$$ (\forall t,T)\bigl(\vdash t:T\ \Longrightarrow\ (\exists!v)(t\to^*v\land\vdash v:T)\bigr). $$

Kvantifikátor $\exists!$ vyjadruje existenciu práve jednej hodnoty; $v$ sa pohybuje v kategórii hodnôt.

Tvrdenie spája ukončenie, deterministickosť a stabilitu typov. Normalizácia spolu s bezpečnosťou zaručuje dosiahnutie hodnoty, deterministickosť jej jednoznačnosť a stabilita pôvodný typ. Napríklad uzavretá aplikácia:

$$ (\lambda x:\mathsf{Nat}.\mathsf{if}\ \mathsf{iszero}\ x\ \mathsf{then}\ \mathsf{succ}\ 0\ \mathsf{else}\ \mathsf{pred}\ x)\;(\mathsf{pred}\;(\mathsf{succ}\;(\mathsf{succ}\ 0))) $$

má jediný výsledok $0$ typu $\mathsf{Nat}$.

$\lambda$-kocka

STLC je východiskom viacerých teórií typov. $\lambda$-kocka Henka Barendregta opisuje osem systémov vznikajúcich kombináciou troch smerov rozšírenia. Slúži ako orientačná mapa ďalších prednášok.

Základný systém $\lambda_{\to}$ umožňuje, aby term závisel od termu: telo abstrakcie môže používať svoj termový parameter. Tri ďalšie závislosti zodpovedajú osiam kocky:

• Term závisí od typu: abstrakcia termu nad typom a aplikácia termu na typ prinášajú polymorfizmus.
• Typ závisí od termu: typ môže obsahovať termový parameter; ide o závislé typy.
• Typ závisí od typu: abstrakcia na úrovni typov umožňuje vytvárať typové operátory.

Na diagrame vodorovný smer pridáva závislé typy, zvislý polymorfizmus a šikmý typové operátory:

Tri susedné vrcholy základného systému majú osobitný význam: $\lambda P$ zavádza závislé typy, $\lambda 2$, známy ako Systém F, polymorfizmus a $\lambda\underline{\omega}$ typové operátory. Kombinácie dvoch smerov tvoria $\lambda P2$, $\lambda P\underline{\omega}$ a $\lambda\omega$. Podčiarknuté $\omega$ v $\lambda\underline{\omega}$ odlišujeme od $\lambda\omega$, ktorý navyše podporuje polymorfizmus.

Vrchol $\lambda C$ je Calculus of Constructions, kalkul konštrukcií. Nie je totožný s Calculus of Inductive Constructions, kalkulom induktívnych konštrukcií. Rocq je založený na rozšírení Calculus of Constructions o induktívne konštrukcie a ďalšie mechanizmy.

V ďalších prednáškach sa postupne budeme venovať polymorfizmu Systému F, typovým operátorom systému $\lambda\underline{\omega}$ a závislým typom systému $\lambda P$. Kocka zatiaľ ukazuje ich vzťahy; ich formálne pravidlá tu nezavádzame.

Zhrnutie

Statická sémantika analyzuje program bez vykonania; dynamická sémantika opisuje jeho výpočet. V NBL úsudok $t:T$ vyjadruje priradenie typu termu. Typy nemenia jeho syntax ani vyhodnocovacie pravidlá.

Pri STLC používame úsudok $\Gamma\vdash t:T$. Kontext $\Gamma$ uchováva typy dostupných premenných. Atómové typové konštanty z $\mathcal{A}$ odlišujeme od vstavaných základných typov z $\mathcal{B}$; v čistom kalkule je prázdna iba $\mathcal{B}$.

Funkčný typ $T_1\to T_2$ určuje typ argumentu a výsledku. T-Var použije deklaráciu premennej, T-Abs vytvorí funkčný typ z anotácie a typu tela a T-App overí zhodu argumentu s doménou. Rozšírenie o $\mathsf{Bool}$ a $\mathsf{Nat}$ umožní kombinovať funkcie so základnými údajmi.

Progres vylučuje zaseknutie správne typovaného uzavretého stavu. Stabilita typov zaručuje, že krok nemení typ. Spolu poskytujú typovú bezpečnosť. Samostatný výsledok o silnej normalizácii pri volaní hodnotou navyše zaručuje ukončenie; deterministickosť zabezpečuje jedinú výslednú hodnotu. STLC je v $\lambda$-kocke základom troch smerov rozšírenia: polymorfizmu, závislých typov a typových operátorov.

Kontrolné úlohy

Úlohy precvičujú typovacie pravidlá, vyhodnocovanie a porozumenie vlastnostiam typového systému.

1. Rozhodnite, ktoré termy NBL sú typovateľné, a určte ich typ: $\mathsf{succ}\;(\mathsf{pred}\ 0)$, $\mathsf{iszero}\;(\mathsf{succ}\ 0)$, $\mathsf{if}\ \mathsf{true}\ \mathsf{then}\ 0\ \mathsf{else}\ \mathsf{false}$. Pri neúspechu určte neodvoditeľnú premisu.

2. Zostrojte úplné typovacie stromy pre $\mathsf{iszero}\;(\mathsf{pred}\;(\mathsf{succ}\ 0))$ a $\mathsf{if}\ \mathsf{false}\ \mathsf{then}\ 0\ \mathsf{else}\ \mathsf{succ}\ 0$. Označte každé pravidlo.

3. Určte typy abstrakcií $\lambda x:A.\lambda y:B.x$ a $\lambda g:A\to B.\lambda x:A.g\ x$. Zostrojte ich typovacie stromy v prázdnom kontexte.

4. Nech $A,B,C$ sú navzájom rôzne atómové typové konštanty. Skontrolujte term $g\ z$ v kontextoch $g:A\to B,z:A$ a $g:A\to B,z:C$. Vysvetlite požiadavku pravidla T-App.

5. Premenujte term $\lambda x:A.\lambda x:A.x$ na $\alpha$-ekvivalentný term s rôznymi menami parametrov a určte jeho typ. Ktorý parameter označuje posledný výskyt $x$?

6. Vyhodnoťte nasledujúce aplikácie a pri každom kroku označte pravidlo:

   $$ \begin{gathered} (\lambda x:\mathsf{Nat}.\mathsf{if}\ \mathsf{iszero}\ x\ \mathsf{then}\ \mathsf{succ}\ 0\ \mathsf{else}\ \mathsf{pred}\ x)\;0,\\ (\lambda x:\mathsf{Nat}.\mathsf{if}\ \mathsf{iszero}\ x\ \mathsf{then}\ \mathsf{succ}\ 0\ \mathsf{else}\ \mathsf{pred}\ x)\;(\mathsf{succ}\;(\mathsf{succ}\ 0)). \end{gathered} $$

7. Vyhodnoťte $(\lambda x:\mathsf{Nat}.\mathsf{succ}\ x)\;(\mathsf{pred}\;(\mathsf{succ}\ 0))$. Určte typ každého medzitermu a vysvetlite, prečo najprv vyhodnocujeme argument.

8. Prečo úsudok $x:\mathsf{Nat}\vdash x:\mathsf{Nat}$ neprotirečí progresu? Ktorý predpoklad teorémy tento príklad nespĺňa?

9. Slovne odlíšte jednoznačnosť typov, deterministickosť vyhodnotenia, typovú bezpečnosť a silnú normalizáciu vzhľadom na $\to$. Ktoré tvrdenie zabezpečuje typ po kroku a ktoré vylučuje nekonečný výpočet?

10. Pomocou tabuľky $\lambda$-kocky porovnajte $\lambda P$, $\lambda 2$, $\lambda\underline{\omega}$ a $\lambda\omega$. Pomenujte závislosti, ktoré pridávajú k STLC.