\(\newenvironment{bprooftree}{\begin{prooftree}}{\end{prooftree}}\)
05 Apr 2026

Teorija programskih jezikov (Pretnar)

Lecture 1: Praksa programskih jezikov

Razlika med tem kako je jezik implementiran in kako je standardiziran.

Sintaksa in semantika

Sintaksa opisuje kako napišemo programe. Semantika opisuje kaj pomenijo.

Konkretna in abstraktna sintaksa

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)
Faze urejevalnika
  1. Razčlenjevalnik (Parser): Prevodba iz konkretne sintakse v abstraktno sintakso (AST)
  2. Obogatitev drevesa: Preverjanje tipov, optimizacija, ipd.
  3. Interpreter/Compiler: Tolmačimo ali prevedemo v drug jezik/strojno kodo
Jezik Imp

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.

Funktor za naravna števila

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
Sintaksa jezika Imp

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
Semantika jezika Imp

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.

\begin{prooftree} \AxiomC{} \UnaryInfC{\(S, \underline{3} \Downarrow 3\)} \AxiomC{\(S(a) = 10 \neq \bot\)} \UnaryInfC{\(S, a \Downarrow 10\)} \AxiomC{} \UnaryInfC{\(S, b \Downarrow 4\)} \BinaryInfC{\(S, a + b \Downarrow 14\)} \BinaryInfC{\(S, \underline{3} * (a + b) \Downarrow 42\)} \end{prooftree}
Napredek

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

  1. bodisi \(c_1 = \) skip, zato \(s, (\text{skip} ; c_2) \leadsto s, c_2\).
  2. bodisi \(s, c_1 \leadsto s', c_1'\), zato \(s, (c_1 ; c_2) \leadsto s', (c_1'; c_2)\).

in tako dalje.

Ohranitev

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).

STLC \begin{align*} M, N &::= x \mid \lambda x . M \mid M N \mid & \underline{n} \mid \operatorname{isZero} M \mid M + N \mid M * N \mid M - N \mid \cdots \\ & \texttt{true} \mid \texttt{false} \mid \text{if } M \text{ then } N_1 \text{ else } N_2 \\ A, B ::= \text{int} \mid \text{bool} \mid A \rightarrow B \end{align*}

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*}
\begin{prooftree} \AxiomC{} \UnaryInfC{\(x : \operatorname{int}\vdash x : \operatorname{int}\) } \AxiomC{} \UnaryInfC{\(x : \operatorname{int} \vdash \underline{3} : \operatorname{int}\) } \BinaryInfC{\(x : \operatorname{int} \vdash x + \underline{3} : \operatorname{int}\) } \UnaryInfC{\(x : \operatorname{int} \vdash \operatorname{isZero}(x + \underline{3}) : \operatorname{bool}\) } \UnaryInfC{\(\vdash \lambda x . \operatorname{isZero}(x + \underline{3}) : \operatorname{int} \rightarrow \operatorname{bool}\) } \end{prooftree}
Napredek

Če velja \(\vdash M : A\), tedaj

  1. Bodisi je \(M\) vrednost,
  2. 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.

(o substituciji)

Če velja \(\Gamma, x : A \vdash M : B\) in \(\Gamma \vdash N : A\), tedaj velja \(\Gamma \vdash M[N/x] : B\)

Vaja.

Ohranitev

Če velja \(\vdash M : A\) in \(M \leadsto M'\), tedaj velja tudi \(\vdash M' : A\).

Z indukcijo na \(M \leadsto M'\).

  1. 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}

  2. Za

    \begin{prooftree} \AxiomC{\(N \leadsto N'\)} \UnaryInfC{\(VN \leadsto VN'\) } \end{prooftree}

    postopamo podobno.

  3. \((\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\).
Izrek o varnosti

Č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'\).
Normalizacija

Č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
\begin{gather*} \begin{bprooftree} \AxiomC{\(\Gamma \vdash M : A\)} \AxiomC{\(\Gamma \vdash N : B\)} \BinaryInfC{\(\Gamma \vdash \left< M, N \right> : A \times B\)} \end{bprooftree} \quad \begin{bprooftree} \AxiomC{\(\Gamma \vdash M : A \times B\)} \UnaryInfC{\(\Gamma \vdash \operatorname{fst} M : A\) } \end{bprooftree} \quad \begin{bprooftree} \AxiomC{\(\Gamma \vdash M : A \times B\)} \UnaryInfC{\(\Gamma \vdash \operatorname{snd} M : B\) } \end{bprooftree} \\ \begin{bprooftree} \AxiomC{\(\Gamma \vdash M : A\)} \UnaryInfC{\(\Gamma \vdash \iota_0 M : A + B\) } \end{bprooftree} \quad \begin{bprooftree} \AxiomC{\(\Gamma \vdash M : B\)} \UnaryInfC{\(\Gamma \vdash \iota_1 M : A + B\) } \end{bprooftree} \\ \begin{bprooftree} \AxiomC{\(\Gamma \vdash M : A + B\)} \AxiomC{\(\Gamma, x : B \vdash N_1 : C\)} \AxiomC{\(\Gamma, y : B \vdash N_2 : C\)} \TrinaryInfC{\(\Gamma \vdash \text{match } M \text{ with } \iota_1 x \rightarrow N_1 \mid \iota_1 x \rightarrow N_1\)} \end{bprooftree} \end{gather*}

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 \]

\begin{align*} \llbracket \Gamma \vdash \mathtt{true} : \mathtt{bool} \rrbracket (\gamma) &= \mathtt{tt} \\ \llbracket \Gamma \vdash \mathtt{false} : \mathtt{bool} \rrbracket (\gamma) &= \mathtt{ff} \\ \llbracket \Gamma \vdash \text{if } M \text{ then } N_1 \text{ else } N_2 A \rrbracket(\gamma) &= \begin{cases} \llbracket N_1(\gamma) \rrbracket &; \llbracket M \rrbracket(\gamma) = \mathtt{tt} \\ \llbracket N_1(\gamma) \rrbracket &; \text{sicer} \end{cases} \\ \llbracket \Gamma \vdash \underline{n} : \mathtt{int} \rrbracket(\gamma) &= n \\ \llbracket \Gamma \vdash M + N : \mathtt{int}(\gamma) \rrbracket &= \llbracket M \rrbracket(\gamma) + \llbracket M \rrbracket(\gamma) \\ \llbracket x_1 : A_1, \dots, x_n A_n \vdash x_i : A_i \rrbracket((\gamma_1, \dots, \gamma_n)) &= \gamma_i \\ \llbracket \Gamma \vdash \lambda x .\, M : A \rightarrow B \rrbracket(\gamma) &= a \in \llbracket A \rrbracket \mapsto \llbracket \Gamma, x : A \vdash M : B \rrbracket(\gamma, a) \\ \llbracket \Gamma \vdash MN : B \rrbracket(\gamma) &= \llbracket \Gamma \vdash M : A \rightarrow B\rrbracket(\gamma)\left(\llbracket \Gamma \vdash N : A\rrbracket(\gamma)\right) \end{align*}
\begin{align*} &\llbracket x : \mathtt{int} \vdash \lambda y .\, 2 * x > y + 5 : \mathtt{int} \rightarrow \mathtt{bool} \rrbracket(a): \Z \rightarrow (\Z \rightarrow \mathbf{B}) \\ = &b \in \Z \mapsto \llbracket x : \mathtt{int}, y : \mathtt{int} \vdash 2 * x > y + 5 : \mathtt{bool} \rrbracket(a, b) \\ =& b \in \Z \mapsto \begin{cases} \mathsf{tt} & \llbracket 2 * x \rrbracket(a, b) > \llbracket y + y \rrbracket(a, b) \\ \mathsf{ff} & \text{sicer} \\ \end{cases} \\ =& b \in \Z \mapsto \begin{cases} \mathsf{tt} & 2a > b + 5 \\ \mathsf{ff} & \text{sicer} \end{cases} \end{align*}
Skladnost

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

Tags: lecture-notes