Funktsionaalprogrammeerimine 2024/25 sügis

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.