# JP 9

[JP 8](https://hackmd.io/06zXspmXQW-BCzT5D2Kctw)


## Zadanie 1

Niech $\text{refs}(t)$ = wszystkie wskaźniki w pamięci używane w $t$.

Wskaźnik $l$ jest osiągalne w jednym kroku z $l'$ w pamięci $\mu'$ jeśli $l' \in \text{refs}(\mu(l))$.
Wskaźnik $l$ jest osiągalne w wielu krokach z $l'$ jeśli istnieje ciąg lokalizacji zaczynający się na $l$ i kończący się na $l'$, taki, że każdy kolejny element jest osiągalny w jednym kroku z poprzedniego.

$$
\frac{\mu' = \mu \text{ obciete do osiagalnych wskaznikow z $t$}}{t|\mu \rightarrow^{GC} t|\mu'}
$$

Tę regułę wykonujemy na skrajnie zewnętrznym termie (jeśli potrafimy) albo musimy zastosować trick z dzieleniem pamięci przy schodzeniu w podterm:
$\mu_1, v_1 \ t_2 \rightarrow \mu_1 \cap refs(t_2), t_2 \rightarrow \mu_1 \cup \mu_2, v_1 \, v_2$.

Twierdzenie do pokazania:

$$
\forall_{t, t_1, \mu} \,
\exists_{\mu_1, \mu_2} \,
t \, | \, \mu \rightarrow^{*} t_1 \, | \, \mu_1 \iff
t \, | \, \mu \rightarrow^{*}_{GC} t_1 \, | \, \mu_2
\land (\mu_2 \subseteq \mu_1)
$$

## Zadanie 2


Mamy taką regułę typowania:


$\texttt{let } r_1 = \texttt{ref } (\lambda x : \texttt{Nat}. 0) \texttt{ in}$
$\texttt{let } r_2 = \texttt{ref } (\lambda x : \texttt{Nat}. (!r_1) \, 0) \texttt{ in}$
$(r_1 := (\lambda x : \texttt{Nat}. (!r_2) \, 0));$
$r_2$

let r_1 = ref (fun x : Nat -> 0) in
let r_2 = ref (fun x : Nat -> (!r_1) 0) in
r_1 := (fun x : Nat -> (!r_2) 0);
r_2

----------------------------------------------------------


## Zadanie 3


### Lemat o podstawieniu

W trywialny sposób można zauważyć, że nic się nie zmieni.

### Lemat o osłabianiu

$\Gamma \, | \, \Sigma \vdash t : T$, to dla $\Sigma \subseteq \Sigma'$ mamy $\Gamma \, | \, \Sigma' \vdash t : T$.

### Dowód

Indukcja po strukturze wyprowadzenia typu.

* (T-LOC) -- trywialne (bo nasz term jest wartością)
$$
\frac{\Sigma(l) = T_1}{\Gamma \, | \, \Sigma \vdash l : \texttt{Ref } T_1}
$$

* (T-REF)
$$
\frac{\Gamma \, | \, \Sigma \vdash t_1 : T_1}
{\Gamma \, | \, \Sigma \vdash \texttt{ref } t_1 : \texttt{Ref } T_1}
$$
* Jeśli $t_1 = v_1$, to zrobimy krok z (E-REFV). Uzyskamy z tego pewne miejsce w pamięci $l$ z $\mu' = \mu \cup \{ l, v_1 \}$. Weźmy $\Sigma' = \Sigma \cup \{ l : T_1 \}$. Oczywiście $\Gamma \, | \, \Sigma' \vdash \mu'$, bo $v_1$ ma typ $T_1$. $\Gamma \, | \, \Sigma' \vdash l : \texttt{Ref } T_1$ mamy z (T-LOC), bo przesłanka $\Sigma'(l) = T_1$ jest spełniona.
* Wpp. $t_1 \rightarrow t_1'$ i z założenia indukcyjnego dla $t_1$ wiemy, że $t_1'$ ma typ $T_1$.

* (T-DEREF)
$$
\frac{\Gamma \, | \, \Sigma \vdash t_1 : \texttt{Ref } T_{11}}
{\Gamma \, | \, \Sigma \vdash \, !t_1 : T_{11}}
$$
* Jeśli $t_1 = l_1$, to korzystamy z reguły (E-DEREFLOC). Zwrócimy $\mu(l_1) = v_1$. Korzystamy z $\Gamma \, | \, \Sigma \vdash \mu$, więc wiemy że $\Sigma(l_1) = T_{11}$, czyli $v_1$ ma typ $T_{11}$.
* Wpp. $t_1 \rightarrow t_1'$ i z założenia indukcyjnego dla $t_1$, wiemy że $t_1'$ ma typ $T_1$.

* (T-ASSIGN)
$$
\frac{\Gamma \, | \, \Sigma \vdash t_1 : \texttt{Ref } T_{11} \hspace{10pt} \Gamma \, | \, \Sigma \vdash t_2 : T_{11}}
{\Gamma \, | \, \Sigma\ \vdash t_1 := t_2 : \texttt{Unit}}
$$
* Jeśli $t_1 = l_1, t_2 = v_2$, to korzystamy z reguły (E-ASSIGN). W oczywisty sposób zwracamy $\texttt{unit}$, czyli zwracany typ to $\texttt{Unit}$. Zauważmy, że w $\mu'$ pod $l$ mamy nadal ten sam typ, czyli nadal zachodzi $\Gamma \, | \, \Sigma \vdash \mu'$.
* Wpp. jeśli $t_1 = l_1$, to korzystamy z reguły (E-ASSIGN2). Wtedy $t_2 \rightarrow t_2'$, a z założenia indukcyjnego dla $t_2'$ ma ono ten sam typ co $t_2$.
* Wpp. korzystamy z reguły (E-ASSIGN1). Wtedy $t_1 \rightarrow t_1'$, a z założenia indukcyjnego dla $t_1'$ ma ono ten sam typ co $t_1$.

## Zadanie 4

Indukcja po strukturze wyprowadzenia typu.

* (T-LOC) -- trywialne (bo nasz term jest wartością)
$$
\frac{\Sigma(l) = T_1}{\Gamma \, | \, \Sigma \vdash l : \texttt{Ref } T_1}
$$
* (T-REF)
$$
\frac{\Gamma \, | \, \Sigma \vdash t_1 : T_1}
{\Gamma \, | \, \Sigma \vdash \texttt{ref } t_1 : \texttt{Ref } T_1}
$$
* Jeśli $t_1 = v_1$, to korzystamy z reguły (E-REFV)
* Wpp. korzystamy z reguły (E-REF) i założenia indukcyjnego dla $t_1$

* (T-DEREF)
$$
\frac{\Gamma \, | \, \Sigma \vdash t_1 : \texttt{Ref } T_{11}}
{\Gamma \, | \, \Sigma \vdash \, !t_1 : T_{11}}
$$
* Jeśli $t_1 = l$, to korzystamy z reguły (E-DEREFLOC)
* Wpp. korzystamy z reguły (E-DEREF) i założenia indukcyjnego dla $t_1$

* (T-ASSIGN)
$$
\frac{\Gamma \, | \, \Sigma \vdash t_1 : \texttt{Ref } T_{11} \hspace{10pt} \Gamma \, | \, \Sigma \vdash t_2 : T_{11}}
{\Gamma \, | \, \Sigma\ \vdash t_1 := t_2 : \texttt{Unit}}
$$
* Jeśli $t_1 = l_1, t_2 = v_2$, to korzystamy z reguły (E-ASSIGN)
* Wpp. jeśli $t_1 = l_1$, to korzystamy z założenia indukcyjnego dla $t_2$ i reguły (E-ASSIGN2)
* Wpp. korzystały z założenia indukcyjnego dla $t_1$ i reguły (E-ASSIGN1)

## Zadanie 5

### CBV

Z podstawieniem:

$$
\frac{}{v \Downarrow v}
$$

$$
\frac{t_1 \Downarrow \lambda x. t_1' \hspace{30pt} t_2 \Downarrow v_2 \hspace{30pt} [x \mapsto v_2]t_1' \Downarrow v_3}
{t_1 t_2 \Downarrow v_3}
$$

Bez podstawienia (środowisko):
$$
\frac{}{E \vdash v \, | \, \mu \Downarrow E, v, \mu} \hspace{30pt} $$

$$
\frac{x \in \text{Dom}(E) \hspace{30pt} E(x) = E', v}
{E \vdash x \, | \, \mu \Downarrow E', v, \mu}
$$

$$
\frac{E \vdash t_1 \, | \, \mu \Downarrow E_1, \lambda x.t_1', \mu_1 \hspace{10pt}
E \vdash t_2 \, | \, \mu_1 \Downarrow E_2, v_2, \mu_2 \hspace{10pt}
[E_1;(x \mapsto E_2, v_2)] \vdash t_1' \, | \, \mu_2 \Downarrow E', v_3, \mu_3}
{E \vdash t_1 t_2 \, | \, \mu \Downarrow E', v_3, \mu_3}
$$

$$
\frac{E \vdash t_1, \mu \Downarrow E_1, l_1, \mu_1
\hspace{20pt} \mu_1(l_1) = E', v_1}
{E \vdash \, !t_1 \, | \, \mu \Downarrow E', v_1, \mu_1}
$$

$$
\frac{E \vdash t_1 \, | \, \mu \Downarrow E_1, v_1, \mu_1
\hspace{20pt}
l \notin Dom(\mu_1)
\hspace{20pt}
\mu_2 = [\mu_1; (l \mapsto E_1, v_1)]
}
{E \vdash \texttt{ref } t_1 \, | \, \mu \Downarrow E, l, \mu_2}
$$

$$
\frac{E \vdash t_1 \, | \, \mu \Downarrow E_1, l_1, \mu_1
\hspace{20pt}
E \vdash t_2 \, | \, \mu_1 \Downarrow E_2, v_2, \mu_2
\hspace{20pt}
\mu_3 = [\mu_2; (l_1 \mapsto E_2, v_2)]
}
{E \vdash t_1 := t_2 \, | \, \mu \Downarrow E, \texttt{unit}, \mu_3}
$$

Przykład, dla którego w powyższych dwóch regułach zwracamy $E$, a nie $E_1$ ani $E_2$
$$
\texttt{ref } (\lambda x. x) \, 0
$$