# Lista 12
###### tags: `jp21`

# Zadanie 1 (TAPL 15.3.2)


ezpz




# Zadanie 2 (TAPL 15.5.2, 15.5.3)


$$
\dfrac{S_1 <: T_1 \quad T_1 <: S_1}{Ref\ S_1 <: Ref\ T_1} \qquad \dfrac{}{}
$$

(1)

Mamy:
$$
\dfrac{T_1 <: S_1}{Ref\ S_1 <: Ref\ T_1} (S-Ref_{(1)})
$$

T = {x:Nat, y:Nat} S ={x:Nat}

a = {x = 5}
b = {x=7, y=8}
store := ref a (Ref S)
odczyt = (!store).y (no i y nie jest zapisany??)


$$
\dfrac{
\dfrac{5 : Nat}{ref \{x = 5\} : Ref \{x\}} \quad
\dfrac{
\dfrac{
\dfrac{
s:Ref\{x\} \vdash s:Ref\{x\} \quad \dfrac{\{x, y\} <: \{x\}}{Ref\{x\} <: Ref\{x, y\}} (S-Ref_{(1)})
}{
s:Ref\{x\} \vdash s : Ref \{y, x\}} (T-Sub)
}{
s:Ref\{x\} \vdash !s : \{y, x\}
}
}{s:Ref \{x=Nat\} \vdash (!s).y : Nat}
}{\emptyset \vdash let\, s = ref \{x = 5\}\, in\, (!s).y : Nat}
$$

---
(2)
~~albo:
a = {x = 5} ( S<=T)
b = {x=7, y=8}
store := ref a
store := b (no i y nie ma miejsca?? )~~

Mamy:
$$
\dfrac{S_1 <: T_1}{Ref\ S_1 <: Ref\ T_1} (S-Ref_{(2)})
$$

let x = ref {a:1, b:2} in x := {a:0}; !x.b

$$t = [\lambda l. \ (\lambda \_. \ (!l).y)(l := \{x : unit\})](ref \{x : unit, y : unit\})$$

$$\dfrac{\dfrac{\dfrac{\dfrac{\dfrac{\dfrac{l : Ref\{x : Unit, y : Unit\} \ | \ \emptyset \vdash \ \ l : Ref\{x : Unit, y : Unit\}}{l : Ref\{x : Unit, y : Unit\} \ | \ \emptyset \vdash \ \ !l : \{x : Unit, y : Unit\}}}{l : Ref\{x : Unit, y : Unit\} \ | \ \emptyset \vdash \ \ (!l).y : Unit}}{l : Ref\{x : Unit, y : Unit\} \ | \ \emptyset \vdash \ \ \lambda \_. \ (!l).y : Unit \rightarrow Unit}
\quad\quad \dfrac{\color{blue}{\dfrac{\dfrac{}{l : Ref\{x : Unit, y : Unit\} \ | \ \emptyset \vdash \ l : Ref\{x : Unit, y : Unit \}} \quad\quad \dfrac{\{x : Unit, y : Unit\} <: \{x : Unit \}}{Ref\{x : Unit, y : Unit\} <: Ref\{x : Unit \}}}{l : Ref\{x : Unit, y : Unit\} \ | \ \emptyset \vdash \ l : Ref\{x : Unit \}}} \quad\quad \dfrac{}{l : Ref\{x : Unit, y : Unit\} \ | \ \emptyset \vdash \ \{x : unit\} : \{x : Unit\}}}{l : Ref\{x : Unit, y : Unit\} \ | \ \emptyset \vdash \ l := \{x : unit\} : Unit}}{l : Ref\{x : Unit, y : Unit\} \ | \ \emptyset \vdash \ (\lambda \_. \ (!l).y)(l := \{x : unit\}) : Unit}}{\emptyset \ | \ \emptyset \vdash \lambda l. \ (\lambda \_. \ (!l).y)(l := \{x : unit\}) : Ref\{x : Unit, y : Unit\} \rightarrow Unit} \quad\quad \dfrac{}{\emptyset \ | \ \emptyset \vdash ref \{x : unit, y : unit\} : Ref\{x : Unit, y : Unit\}}}{\emptyset \ | \ \emptyset \vdash [\lambda l. \ (\lambda \_. \ (!l).y)(l := \{x : unit\})](ref \{x : unit, y : unit\}) : Unit}$$


# Zadanie 3 (TAPL 15.6.3)


# Zadanie 4 (TAPL 20.2.1)


# Zadanie 5 (TAPL 20.2.2)



**Lemat o postaciach kanonicznych**
- ...
- Jeśli $v$ jest zamkniętą wartością o typie $U = \mu X. T$ to $v$ ma postać $fold \ [U] \ v_0$ gdzie $v_0$ również jest wartością.

**Lemat o inwersji**
- ...
- Jeśli $\Gamma \vdash fold \ [S] \ t_1 : T$ to $S = T$ oraz istnieje taki $T_1$, że $T = \mu X. T_1$ oraz $\Gamma \vdash t_1 : [X := T]T_1$.
- Jeśli $\Gamma \vdash unfold \ [S] \ t_1 : T$ istnieje taki $S_1$, że $S = \mu X. S_1$ oraz $\Gamma \vdash t_1 : S$ oraz $T = [X := S]S_1$.

Dowody obu lematów wynikają wprost z definicji.

---

**Progress:** Jeśli $\emptyset \vdash t : T$ to $t$ jest wartością lub istnieje $t'$ taki, że $t \rightarrow t'$.

Dowód: Indukcja względem relacji $\emptyset \vdash t : T$. Rozważymy tylko dwa nowe przypadki:

- $\dfrac{T = \mu X.T_1 \quad\quad \emptyset \vdash t_1 : [X := T]T_1}{\emptyset \vdash fold \ [T] \ t_1 : T}$ czyli $t = fold \ [U] \ t_1$

Mamy dwa podprzypadki zależnie od tego, czy $t_1$ jest wartością. Jeśli tak, to $t = fold \ [T] \ t_1$ także jest wartością.

Załóżmy więc, że $t_1$ nie jest wartością. Mamy $\emptyset \vdash t_1 : [X := T]T_1$, zatem z ZI istnieje taki $t_1'$, że $t_1 \rightarrow t_1'$. Zatem:
$$\dfrac{t_1 \rightarrow t_1'}{fold \ [T] \ t_1 \rightarrow fold \ [T] \ t_1'}$$

- $\dfrac{T = \mu X.T_1 \quad\quad \Gamma \vdash t_1 : T}{\Gamma \vdash unfold \ [T] \ t_1 : [X := T]T_1}$ czyli $t = unfold \ [U] \ t_1$

Mamy dwa podprzypadki zależnie od tego, czy $t_1$ jest wartością. Jeśli nie, to skoro $\Gamma \vdash t_1 : T$ to z ZI istnieje $t_1'$, że $t_1 \rightarrow t_1'$, zatem:
$$\dfrac{t_1 \rightarrow t_1'}{unfold \ [T] \ t_1 \rightarrow unfold \ [T] \ t_1'}$$

Załóżmy więc, że $t_1$ jest wartością. Skoro ma ona typ $T = \mu X. T_1$, to z lematu o postaciach kanonicznych $t_1 = fold \ [T] \ v$. Zatem $t = unfold \ [T] \ (fold \ [T] \ v))$, więc:
$$\dfrac{}{unfold \ [T] \ (fold \ [T] \ v) \rightarrow v}$$

---

**Preservation:** Jeśli $t \rightarrow t'$ oraz $\Gamma \vdash t : T$ to $\Gamma \vdash t' : T$.

Dowód: Indukcja względem relacji $t \rightarrow t'$. Rozważymy tylko 3 nowe przypadki.

- $\dfrac{}{unfold \ [S] \ (fold \ [U] \ v_1) \rightarrow v_1}$ czyli $t = unfold \ [S] \ (fold \ [U] \ v_1)$ oraz $t' = v_1$

Stosujemy inwersję dwa razy: najpierw skoro $\Gamma \vdash unfold \ [S] \ (fold \ [U] \ v_1) : T$ to $S = \mu X. S_1$ oraz $T = [X := S]S_1$ oraz $\Gamma \vdash fold \ [U] \ v_1 : S$. Następnie z tego ostatniego faktu dostajemy, że $U = S$ oraz że $\Gamma \vdash v_1 : [X := S]S_1$, czyli $\Gamma \vdash v_1 : T$.

- $\dfrac{t_1 \rightarrow t_1'}{fold \ [S] \ t_1 \rightarrow fold \ [S] \ t_1'}$ czyli $t = fold \ [S] \ t_1$ oraz $t' = fold \ [S] \ t_1'$

Z inwersji skoro $\Gamma \vdash fold \ [S] \ t_1 : T$ to $S = T = \mu X. T_1$ oraz $\Gamma \vdash t_1 : [X := T]T_1$. Zatem z ZI dostajemy $\Gamma \vdash t_1' : [X := T]T_1$, co z reguły typowania dla fold od razu daje:
$$\dfrac{T = \mu X.T_1 \quad\quad \Gamma \vdash t_1' : [X := T]T_1}{\Gamma \vdash fold \ [T] \ t_1' : T}$$

- $\dfrac{t_1 \rightarrow t_1'}{unfold \ [S] \ t_1 \rightarrow unfold \ [S] \ t_1'}$ czyli $t = unfold \ [S] \ t_1$ oraz $t' = unfold \ [S] \ t_1'$

Z inwersji skoro $\Gamma \vdash unfold \ [S] \ t_1 : T$ to $S = \mu X. S_1$ oraz $T = [X := S]S_1$ oraz $\Gamma \vdash t_1 : S$. Zatem z ZI dostajemy $\Gamma \vdash t_1' : S$, co z reguły typowania dla unfold od razu daje:
$$\dfrac{S = \mu X.S_1 \quad\quad \Gamma \vdash t_1' : S}{\Gamma \vdash unfold \ [S] \ t_1' : [X := S]S_1}$$