Teorija programskih jezikov (Pretnar)

Podatkovne tipe specificiramo z indukcijo.

i.e. simply-typed \(\lambda\)-calculus (STLC).

Rekurzijo moramo dotati eksplicitno.

Preverimo lahko, da varnost še velja, normalizacija pa ne.

Zakaj bi sploh imeli denotacijsko semantiko?

\noindent To nas motivira, da uvedemo kontekstno ekvivalenco.

\noheading Podobno lahko pokažemo da je \[ M \simeq N \iff \left( \forall \mathcal{C} .\, \mathcal{C}[M] \leadsto^{ * } \underline{n} \leadsto \mathcal{C}[N] \leadsto^{ * } \underline{n}\right) \] ali celo \[ M \simeq N \iff \left( \forall \mathcal{C} .\, \mathcal{C}[M] \text{ konvergira} \iff \mathcal{C}[N] \text{ konvergira} \right). \]

Kontekstna ekvivalenca je zelo močno orodje, vendar je zelo težko kvantificirati čez vse kontekste.

Vidimo, da za interpretacije rekurzivnih funkcij potrebujemo fiksne točke (skoraj vseh) preslikav. Ideja konstrukcije \(\mu f\) za nek Scottovo zvezen funktor \(F\) nas pripelje do domen.

\noindent NB to je v resnici \(\omega\)-continuous partial order domain. Urejenost si predstavljamo kot "več informacij". \(\bot\) je nikjer definirana, kar pomeni da ima nič informacij. true in false sta oba definirana, a "nosita enako informacij" zato sta neprimerljiva. Funkcija, ki je nekje nedefinirana nosi manj informacij kot funkcija, ki se z njo ujema na prvotni domeni in ima več definiranih vrednosti.

\noindent Vsak tip \(\llbracket A \rrbracket\) lahko interpretiramo z domeno \(\llbracket A \rrbracket\) tako da dodamo \(\bot\).

kjer je \([D_1 \rightarrow D_2]\) domena vseh zveznih funkcij \(D_1 \rightarrow D_2\) urejene po točkah.

Kontekst interpretiramo s produktom \[ \llbracket x_1 : A, \dots, x_n : A_n \rrbracket = \llbracket x_1 : A \rrbracket \times \dots \times \llbracket x_n : A_n \rrbracket \] Tedaj lahko vsak izraz \(\Gamma \vdash M : A\) interpretiramo z zvezno preslikavo \(\llbracket \Gamma \vdash M : A \rrbracket : \llbracket \Gamma \rrbracket \rightarrow \llbracket A \rrbracket\).

Torej je

Nimamo pa zadostnosti. Na primer, velja \[ \llbracket (\lambda .\, \mathtt{true})(\Omega) \rrbracket = \mathit{tt} \] ampak ta izraz ne bo prišel do true v končno mnogo korakih. Problem rešimo tako, da definiramo \[ \llbracket \lambda x.\, M \llbracket(\gamma) = a \mapsto \begin{cases} \bot & a = \bot \\ \llbracket M \rrbracket(\gamma, a) \end{cases} \] ker želimo zadostnost. Uporabimo torej stroge funkcije. \[ \llbracket M + N \rrbracket(\gamma) = \begin{cases} \bot & \text{če } \llbracket M \rrbracket = \bot \lor \llbracket N \rrbracket = \bot \\ \llbracket M \rrbracket + \llbracket N \rrbracket & \text{sicer} \end{cases} \] Končno definiramo še rekurzivne funkcije. \[ \llbracket \mathtt{rec}\, f\, x .\, M \rrbracket(\gamma) = \mu \Phi \] kjer je \[ \Phi(g) = a \mapsto \llbracket M \rrbracket(\gamma, g, a) \] oziroma \[ \mu g .\, a \mapsto \llbracket M \rrbracket(\gamma, g, a). \]

Za vse primere moramo pokazati, da dobimo zvezne funkcije. Oglejmo si rekurzijo. Najprej moramo pokazati, da imamo zvezno funkcijo.

Če imamo množice \(X_1, \dots, X_n\) in \(Y_i\) za vse parametre \(\alpha_1, \dots, \alpha_n\) ter relacije \(R_i \subseteq X_i \times Y_i\), lahko definiramo relacije \( \llbracket A \rrbracket_{\vec{R}} \subseteq \llbracket A \rrbracket_{\vec{X}} \times \llbracket A \rrbracket_{\vec{Y}}\) za poljuben tip \(A\) kot

Programe \(M : A \rightarrow B\) smo intepretirali s funkcijami \(\llbracket A \rrbracket \rightarrow \llbracket B \rrbracket\). Toda programi lahko sprožajo učinke (branje/pisanje z IO naprav, naključna izbira, izjeme, nedeterminizem, ipd.), ki jih funkcije ne zajamejo.

Za začetek si oglejmo operacijsko semantiko. Najprej si prilagodimo osnovni jezik. Zaradi učinkov želimo neučakano izvajanje.

\noindent Ta pristop je znan pod imenom "A-normal form". Poskrbi, da je vedno natanko ena točka izvajanja. Ideja je podobna SSA.

Oglejmo si operacijsko semantiko.

S tem zapisom se bistveno zmanjša število pravil na vsakem koraku.

Podati moramo še pravila za tipe \(\Gamma \vdash V : A\) in \(\Gamma \vdash M : A\) Večinoma imamo običajna pravila

Če imamo programe, ki lahko sprožijo učinke, i.e. \(\Gamma \vdash_C M : A! \mathcal{E}\), dobimo

Imamo standardni izreke o varnosti, ohranitvi, in napredku.

Recimo, da tip \(A\) interpretiramo z množico \(\llbracket A \rrbracket\). Tedaj lahko vrednost interpretiramo kot prej \[ \llbracket \Gamma \vdash_V V : A \rrbracket : \llbracket \Gamma \rrbracket \rightarrow \llbracket A \rrbracket \] izračune pa odvisno od učinka.

Ideja od zadnjič je, da vsak učinek zapišemo z algebrajsko teorijo. Algebrajska teorija je množica operacij in enačb med njimi.

Zakodiramo lahko tudi druge stvari, recimo pomnilnik z eno logično vrednostjo. Imeli bomo 3 operacije. Namesto da imamo \(\operatorname{get} : \operatorname{unit} \rightarrow \operatorname{bool} \), našemu \(\operatorname{get}\) podamo dve kontinuaciji glede na vrednost pomnilnika.

let _ = (set0 ∨ set1)
let x = get
return x + 2

Primer modela za to teorijo je \(\mathbb{B} \rightarrow \mathbb{B}\);

Potem je recimo

Izračune interpretiramo v prostem modelu. Naredimo kvocient množice vseh izrazov/dreves glede na enačbe teorije. Pri nedeterminizmu vidimo, da je \(F X = \pot_{\operatorname{fin} X}\).

Kaj je prosti model za teorijo pomnilnika? Normalna oblika izrazov je \[ \operatorname{get}(\operatorname{set}_a(x), \operatorname{set}_b(y)) \] in dobimo \[ FX \cong (\mathbb{B} \times X)^2 \cong \mathbb{B} \rightarrow \mathbb{B} \times X \]

Z algebrajskimi teorijami se izognemu težavam z monadami. Specifično, komponiranje deluje. Vzamemo unijo obeh teorij in dodamo potencialne enačbe za interakcijo. Oglejmo si še operacijsko semantiko.

Učinke opisujemo z operacijami \((\operatorname{op} : P \rightarrow A) \in \Sigma\), eg

Imamo \(M \Coloneqq \operatorname{op}(V; \, x.\, M)\), kjer je \(V\) parameter, \(M\) pa kontinuacija. Pravila so

Velja izrek o varnosti.

Definiramo okrajšavo (generični učinek) \[ \underline{\operatorname{op}}(V) \coloneqq \operatorname{op}(V;\, x . \operatorname{return} x). \] Tedaj je \[ \operatorname{op}(V;\, x. \operatorname{M}) \cong \operatorname{let} x = \underline{\operatorname{op}}(V) \operatorname{in} M \]

Alternativi za operacijsko semantiko so

• Veliki koraki \(M \Downarrow R\), kjer je \[ R \Coloneqq \operatorname{return} V \mid \operatorname{op}(V; \, (R_i)_i) \] in

  \begin{gather*} \begin{bprooftree} \AxiomC{\(M[V_i / x] \Downarrow R_i\)} \AxiomC{za vse vrednosti \(V_1,\dots\) iz členosti operacij} \BinaryInfC{\(\operatorname{op}(V;\, x. \operatorname{M} \Downarrow \operatorname{op}(V;\, (R_i)_i))\)} \end{bprooftree} \end{gather*}

• Srednji koraki:

  \begin{prooftree} \AxiomC{\(\text{za vsako vrednost}\vdash W : A\)} \UnaryInfC{\(\operatorname{op}(V;\, x. \operatorname{M}) \xrightarrow{\operatorname{op} V!W} M[W/x]\) } \end{prooftree}

  kjer se je vmes zgodila operacija \(\operatorname{op}\) s parametrom \(V\) in rezultatom \(W\).

Imamo težavo. Kakšna je teorija za učinek izjem? Spomnimo se, da smo imeli

Monada je bila \(TX = X + 1\). Poskusimo z \[ \Sigma = \operatorname{raise} : o, \operatorname{try} : 2 \] in enačbo \(\operatorname{try}(\operatorname{raise}(), y) = y\). Problem je, da se \(\operatorname{try}\) ne obnaša enako kot ostale operacije, ker imamo \[ \operatorname{let} x = \operatorname{try}(M_1, M_2) \operatorname{in} N \not\cong \operatorname{try}(\operatorname{let} x = M_1 \operatorname{in} N, \operatorname{let} x_2 = M_2 \operatorname{in} N \] recimo za \(M_1 = M_2 = \operatorname{ret} 0\) in \(N = \operatorname{let} x = \operatorname{print}(42)\) in \(\operatorname{raise}()\).

Toda, že prosti model za \(\Sigma = \left\{ \operatorname{raise} : _0 \right\}\) nam da monado za izjeme \[ FX = \left\{ [x] \mid x \in X \right\} \cup \left\{ [ \operatorname{raise}()] \right\} \cong X + 1 \] Torej ima \(\operatorname{try}\) drugačno vlogo. Če ni operacija, kaj je?

Imejmo izjeme \(E_1, \dots, E_n\) in prestreznik \[ \operatorname{try} M \operatorname{with} E_1 \rightarrow M_1 \mid \cdots \mid E_n \rightarrow M_n. \] Alg. teorija je \(\left\{ E_1 : 0, \dots, E_n : 0 \right\}\).

Prestreznik nam za vsako izjemo da nadomestno vrednost. Ni samo funkcija \(\left\{ E_i \right\} \rightarrow \) ampak ga lahko vidimo tudi kot model teorije. V splošnem je model \[ M, (\llbracket \operatorname{op} \rrbracket : M^n \rightarrow M)_{\operatorname{op} : n \in \Sigma}. \] skupaj z enačbami, za izjeme pa imamo \[ (M, (\llbracket E_i \rrbracket : \underline{M^0 \rightarrow M}_{\cong M}))_{i=1,\dots, n} \]

See also (Pretnar, Matija, 2015).

Vsak element prostega modela \(FX\) lahko interpretiramo v poljubnem drugem modelu na \(X\), recimo \[ [m(i(4), m(e(), 3))] \] lahko interpretiramo v \((\Z, +, -, 0)\) kot \(-4 + (0 + 3) = -1\). V splošnem je model lahko tudi nad drugo množico \(Y\), če imamo preslikavo \(X \rightarrow Y\). Na primer \(f : \Z \rightarrow \Q\), \(f(m) = \frac{1}{1 + m^2}\). S tem naša interpretacija postane \[ \frac{1}{f(4)} \cdot (1 \cdot f(3)) = 17 \cdot \left(1 \cdot \frac{1}{1 + 3^{2}}\right) = \frac{17}{10} \] Prosti model ima univerzalno lastnost. Za vsak \(f : X \rightarrow Y\) in model \(Y\) imamo enolično določen homomorfizem \(h : FX \rightarrow Y\), da velja

\[\begin{tikzcd} FX && Y \\ \\ X \arrow["h", dashed, from=1-1, to=1-3] \arrow[hook', from=3-1, to=1-1] \arrow["f"', from=3-1, to=1-3] \end{tikzcd}\] Še več, vsi homomorfizmi \(FX \rightarrow Y\) so porojeni na ta način. Za vsako teroijo \(\mathcal{T}\) imamo kategorijo \(\underline{\mathbf{Mod}}_{\mathcal{T}}\) njenih modelov in homomorfizmov med njimi.

Imamo pozabljivi funktor \(U : \underline{\mathbf{Mod}}_{\mathcal{T}} \rightarrow \mathbf{Set}\) in ta funktor ima levi adjunkt \(F : \mathbf{Set} \rightarrow \underline{\mathbf{Mod}}_{\mathcal{T}}\). Imamo adjunkcijo \(F \vdash U\). Kompozicija \(UF\) je prosta monada, s katero smo delali ves čas.

Vse skupaj je interretacija \(F \llbracket A \rrbracket\) v modelu \(\left\{ E_1 \rightarrow M_1, \dots \right\} : A\). To je le poseben primer za identiteto. Pripeljimo še našo preslikavo \(f : FX \rightarrow Y\). Dobimo

Teorija za izjeme je najenostavnejša algebrajska teorija za učinke. Kaj so modeli drugih teorij? V splošnem je to \[ (M, (\llbracket \operatorname{op} \rrbracket : M^n \rightarrow M)_{(\operatorname{op} : n) \in \Sigma}) \] z razširjenimi operacijami pa \[ (M, (\llbracket \operatorname{op} \rrbracket : \llbracket P \rrbracket \times M^{\llbracket A \rrbracket} \rightarrow M)_{(\operatorname{op} : P \rightarrow A) \in \Sigma}) \] Prestreznike posplošimo na obliko