Lihtsalt tüübitud {$\lambda$}-arvutus
Tüübid spetsifitseerivad programmide omadusi.
- {$\lambda$}-arvutuses klassifitseerivad normaalkujusid.
- Kui term on tüüpi {$\text{Nat}$}, ja ta on normaalkujul, siis see term esitab naturaalarvu.
Tüübisüsteem koosneb kolmest komponendist:
- tüüpide hulk;
- programmide hulk;
- tüüpimisreeglid.
Olgu antud loenduv hulk tüübimuutujaid (baastüübid). (Lihtsad tüübid = ei ole polümorfsed.)
Lihtsate tüüpide süntaks
{$ \begin{array}{lcl@{\hspace{5em}}l} \tau & ::= & \alpha & \mbox{tüübimuutuja} \\ & \mid & \tau_1 \to \tau_2 & \mbox{funktsioonitüüp} \end{array} $}
Tüübikonstruktor {${\to}$} on paremassotsiatiivne. {$ \tau_1 \to \tau_2 \to \tau_3 \equiv \tau_1 \to (\tau_2 \to \tau_3) $}
Church vs. Curry
Tüüpidega {$\lambda$}-avaldiste esitamiseks on kaks peamist stiili.
- Church'i stiil: funktsiooni parameetrite tüübid esitatakse ilmutatult {$\lambda$}-termis {$\lambda x : \tau.\ e$}.
- Näiteks: {$\lambda x : \text{Nat}.\ x + x : \text{Nat} \to \text{Nat}$}.
- Igal termil on unikaalne tüüp.
- Curry stiil: termid on tavalised (s.o. ilma tüüpideta) ja kasutatakse tüübikorrektsuse predikaati (tüübituletus).
- Näide: {$\lambda x.\ x + x : \text{Nat} \to \text{Nat}$}.
- Termidel on palju tüüpe (näit. {$\lambda x.\ x : \text{Nat} \to \text{Nat}$}, kuid ka {$\lambda x.\ x : \text{Bool} \to \text{Bool}$}).
Meie kasutame põhiliselt esimest stiili.
Termid ja redutseerimine
Termide süntaks:
{$ \begin{array}{lcl@{\hspace{5em}}l} e & ::= & x & \mbox{muutuja} \\ & \mid & e_1\,e_2 & \mbox{aplikatsioon} \\ & \mid & \lambda x : \tau.\, e & \mbox{abstraktsioon} \end{array} $}
Sarnased süntaktilised konventsioonid kui puhtas {$\lambda$}-arvutuses. Väike erinevus sulgudest hoidumises: {$$ \begin{array}{lcl} \lambda x_1 : \tau_1, \ x_2 : \tau_2, \ \ldots,\ x_n : \tau_n, .\ e & \equiv & (\lambda x_1 : \tau_1, .\ (\lambda x_2 : \tau_2, .\ (\ldots(\lambda x_n : \tau_1, .\ e)\ldots)) \end{array} $$}
Näited: {$$ \begin{array}{l@{\hspace{7em}}l} \lambda x : \tau .\ x \;\;\;& ((\lambda x : \tau .\ (\lambda f : \tau\to\tau.\ f\ x))\ y)\,(\lambda z:\tau\to\tau.\ z) \end{array} $$}
Substitutsioon, reduktsioon jmt on defineertud analoogselt puhta {$\lambda$}-avutusega ignoreerides tüübiannotatsioone.
Tüüpimisrelatsioon
Et teha kindlaks mis termid on millist tüüpi, defineerime tüüpimisrelatsiooni.
Baasrelatsioon on kujul {$\Gamma \vdash e : \tau$}
- term {$e$} on tüüpi {$\tau$} kontekstis {$\Gamma$}.
Kontekst {$\Gamma$} on muutujast ja tüübist koosnevate paaride jada {$\Gamma = \{x_1:\tau_1,\ \ldots,\ x_n:\tau_n\}$}.
- Konteksti {$\Gamma$} domeeni (i.k. domain) tähistame
{$\text{dom}(\Gamma) = \{x_1,\ \ldots,\ x_n\}$}.
- Korrektses tüüpimisrelatsioonis peab olema {$\text{fv}{e} \subseteq \text{dom}(\Gamma)$}.
{$\Gamma \leq \Delta$} tähendab, et kui {$x \in \text{dom}(\Gamma)$}, siis {$x \in \text{dom}(\Delta)$} ja {$\Gamma(x) = \Delta(x)$}.
Programm (s.o. kinnine term) {$e$} on tüüpi {$\tau$}, kui tal on see tüüp tühjas kontekstis: {$\vdash e : \tau$}.
Tüüpimisreeglid
Tüüpimisrelatsioon on defineeritud tüüpimisreeglite abil.
Lihtsalt tüübitud {$\lambda$}-arvutuse tüüpimisreeglid:
{$$ \color{blue}{ \frac{}{\Gamma, x:\tau \vdash x : \tau} var \qquad \qquad \frac{\Gamma, x:\sigma \vdash e : \tau} {\Gamma \vdash \lambda x : \sigma.\,e : \sigma \to \tau} abs } $$}
{$$ \color{blue}{ \frac{\Gamma \vdash e_1 : \sigma \to \tau \quad \Gamma \vdash e_2 : \sigma} {\Gamma \vdash e_1\,e_2 : \tau} app } $$}
kus {$\color{blue}{x \not\in\text{dom}(\Gamma)}$}.
Edaspidi tähistame lihtsalt tüübitud {$\lambda$}-arvutust {$\lambda{\to}$}.
Tüübiohutus
Korrektselt tüübitud programmid ei lähe valesti.
Hind:
- Mõned mõistlikud programmid hüljatakse.
Koosneb kahest osast:
- Progress: Korrektselt tüübitud ei ole tupikus (ta on kas väärtus või saab teha ühe väärtustusreeglitele vastava sammu).
- Säilitamine: Kui korrektselt tüübitud term teeb ühe sammu, siis ka resultaat on korrektselt tüübitud.
Tüüpide unikaalsus, säilimine ja progress
Tüüpide unikaalsus: Kui {$\Gamma \vdash e : \tau_1$} ja {$\Gamma \vdash e : \tau_2$}, siis {$\tau_1 = \tau_2$}.
NB! Tüüpide unikaalsus ei kehti mitmete rikkamate keelte korral.
Tüüpide säilimine (subjekt-reduktsioon): Kui {$\Gamma \vdash e : \tau$} ja {$e \twoheadrightarrow e'$}, siis {$\Gamma \vdash e' : \tau$}.
Progress: Kui {$\Gamma \vdash e : \sigma$}, siis {$\exists e' : \sigma. e \rightarrow_\beta e'$} või {$e \in \mathrm{Val}$}, kus {$ v \in \mathrm{Val}\ ::=\ x\,v\,\ldots\,v \mid \lambda x{:}\tau.v $}
Tugev normaliseerimine: Lihtsalt tüübitud {$\lambda$}-arvutuses {$\lambda{\to}$} on iga {$\beta$}-reduktsiooni jada lõplik.
Mõned lihtsad järeldused:
- Termide võrdsuse küsimus on lahenduv.
- Püsipunktikombinaatorid ei ole defineeritavad.