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 &::= \text{true} \mid \text{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, \text{true} \Downarrow \mathit{tt} \)} \end{bprooftree} \quad \begin{bprooftree} \AxiomC{} \UnaryInfC{\(S, \text{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\}\).