Teorija programskih jezikov (Pretnar)
Lecture 1: Praksa programskih jezikov
Razlika med tem kako je jezik implementiran in kako je standardiziran.
Sintaksa opisuje kako napišemo programe. Semantika opisuje kaj pomenijo.
Konkretna sintaksa: zaporedja črk, ki jih zapišemo (besedilo). Abstraktna sintaksa: syntax trees (AST - abstract syntax tree).
Semantiko lahko podajamo na različne načine.
- Specificirano z implementacijo
- Specificirano s prozo
- Specificirano z matematičnimi simboli
- Specificirano z matematičnimi objekti (denotacijska semantika)
- Razčlenjevalnik (Parser): Prevodba iz konkretne sintakse v abstraktno sintakso (AST)
- Obogatitev drevesa: Preverjanje tipov, optimizacija, ipd.
- Interpreter/Compiler: Tolmačimo ali prevedemo v drug jezik/strojno kodo
Najpreprostejši učni jezik za definicijo semantike.
Implementirali smo type checker.
Lecture 2: Indukcija
Podatkovne tipe specificiramo z indukcijo.
\(\N\) je definirana kot najmanjša množica, kjer je
- \(0 \in \N\)
- \(n \in \N \implies n^{ + } \in \N\)
To zapišemo tudi s pravili izpeljave:
\begin{gather*} \begin{bprooftree} \AxiomC{} \UnaryInfC{\(0 \in \N\)} \end{bprooftree} \quad \begin{bprooftree} \AxiomC{\(n \in \N\)} \UnaryInfC{\(n^{ + } \in \N\)} \end{bprooftree} \end{gather*}Aritmetične izraze lahko podamo kot \[ e ::= \underline{n} \mid -e \mid e_1 + e_2 \mid e_1 * e_2, \] ali s pravili izpeljave:
\begin{gather*} \begin{bprooftree} \AxiomC{\(n \in \Z\)} \UnaryInfC{\(\underline{n} \in \mathbb{E}\)} \end{bprooftree} \quad \begin{bprooftree} \AxiomC{\(e \in \mathbb{E}\)} \UnaryInfC{\(-e \in \mathbb{E}\)} \end{bprooftree} \quad \begin{bprooftree} \AxiomC{\(e_1 \in \mathbb{E}\)} \AxiomC{\(e_2 \in \mathbb{E}\)} \BinaryInfC{\(e_1 + e_2 \in \mathbb{E}\)} \end{bprooftree} \quad \begin{bprooftree} \AxiomC{\(e_1 \in \mathbb{E}\)} \AxiomC{\(e_2 \in \mathbb{E}\)} \BinaryInfC{\(e_1 * e_2 \in \mathbb{E}\)} \end{bprooftree} \end{gather*}Z drevesom izpeljave lahko ekonomično pišemo dokaze vsebovanosti.
Induktivna definicija sodosti naravnih števil:
\begin{gather*} \begin{bprooftree} \AxiomC{} \UnaryInfC{\(0\) je sodo} \end{bprooftree} \quad \begin{bprooftree} \AxiomC{\(n\) je sodo} \UnaryInfC{\(n^{ ++ }\) je sodo} \end{bprooftree} \end{gather*}Induktivna definicija relacije manjšega ali enakosti:
\begin{gather*} \begin{bprooftree} \AxiomC{} \UnaryInfC{\(n \leq n\)} \end{bprooftree} \quad \begin{bprooftree} \AxiomC{\(m \leq n\)} \UnaryInfC{\(m \leq n^{ + }\)} \end{bprooftree} \end{gather*}Alternativna (ekvivalentna) definicija:
\begin{gather*} \begin{bprooftree} \AxiomC{} \UnaryInfC{\(0 \leq n\)} \end{bprooftree} \quad \begin{bprooftree} \AxiomC{\(m \leq n\)} \UnaryInfC{\(m^{ + } \leq n^{ + }\)} \end{bprooftree} \end{gather*}Obe definiciji podata ekvivalentno relacijo.
Induktivno relacijo \(R \subseteq X\) lahko predstavimo z družino induktivnih množic \((D_x)_{x \in X}\), kjer \(D_x\) predstavlja množico dokazov, da je \(x \in R\).
Obratno, iz vsake družine \((D_x)_{x \in X}\) lahko definiramo relacijo \(R \subseteq X\) kot \[ R = \left\{ x \in X \mid D_x \neq \emptyset \right\}. \]
Definirajmo družino \((S_n)_{n \in \N}\) s pravili
\begin{gather*} \begin{bprooftree} \AxiomC{} \UnaryInfC{\(\text{NicSodo} \in S_{0}\)} \end{bprooftree} \quad \begin{bprooftree} \AxiomC{\(d \in S_n\)} \UnaryInfC{\(\text{NaslNaslSodo } d \in S_{n^{ ++ }}\)} \end{bprooftree} \end{gather*}Elementi \(S_n\) so dokazni drevesi, da je \(n\) sodo.
Pri aritmetičnih izrazih:
- Ker imamo konstante, moramo imeti vsaj \(I_0 = \{\underline{n} \mid n \in \Z\}\)
- Zaradi pravila \(\operatorname{Plus}\) imamo tudi \((\underline{0} + \underline{0}) \in I_1\), podobno za \(\operatorname{Krat}\) in \(\operatorname{Minus}\)
- Iz teh dobimo dodatne elemente, kot so \(((\underline{0} + \underline{0}) * \underline{0}) \in I_2\)
Ideja je, da na vsakem koraku iz do sedaj zgrajenih elementov \(I_n\) dobimo množico \(I_{n+1}\). To konstrukcijo bomo opisali s funktorjem.
Naravna števila predstavimo s funktorjem \[ FX = 1 + X \]
Tu \(X\) predstavlja že sestavljene elemente. Iterirana aplikacija predstavlja dodajanje vseh novih izrazov na danem koraku:
- \(I_0 = \emptyset\)
- \(I_1 = 1 + \emptyset = \{\iota_0(\cdot)\}\)
- \(I_2 = 1 + I_1 = \{\iota_0(\cdot), \iota_1(\iota_0(\cdot))\}\)
- \(I_3 = 1 + I_2 = \{\iota_0(\cdot), \iota_1(\iota_0(\cdot)), \iota_1(\iota_1(\iota_0(\cdot)))\}\)
In tako dalje. Pišemo \(\iota_0(\cdot) = 0\) in \(n^{ + } = \iota_1(n)\).
Aritmetične izraze predstavimo s funktorjem \[ FX = \Z + X + 2X^2 \]
kjer \(\Z\) predstavlja konstante, \(X\) unarni operatorji in \(2X^2\) binarni operatorji.
Naj bo \(F\) funktor, ki je monoton in Scottovo zvezen. Potem ima \(F\) najmanjšo fiksno točko, ki jo označimo z \(\mu F\).
Monotonost: \(X \subseteq Y \implies FX \subseteq FY\)
Scottova zveznost: \[ F\left(\bigcup_{i=1}^{\infty} X_i\right) = \bigcup_{i=1}^{\infty} FX_i \]
Najmanjša fiksna točka je \[ \mu F = \bigcup_{i=1}^{\infty} F^i \emptyset \]
To je najmanjša množica, zaprta za \(F\): \[ FX \subseteq X \implies \mu F \subseteq X \]
Opomba: Potenčna množica ni Scottovo zvezna.
Pišimo \(I_0 = \emptyset\) in \(I_{n+1} = FI_n\) ter \(I = \bigcup_{i=1}^{\infty} I_i\).
Najprej pokažimo, da je \(\mu F\) fiksna točka.
\textit{(1) \(I \subseteq FI\)):}
Imamo \(I_0 = \emptyset \subseteq I_1\), zato je po monotonosti tudi \(I_1 = F\emptyset \subseteq FI_1 = I_2\), in tako dalje. Zato \(I_n \subseteq FI_n\) za vsak \(n\). Potem je \[ I = \bigcup_j I_j \subseteq \bigcup_j FI_j \subseteq FI. \]
Zadnja inkluzija velja, ker je \(I_j \subseteq I\) za vsak \(j\), zato je \(FI_j \subseteq FI\) po monotonosti, torej tudi \(\bigcup_j FI_j \subseteq FI\).
\textit{(2) \(FI \subseteq I\)):}
Naj bo \(x \in FI\). Po definiciji \(x\) nastane iz končno mnogo elementov \(I_k\) za neki fiksni \(k\). Zato je \(x \in FI_k = I_{k+1} \subseteq I\). Torej \(FI \subseteq I\).
\textit{(3) Minimalnost:} Če je \(FX \subseteq X\), je \(I \subseteq X\).
Imamo \(\emptyset \subseteq X\). Ker je \(F\emptyset \subseteq FX \subseteq X\), je \(I_1 \subseteq X\). Induktivno, če je \(I_j \subseteq X\), je \(I_{j+1} = FI_j \subseteq FX \subseteq X\). Zato je \[ I = \bigcup_{j=1}^{\infty} I_j \subseteq X. \]
Lecture 3: Indukcija 2
Lastnost \(\mu F\) lahko uporabimo za dokazovanje z indukcijo.
Naj bo \(P \subseteq \mu F\) zaprta za \(F\), torej \(FP \subseteq P\). Po izreku sledi \(P = \mu F\).
\(P \subseteq \N\) naj bo nek predikat na \(\N\), zaprt za \(F : X \rightarrow 1 + X\). Razpišim \(FP \subseteq P\).
\begin{align*} FP &\subseteq P \\ n \in FP &\implies n \in P \\ n \in 1 + P &\implies n \in P \\ n = \iota_0( * ) \lor \exists m \in P . \, n \iota_1(n) & \implies n \in P \end{align*}To pomeni, da imamo \[ 0 \in P \lor \forall m \in \N \implies m \in P \implies m^{ + } \in P \] Rekonstruirali smo načelo indukcije za naravna števila.
Konstrukcija primitivne rekurzije
S pomočjo funktorja \(F\) lahko izrazimo tudi primitivno rekurzivne funkcije na \(\mu F\).
Recimo, za \(\operatorname{ev} : \mathbb{E} \rightarrow \Z\) imamo
\begin{align*} \operatorname{ev}(\underline{n}) &= n \operatorname{ev}(e_1 + e_2) &= \operatorname{ev}(e_1) + \operatorname{ev}(e_2) \operatorname{ev}(e_1 * e_2) &= \operatorname{ev}(e_1) \cdot \operatorname{ev}(e_2) \operatorname{ev}(-e) &= -\operatorname{ev}(e) \end{align*}NB primitivno rekurzivna funkcija je podana že s štirimi funkcijami:
\begin{align*} \alpha_{1} &: \N \rightarrow \Z \alpha_{2} &: \Z \times \Z \rightarrow \Z \alpha_{3} &: \Z\times \Z\rightarrow \Z \alpha_{4} &: \Z \rightarrow \Z \end{align*}kar lahko predstavimo ravno s preslikavo \[ \alpha : \N + \Z \times \Z + \Z \times \Z + \Z \rightarrow \Z. \] To je ravno \(F\Z\). To je algebra za funktor \(F\).
Algebra za funktor \(F\) je
- Množica \(X\)
- Preslikava \(\alpha : FX \rightarrow X\)
Homomorfizem algebr je homomorfizm algebr.
Trditev: Obstoj začetne algebre.
Algebra \((\mu F, \operatorname{id} : \mu F = F \mu F \rightarrow F \mu F)\) je začetna algebra za \(F\). Za poljubno algebro \(X, \alpha\) obstaja enoličen homomorfizem \(\alpha : \mu F \rightarrow X\).
Lecture 3: Metateorija programskih jezikov
Za množico lokacij \(l \in \mathbb{L}\) definiramo sinkakso jezika
\begin{align*} e &::= \underline{n} \mid e_1 + e_2 \mid e_1 * e_2 \mid -e \mid l \\ b &::= \texttt{true} \mid \texttt{false} \mid e_1 < e_2 \mid e_1 = e_2 \mid e_1 > e_2 \\ c &::= \text{skip} \mid c_1 ; c_2 \mid \text{if } b \text{ then } c_1 \text{ else } c_2 \mid l := e \mid \text{while } b \text{ do } c \end{align*}Semantiko izrazov bomo podali operacijsko – prek relacij, ki bodo opisale korake računanja. Imamo dve različici.
- Mali koraki: \((2 + 4) * 7 \rightsquigarrow 6 * 7 \rightsquigarrow 42\)
- Veliki koraki: \((2 + 4) * 7\ \rightsquigarrow 42)
Imp - Semantika
Naj bo \(\mathbb{S} = \Z_{\bot}^{\mathbb{L}}\) množica stanj pomnilnika. Evaluacijo aritmetičnih izrazov podamo z relacijo \(s, e \Downarrow n \subseteq \mathbb{S} \times \mathbb{E} \times \Z\).
\begin{gather*} \begin{bprooftree} \AxiomC{} \UnaryInfC{\(S, \underline{n} \Downarrow n\) } \end{bprooftree} \\ \begin{bprooftree} \AxiomC{\(S, e_1 \Downarrow n_1\)} \AxiomC{\(S, e_2 \Downarrow n_2\)} \BinaryInfC{\(S, e_1 + e_2 \Downarrow n_1 + n_2\)} \end{bprooftree} \qquad \begin{bprooftree} \AxiomC{\(S, e_1 \Downarrow n_1\)} \AxiomC{\(S, e_2 \Downarrow n_2\)} \BinaryInfC{\(S, e_1 * e_2 \Downarrow n_1 \cdot n_2\)} \end{bprooftree} \\ \begin{bprooftree} \AxiomC{\(S, e \Downarrow n\)} \UnaryInfC{\(S, -e \Downarrow -n\) } \end{bprooftree} \quad \begin{bprooftree} \AxiomC{\(s(l) \neq \bot\)} \UnaryInfC{\(s, l \Downarrow s(l)\) } \end{bprooftree} \end{gather*}Za logične izraze imamo relacijo \(s, b \Downarrow r \in \mathbb{B} = \left\{ \mathit{tt}, \mathit{ff} \right\}\)
\begin{gather*} \begin{bprooftree} \AxiomC{} \UnaryInfC{\(S, \texttt{true} \Downarrow \mathit{tt} \)} \end{bprooftree} \quad \begin{bprooftree} \AxiomC{} \UnaryInfC{\(S, \texttt{false} \Downarrow \mathit{ff} \)} \end{bprooftree} \\ \begin{bprooftree} \AxiomC{\(S, e_1 \Downarrow n_1\)} \AxiomC{\(S, e_2 \Downarrow n_2\)} \AxiomC{\(n_1 < n_2\)} \TrinaryInfC{\(S, e_1 < e_2 \Downarrow \mathit{tt}\)} \end{bprooftree} \quad \begin{bprooftree} \AxiomC{\(S, e_1 \Downarrow n_1\)} \AxiomC{\(S, e_2 \Downarrow n_2\)} \AxiomC{\(n_1 \geq n_2\)} \TrinaryInfC{\(S, e_1 < e_2 \Downarrow \mathit{ff}\)} \end{bprooftree} \end{gather*}in podobno za ostale.
\begin{prooftree} \AxiomC{\(S, c_1 \leadsto S', c_1'\)} \UnaryInfC{\(S, (c_1 ; c_2) \leadsto S', (c_1', c_2)\)} \end{prooftree} \begin{prooftree} \AxiomC{\(\)} \UnaryInfC{\(S, (\text{skip} ; c_2) \leadsto S, c_2\)} \end{prooftree} \begin{prooftree} \AxiomC{\(S, b \Downarrow \mathit{tt}\)} \UnaryInfC{\(S,\ \text{if } b \text{ then } c_1 \text{ else } c_2 \leadsto S, c_1\)} \end{prooftree}Podobno za \(\mathit{ff}\) in \(c_2\).
\begin{prooftree} \AxiomC{\(S, e \Downarrow n\)} \UnaryInfC{\(S, l := e \leadsto S[l \mapsto n], \text{ skip}\)} \end{prooftree} \begin{prooftree} \AxiomC{\(S, b \Downarrow \mathit{ff}\)} \UnaryInfC{\(S, \text{ while } b \text{ do } c \leadsto S, \text{ skip}\)} \end{prooftree} \begin{prooftree} \AxiomC{\(S, b \Downarrow \mathit{tt}\)} \UnaryInfC{\(S, \text{ while } b \text{ do } c \leadsto S, (c ; \text{ while } b \text{ do } c)\)} \end{prooftree}Da izključimo možnost neveljavnega branja iz pomnilnika, podajmo relacije za preverjanje veljavnosti. Z \(L\) označimo množice lokacij. Pišemo \(L \vdash e\) ko je \(e\) veljavna za veljavne lokacije \(L\).
\begin{gather*} \begin{bprooftree} \AxiomC{} \UnaryInfC{\(L \vdash \underline{n}\) } \end{bprooftree} \quad \begin{bprooftree} \AxiomC{\(L \vdash e_1\)} \AxiomC{\(L \vdash e_2\)} \BinaryInfC{\(L \vdash e_1 + e_2\)} \end{bprooftree} \quad \text{ podobno za ostale operacije. } \\ \begin{bprooftree} \AxiomC{\(l \in L\)} \UnaryInfC{\(L \vdash l\) } \end{bprooftree} \end{gather*}Podobno za \(L \vdash b\). Moramo še podati pravila oblike \(L \vdash c, L'\).
\begin{gather*} \begin{bprooftree} \AxiomC{} \UnaryInfC{\(L \vdash \text{ skip}, L\) } \end{bprooftree} \quad \begin{bprooftree} \AxiomC{\(L \vdash c_1, L'\)} \AxiomC{\(L' \vdash c_2, L''\)} \BinaryInfC{\(L \vdash (c_1 ; c_2), L''\) } \end{bprooftree} \\ \begin{bprooftree} \AxiomC{\(L \vdash b\)} \AxiomC{\(L \vdash c_1, L_1\)} \AxiomC{\(L \vdash c_2, L_2\)} \TrinaryInfC{\(L \vdash \text{ if } b \text{ then } c_1 \text{ else } c_2, L_1 \cap L_2\)} \end{bprooftree} \text{ lahko bi vzeli tudi samo } L \text{ (lokalni bind)} \\ \begin{bprooftree} \AxiomC{\(L \vdash b\)} \AxiomC{\(L \vdash c, L'\)} \BinaryInfC{\(L \vdash \text{ while } b \text{ do } c, L\)} \end{bprooftree} \quad \begin{bprooftree} \AxiomC{\(L \vdash e\)} \UnaryInfC{\(L \vdash l := e, L \cup \left\{ l \right\}\) } \end{bprooftree} \end{gather*}S tem lahko končno podamo netrivialno drevo izpeljave.
Naj bo \(L \subseteq \left\{ l \mid S(l) \neq \bot \right\}\) in naj velja \(L \vdash c, L'\).
Tedaj velja:
- Bodisi \(c = \text{skip}\)
- Bodisi obstajata \(s', c'\), da velja \(s, c \leadsto s', c'\)
Z indukcijo na \(L \vdash c, L'\) na drevo izpeljave.
Recimo, da je zadnje uporabljeno pravilo:
- \begin{prooftree} \AxiomC{} \UnaryInfC{\(L \vdash \text{skip, } L\) }
\end{prooftree} Potem velja \(c = \) skip.
- \begin{prooftree}
\AxiomC{\(L \vdash c_1, L'\)} \AxiomC{\(L' \vdash c_2, L''\)} \BinaryInfC{\(L \vdash (c_1 ; c_2), L''\)} \end{prooftree} po indukcijski predpostavki za \(L \vdash c_1, L'\) velja
- bodisi \(c_1 = \) skip, zato \(s, (\text{skip} ; c_2) \leadsto s, c_2\).
- bodisi \(s, c_1 \leadsto s', c_1'\), zato \(s, (c_1 ; c_2) \leadsto s', (c_1'; c_2)\).
in tako dalje.
Naj velja \(L \vdash c, L'\) in \(s, c \leadsto s', c' za nek \(L \subseteq \left\{ l \mid s(l) \neq \bot \right\} \).
Tedaj velja tudi \(L'' \vdash c', L'\) za nek \(L \subseteq L''\), da velja \[ L'' \subseteq \left\{ l \mid s'(l) \neq \bot \right\}. \]
Če imamo \(\underbrace{\emptyset}_{L} \vdash (l := 3, m := 4), \underbrace{\left\{ l, m \right\}}_{L'}\) je potem \(L'' = \left\{ l \right\}\).
Lecture 4: Lambda račun
Rekurzivna definicija fakultete
Želimo definirati \(\operatorname{fact} = \lambda n . \text{if } n = 0 \text{ then } 1 \text{ else } n \cdot \operatorname{fact}(n - 1)\). Znamo zakodirati vse razen ciklične definicije \(\operatorname{fact}\). Da se tej definiciji izognemo, to najprej naredimo za vezano spremenljivko. Definiramo \[ \Phi = \lambda f . \, \dots f \dots \] ki vzame funkcijo in jo aplicira v sebi. Poiščemo fiksno točko \(\Phi\).
Recimo, če vzamemo konstanto \(f_0 = \lambda x .\, 42\) dobimo \(f_1 = \Phi f_0\), ki deluje po korakih.
| 0 | 1 | 2 | 3 | 4 | 5 | 6 | |
|---|---|---|---|---|---|---|---|
| \(f_0\) | 42 | 42 | 42 | 42 | 42 | 42 | 42 |
| \(f_1 = \Phi f_1\) | 1 | 42 | 84 | 126 | |||
| \(f_2 = \Phi f_1\) | 1 | 1 | 84 | 252 | |||
| \(f_3 = \Phi f_2\) | 1 | 1 | 2 | 6 |
Ko gremo naprej dobimo funkcijo vedno bolj podobno fakulteti. Za začetno funkcijo najraje uporabimo nekaj nikjer definiranega. Hkrati imamo operatorja
\begin{align*} \Omega &= (\lambda x . xx) (\lambda x . xx) \\ Y' &= \lambda \Phi . (\lambda f .ff)(\lambda f. \Phi(ff)) \\ Y' \Phi_K &\leadsto (\lambda f. ff)(\lambda f. \Phi_k(ff)) \\ &\leadsto (\lambda f . \Phi_K(ff))(\lambda f. \Phi_K(ff)) \\ &\leadsto \Phi_K\left( (\lambda f. \Phi_k(ff))(\lambda f. \Phi_k(ff)) \right) \end{align*}kjer \(Y'\) na specifičnem \(\Phi_K\) deluje tako, da spredaj dodaja \(\Phi_K\).
Potem vzamemo \[ Y = \lambda \Phi . (\lambda f.ff)(\lambda f.\lambda x . (\Phi(f f)) x) \]
(Better check the online notes for more detail etc).
Lecture 5: Lambda račun s preprostimi tipi
i.e. simply-typed \(\lambda\)-calculus (STLC).
Kjer imamo izraze in njihove tipe. Podajmo semantiko. Vrednosti so \[ V ::= \lambda x . M \mid \underline{n} \mid \texttt{true} \mid \texttt{false} \]
\begin{gather*} \begin{bprooftree} \AxiomC{\(M \leadsto M'\)} \UnaryInfC{\(MN \leadsto M'N\) } \end{bprooftree} \quad \begin{bprooftree} \AxiomC{\(N \leadsto N'\)} \UnaryInfC{\(VN \leadsto VN'\) } \end{bprooftree} \\ \begin{bprooftree} \AxiomC{} \UnaryInfC{\(\lambda x. M\) V \leadsto M[V/x] } \end{bprooftree} \quad \begin{bprooftree} \AxiomC{\(M \leadsto M'\)} \UnaryInfC{\(\operatorname{isZero} M \leadsto \operatorname{isZero} M'\) } \end{bprooftree} \\ \begin{bprooftree} \AxiomC{} \UnaryInfC{\(\operatorname{isZero} 0 \leadsto \texttt{true}\) } \end{bprooftree} \quad \begin{bprooftree} \AxiomC{\(n \neq 0\)} \UnaryInfC{\(\operatorname{isZero} \underline{n} \leadsto \texttt{false}\) } \end{bprooftree} \end{gather*}Podobni pravili imamo še za if then else in ostalo. To poda operacijsko semantiko malih korakov.
Dodamo še relacijo tipov \(\Gamma \vdash M : A\). Te dodajo sintaktična pravila
\begin{gather*} \begin{bprooftree} \AxiomC{\((x : A) \in \Gamma\)} \RightLabel{var} \UnaryInfC{\(\Gamma \vdash x : A\) } \end{bprooftree} \quad \begin{bprooftree} \AxiomC{\(\Gamma, x : A \vdash M : B\)} \RightLabel{lam} \UnaryInfC{\(\Gamma \vdash \lambda x . M : A \rightarrow B\) } \end{bprooftree} \quad \begin{bprooftree} \AxiomC{\(\Gamma \vdash M : A \rightarrow B\)} \AxiomC{\(\Gamma \vdash N : A\)} \RightLabel{app} \BinaryInfC{\(\Gamma \vdash MN : B\) } \end{bprooftree} \\ \begin{bprooftree} \AxiomC{} \RightLabel{const} \UnaryInfC{\(\Gamma \vdash \underline{n} : \operatorname{int}\) } \end{bprooftree} \quad \begin{bprooftree} \AxiomC{\(\Gamma \vdash M : \operatorname{int}\)} \RightLabel{isZero} \UnaryInfC{\(\Gamma \vdash \operatorname{isZero} M : \operatorname{bool}\) } \end{bprooftree} \cdots \begin{bprooftree} \AxiomC{\(\Gamma \vdash M : \operatorname{bool}\)} \AxiomC{\(\Gamma \vdash N_1 : A\)} \AxiomC{\(\Gamma \vdash N_2 : A\)} \RightLabel{if} \TrinaryInfC{\(\Gamma \vdash \text{if } M \text{ then } N_1 \text{ else } N_2 : A\)} \end{bprooftree} \end{gather*}Če velja \(\vdash M : A\), tedaj
- Bodisi je \(M\) vrednost,
- Bodisi obstaja \(M'\), da je \(M \leadsto M'\).
Z indukcijo na drevo izpeljave \(\vdash M : A\). Obravnavajmo zadnje uporabljeno pravilo.
- Če je zadnje pravilo var ne pride v poštev, ker je kontekst prazen.
- Za lam velja, ker že imamo vrednost.
Če imamo
\begin{prooftree} \AxiomC{\(\vdash M' : A' \rightarrow A' \)} \AxiomC{\(\vdash N : A'\)} \BinaryInfC{\(\vdash M' N : A\) } \end{prooftree}po indukcijski predpostavki velja napredek za \(\vdash M' : A' \rightarrow A\). Če je \(M'\) vrednost, hitro vidimo, da je oblike \(\lambda x . M''\). Poleg tega ga po indukcijski predpostavki velja napredek za \(\vdash N : A'\). Če je \(N\) vrednost \(V\), je \(M'N = (\lambda x . M'') V\), zato lahko naredimo korak
\begin{prooftree} \AxiomC{} \UnaryInfC{\((\lambda x . M'') V \leadsto M''[V/x]\) } \end{prooftree}Po drugi strani, če obstaja \(N'\), da je \(N \leadsto N'\), pa velja
\begin{prooftree} \AxiomC{\(N \leadsto N'\)} \UnaryInfC{\((\lambda x . M'') N\leadsto (\lambda x . M'') N'\) } \end{prooftree}Če po drugi strani \(M'\) naredi korak \(M' \leadsto M''\), tedaj velja
\begin{prooftree} \AxiomC{\(M' \leadsto M''\)} \UnaryInfC{\(M' N \leadsto M'' N\) } \end{prooftree}- Za const smo končali.
- Za isZero moramo po indukciji za \(M\).
- Za if moramo po indukciji za bool.
Ostalo podobno.
Če velja \(\Gamma, x : A \vdash M : B\) in \(\Gamma \vdash N : A\), tedaj velja \(\Gamma \vdash M[N/x] : B\)
Vaja.
Če velja \(\vdash M : A\) in \(M \leadsto M'\), tedaj velja tudi \(\vdash M' : A\).
Z indukcijo na \(M \leadsto M'\).
Recimo, da imamo
\begin{prooftree} \AxiomC{\(M' \leadsto M''\)} \UnaryInfC{\(M' N\ \leadsto M'' N) } \end{prooftree}Potem iz \(\vdash M' N : A\) sledi \(\vdash M' : A' \rightarrow A\) in \(\vdash N : A'\) za nek \(A'\). Po indukcijski predpostavki velja \(\vdash M'' : A' \rightarrow A\), zato velja
\begin{prooftree} \AxiomC{\(\vdash M'' : A' \rightarrow A\)} \AxiomC{\(\vdash N : A'\)} \BinaryInfC{\(\vdash M'' N : A\)} \end{prooftree}Za
\begin{prooftree} \AxiomC{\(N \leadsto N'\)} \UnaryInfC{\(VN \leadsto VN'\) } \end{prooftree}postopamo podobno.
- \((\lambda x . M') V \leadsto M'[V/x]\) velja \(\vdash \lambda x . M' : A' \rightarrow A\) in \(\vdash V : A'\), zato tudi \(x : A' \vdash M' : A\) in po lemi o substituciji velja \(M'[V/x] : A\).
Če velja \(\vdash M : A\), tedaj:
- bodisi obstaja vrednost \(\vdash V : A\), da je \(M = V\)
- bodisi obstaja \(\vdash M' : A\), da je \(M \leadsto M'\).
Če velja \(\vdash M : A\), tedaj obstaja \(\vdash V : A\), da je \[ M \leadsto^{ * } V \]
To je zato, ker v jeziku ni rekurzije.
Na izpitu 31. 1. 2020.
Ne obstaja tip \(A\), da bi veljalo \[ \vdash \Omega : A. \]
Rekurzijo moramo dotati eksplicitno.
\begin{align*} M, N &::= \cdots \mid \mathtt{rec} f \,x .\, M \\ V &::= \cdots \mid \mathtt{rec} f\, x.\, M \end{align*} \begin{gather*} \begin{bprooftree} \AxiomC{} \UnaryInfC{\((\mathtt{rec} f\, x.\, M)V \leadsto M[ \mathtt{rec} f\,x.\, M/f, V/x ] \) } \end{bprooftree} \quad \begin{bprooftree} \AxiomC{\(\Gamma, f : A \rightarrow B\)} \AxiomC{\(x : A, \Gamma \vdash M : B\)} \BinaryInfC{\(\Gamma \vdash \mathtt{rec} f\, x.\, M : A \rightarrow B\) } \end{bprooftree} \end{gather*}Preverimo lahko, da varnost še velja, normalizacija pa ne.
Lecture 6: Dokazovalniki
Imamo tudi druga pravila za tipiziranje lambde, specifično unit in empty type
\begin{gather*} \begin{bprooftree} \AxiomC{} \UnaryInfC{\(\Gamma \vdash \left< \right> : 1\) } \end{bprooftree} \quad \begin{bprooftree} \AxiomC{\(\Gamma \vdash M : \emptyset\)} \UnaryInfC{\(\Gamma \vdash \text{absurd } M : C\) } \end{bprooftree} \end{gather*}Naravna dedukcija za izjavni račun poda še en primer induktivno podane relacije. \[ P, Q, R ::= P \Rightarrow Q \mid \top \mid P \land Q \mid \bot \mid P \lor Q. \] Uporabljamo zapis \(\Phi \vdash P\) ki za dane predpostavke izpelje \(P\).
\begin{gather*} \begin{bprooftree} \AxiomC{\(P \in \Phi\)} \UnaryInfC{\(Q \vdash P\) } \end{bprooftree} \quad \begin{bprooftree} \AxiomC{\(\Phi, P \vdash Q\)} \UnaryInfC{\(\Phi \vdash P \Rightarrow Q\) } \end{bprooftree} \quad \begin{bprooftree} \AxiomC{\(\Phi \vdash P \Rightarrow Q\)} \AxiomC{\(\Phi \vdash P\)} \BinaryInfC{\(\Phi \vdash Q\)} \end{bprooftree} \\ \begin{bprooftree} \AxiomC{} \UnaryInfC{\(\Phi \vdash \top\) } \end{bprooftree} \quad \begin{bprooftree} \AxiomC{\(\Phi \vdash P\)} \AxiomC{\(\Phi \vdash Q\)} \BinaryInfC{\(\Phi \vdash P \land Q\)} \end{bprooftree} \quad \begin{bprooftree} \AxiomC{\(\Phi \vdash P \land Q\)} \UnaryInfC{\(\Phi \vdash P\) } \end{bprooftree} \\ \begin{bprooftree} \AxiomC{\(\Phi \vdash P \land Q\)} \UnaryInfC{\(\Phi \vdash Q\) } \end{bprooftree} \quad \begin{bprooftree} \AxiomC{\(\Phi \vdash \bot\)} \UnaryInfC{\(\Phi \vdash P\) } \end{bprooftree} \quad \begin{bprooftree} \AxiomC{\(\Phi \vdash P\)} \UnaryInfC{\(\Phi \vdash P \lor Q\) } \end{bprooftree} \\ \begin{bprooftree} \AxiomC{\(\Phi \vdash Q\)} \UnaryInfC{\(\Phi \vdash P \lor Q\) } \end{bprooftree} \quad \begin{bprooftree} \AxiomC{\(\Phi \vdash P \lor Q\)} \AxiomC{\(\Phi, P \vdash R\)} \AxiomC{\(\Phi, Q \vdash R\)} \TrinaryInfC{\(\Phi \vdash R\)} \end{bprooftree} \end{gather*}S tem podamo intuicionistično logiko. Če dodamo LEM, dobimo klasično logiko.
Opazimo, da so pravila analogna pravilom za tipizacijo. \(\Phi \vdash P\) velja natanko tedaj, ko obstaja \(M\), da velja \[ \Gamma \vdash M : A \] za ustrezna \(\Gamma\) in \(A\).
Gre za konkreten primer Curry-Howardovega izomorfizma.
| Teorija tipov | Logika |
|---|---|
| tip | izjava |
| izraz | dokaz |
| \(\rightarrow\) | \(\Rightarrow\) |
| 1 | \(\top\) |
| \(\times\) | \(\land\) |
| \(\emptyset\) | \(\bot\) |
| \(+\) | \(\lor\) |
| družina tipov \(\{A(X)\}_{x \in X}\) | Predikat \(P(x)\) |
| \(\prod(x : X) .\,A(x)\) | \(\forall\) |
| \(\sum(x : X) . \, A(x)\) | \(\exists\) |
NB produktni tip si predstavljamo kot odvisno funkcijo \((x : X) \rightarrow A(x))\). Odvisno vsoto včasih pišemo tudi \[ \sum(x : X) . \, A(x) = \coprod_{x \in X}A(x)= (x : X) \times A(x) \] kjer zadnji zapis res eksplicitno pokaže dejstvo, da imamo odvisne pare.
(Lecture 7): Denotacijska semantika
Zakaj bi sploh imeli denotacijsko semantiko?
Izraza \[ \lambda x.\, x * 2 \text{ in } \lambda x.\, 2 * x \] nista enaka, želeli pa bi, da sta. Enaka sta na način da se pri vsakem vhodu evaluirata v isti izhod.
\noindent To nas motivira, da uvedemo kontekstno ekvivalenco.
Izraza \(M\) in \(N\) sta kontekstno ekvivalentna in pišemo \(M \simeq N \) če za vsak kontekst \(\mathcal{C}\) (izraz z luknjo) veja \[ \mathcal{C}[M] \leadsto^{ * } \mathtt{true} \iff \mathcal{C}[N] \leadsto^{ * } \mathtt{true} \]
\(\mathcal{C}\) formalno definiramo kot \[ \mathcal{C} ::= [~] \mid \underline{n} \mid \mathcal{C}_1 + \mathcal{C}_2 \mid \mathcal{C}_1 * \mathcal{C}_2 \mid \mathtt{true} \mid \mathtt{false} \mid \lambda x.\, \mathcal{C} \mid \cdots \]
Definiramo še \(\mathcal{C}(M)\) kot izraz, ki ga dobimo, če v \(\mathcal{C}\) vse \([~]\) zamenjamo z \(M\).
\[ \mathcal{C} := \lambda x .\, (1 + [~] * x) \]
\(M \simeq N\) velja natanko tedaj, ko za vsak \(\mathcal{C}\) velja \[ \mathcal{C}[M] \leadsto^{ * } \mathtt{false} \iff \mathcal{C}[N] \leadsto^{ * } \mathtt{false} \]
Predpostavimo \(M \simeq N\) in dokažimo \[ \forall \mathcal{C} .\, \mathcal{C}[M] \leadsto^{ * } \mathtt{false} \iff \mathcal{C}[N] \leadsto^{ * } \mathtt{false}. \] Vzemimo \(\mathcal{C}\) in predpostavko \(\mathcal{C}[M] \leadsto^{ * } \mathtt{false}\). Naj bo \[ \mathcal{C}' = \text{if } \mathcal{C} \text{ then } \mathtt{false} \text{ else } \mathtt{true} \] zato velja \[ C'[M] \leadsto^{ * } \text{ if } \mathtt{false} \text{ then } \mathtt{false} \text{ else} \mathtt{true} \leadsto \mathtt{true}. \] Ker je \(M \simeq N\), velja tudi \(\mathcal{C}'[N] \leadsto^{ * } \mathtt{true}\). Zato mora veljati \(\mathcal{C}[N] \leadsto^{ * } \mathtt{ false}\).
Implikacija v drugo smer poteka enako.
\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.
\[ M \simeq N \centernot\iff \left( \forall \mathcal{C} .\, \mathcal{C}[M] \leadsto^{ * } V \iff \mathcal{C}[N] \leadsto^{ * } V \right) \]
Naivna interpretacija
Vsakemu tipu \(A\) bomo priredili množico \(\llbracket A \rrbracket\), ki ji pravimo interpretacija \(A\).
\begin{align*} \llbracket \mathtt{bool}\rrbracket &= \mathbf{B} = \left\{ \mathsf{tt}, \mathsf{ff} \right\} \\ \llbracket \mathtt{int} \rrbracket &= \Z \\ \llbracket A \rightarrow B \rrbracket &= \llbracket B \rrbracket^{\llbracket A \rrbracket} = \llbracket A \rrbracket \rightarrow \llbracket B \rrbracket \end{align*}Izraze \(\vdash M : A\) bomo interpretirali z elementi \(\llbracket \vdash M : A \rrbracket \in \llbracket A \rrbracket\). V splošnem interpretiramo izraze v kontektsu \[ \llbracket \Gamma \vdash M : A\rrbracket : \llbracket \Gamma \rrbracket \rightarrow \llbracket A \rrbracket \] kjer je \[ \llbracket x_1 : A_1, \dots, x_n : A_n \rrbracket := \llbracket A_1 \rrbracket \times \cdots \times \llbracket A_n \rrbracket \]
Za \(\Gamma \vdash M : A\) in \(M \leadsto M'\) velja \[ \llbracket \Gamma \vdash M : A \rrbracket = \llbracket \Gamma \vdash M' : A \rrbracket \]
Z indukcijo na \(M \leadsto M'\). Da pokažemo
\begin{prooftree} \AxiomC{\(M \leadsto M'\)} \UnaryInfC{\(\text{if } M \text{ then } N_1 \text{ else } N_2\) } \noLine \UnaryInfC{\(\leadsto\text{if }M' \text{ then} N_1 \text{ else } N_2\) } \end{prooftree}pogledamo
\begin{align*} \llbracket \text{ if } M \text{ then } N_1 \text{ else } N_2 \rrbracket(\gamma) &= \begin{cases} \llbracket N_1 \rrbracket(\gamma) & \llbracket M \rrbracket(\gamma) = \mathsf{tt} \\ \llbracket N_2 \rrbracket(\gamma) & \text{sicer} \end{cases} \\ &= \begin{cases} \llbracket N_1 \rrbracket(\gamma) & \llbracket M' \rrbracket \rrbracket(\gamma) = \mathsf{tt} \\ \end{cases} \end{align*}najprej po definiciji, potem po indukcijski predpostavki ter spet po definicji. Ostali primeri so podobni, le pri \(\beta\) redukciji moramo uporabiti lemo o substituciji.
Če imamo \(\Gamma, x : A \vdash M : B\) in \(\Gamma \vdash N : A\), tedaj
\begin{align*} \llbracket \Gamma \vdash M[N/x] : B \rrbracket(\gamma) &= \llbracket \Gamma, x : A \vdash M : B \rrbracket (\gamma, \llbracket \Gamma \vdash N : A \rrbracket (\gamma)) \end{align*}Z indukcijo na \(M\).
Če velja \(\llbracket \vdash M : \mathtt{bool} \rrbracket = \mathit{tt}\), tedaj velja \(M \leadsto^{ * } \mathtt{true}\)
Če imamo krepko normalizacijo, obstaja \(V\), da je \(M \leadsto V^{ * }\). Po skladnosti je \(\llbracket V \rrbracket = \llbracket M \rrbracket = \mathit{tt}\), zato je \(V = \mathtt{true}\).
Če je \(\llbracket M \rrbracket = \llbracket N \rrbracket\), tedaj je \(M \simeq N\).
Opazimo, da je \(\llbracket ~ \cdot ~ \rrbracket\) definirana strukturno, iz česar za \(\llbracket M \rrbracket = \llbracket N \rrbracket\) sledi \[ \llbracket \mathcal{C}[M] \rrbracket = \llbracket \mathcal{C}[N] \rrbracket \] za vse \(\mathcal{C}\).
Recimo \[ \llbracket\underbrace{ \lambda x .\, \text{if } M > 0 \text{ then } M \text{ else } 0}_{\mathcal{C}} \rrbracket = a \mapsto \begin{cases} \llbracket M \rrbracket & \llbracket M \rrbracket > 0 \\ 0 & \text{sicer} \end{cases} \] Če velja \(\mathcal{C}[M] \leadsto^{ * } \mathtt{true}\), je po skladnosti \(\llbracket \mathcal{C}[M] \rrbracket = \llbracket \mathtt{true} \rrbracket = \mathit{tt}\), zato je \(\llbracket \mathcal{C}[N] \rrbracket = \mathit{tt}\), zato po zadostnosti sledi \(\mathcal{C}[N] \leadsto^{ * } \mathtt{true}\).
\noindent Recimo, da dodamo še rekurzijo. Tedaj velja po eni strani \[ \llbracket (\mathtt{rec} \, f \, x .\, f \, x + \underline{1}) \underline{0} \rrbracket = \llbracket \mathtt{rec} \rrbracket(\underline{0}) \] po drugi strani pa \[ \llbracket (\mathtt{rec} \, f \, x .\, f \, x + \underline{1}) \underline{0} \rrbracket = \llbracket (\mathtt{rec} \, f \, x .\, f \, x + \underline{1}) \underline{0} + \underline{1} \rrbracket = \llbracket (\mathtt{rec}\, f\, x .\, f\, x + 1)0 \rrbracket + 1 \] kar pomeni da rekurzije ne moremo pravilno izraziti.
Domene
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.
Delna ureditev \((D, \leq_D)\) je domena, če
- ima najmanjši element \(\bot_D\), i.e. \(\forall d \in D .\, \bot \leq d\)
- vsaka veriga \(d_0, d_1, \dots\) ima natančno zgornjo mejo \(\bigvee_i d_i \in D\)
\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.
- \(X_{\bot} = X + \left\{ \bot \right\}\) kjer so vsi elementi \(X\) nad \(\bot\) in med samo neprimerljivi
- Če imamo domeni \((D_1, \leq_1)\) in \((D_2, \leq_2)\), potem bo \[ (x_1, x_2) \leq_{D_1 \times D_2} (y_1, y_2) \iff (x_1 \leq_{D_1} y_1) \land (x_2 \leq_{D_2} y_2). \]
Naj bosta \((D_1, \leq_{D_1})\) in \((D_2, \leq_{D_2})\). Funkcija \(f : D_1 \rightarrow D_2\) je zvezna, če je monotona, i.e. \[ x \leq_{D_1} y \implies fx \leq_{D_2} fy, \] ohranja supremume verig, i.e. če je \(x_0 \leq x_1 \leq \cdots \in D_1\), velja \[ f \left( \bigvee_i x_i \right) = \bigvee_i fx_i \]
Naj bo \((D, \leq)\) domena. Tedaj ima vsaka zvezna funkcija \(f : D \rightarrow D\) najmanjšo fiksno točko.
Definiramo \(x_0 = \bot\) in \(x_{i+1} = f(x_i)\). Po indukciji pokažemo, da je \(x_0 \leq x_1 \leq \cdots\) veriga. Ker je \(D\) domena, obstaja \(\bigvee_i x_i \in D\). Preverimo, da je \(x\) najmanjša fiksna točka za \(f\). \[ f \left( \bigvee_i x_i \right) = \bigvee_i f(x_i) = \bigvee_i x_{i+1} = \bigvee_i x_i \]
Naj bo \(y = f(y)\). Po indukciji pokažemo, da je \(x_i \leq y\) za vsak \(i\):
\begin{align*} x_0 &= \bot \leq y \\ x_{i+1} &= f(x_i) \leq f(y) = y \end{align*}To pomeni, da je tudi \[ \bigvee_i x_i \leq y. \]
\noindent Vsak tip \(\llbracket A \rrbracket\) lahko interpretiramo z domeno \(\llbracket A \rrbracket\) tako da dodamo \(\bot\).
\begin{align*} \llbracket \mathtt{bool} \rrbracket &=\mathbb{B}_{\bot} \\ \llbracket \mathtt{int} \rrbracket &= \Z_{\bot} \\ \llbracket A \rightarrow B \rrbracket &= [\llbracket A \rrbracket \rightarrow \llbracket B \rrbracket] \end{align*}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
\begin{align*} \llbracket x_i \rrbracket(\gamma) &= \gamma_i \\ \llbracket M N \rrbracket(\gamma) &= \llbracket M \rrbracket (\gamma)(\llbracket N \rrbracket (\gamma)) \end{align*}
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.
je zvezna funkcija
Naj bo \(f \leq g\). Tedaj je
\[
\bot \leq \bot \quad
f \bot \leq g \bot \quad
f(f(\bot)) \leq g(f(\bot)) \leq g(g(\bot))
\]
zato je
\[
\mu f = \bigvee_i f^i \bot \leq \bigvee_i g^i \bot = \mu g,
\]
torej je fix monotona.
Pokažimo, da je zvezna. \[ f_0 \leq f_1 \leq \cdots \] Potem je
\begin{align*} \mathtt{fix} \left( \bigvee_i f_i \right) &= \bigvee_j (\bigvee_i f_i)^j \bot \\ &= \bigvee_j \bigvee_i (f_i^j \bot) \left(= \bigvee_k f_k^k \bot \right)\\ &= \bigvee_i \left( \bigvee_j f_i^j \bot \right) \\ &= \bigvee_i \mathtt{fix} \, f_i \end{align*}NB da je \[ \left( \bigvee_i f_i \right)^{j +1} \bot = \left( \bigvee_i f_i \right)^j \left( \left( \bigvee_i f_i \right) \bot \right) = \left( \bigvee_i f_j \right)^j \left( \bigvee_i (f_i \bot) \right) = \bigvee_i \left( \left( \bigvee_i f_i \right)^j (f_i \bot) \right) \]