###### tags: `jp21`

# Lista 8

### ZADANIE 1

ewalucja:

$$(\lambda\_:S.t) v \rightarrow t$$

v = ... | $(\lambda\_:S.t)$

typowanie:

$$\dfrac{\Gamma \vdash t: T}{\Gamma \vdash (\lambda \_:S.t) : S \rightarrow T}$$

- $t \rightarrow t' \iff e(t) \rightarrow e(t')$

$t = (\lambda \_ : S . t_1) v$
$t' = t_1$

$e(t) = (\lambda x : S . e(t_1)) e(v), x \notin FV(t)$
$e(t) \rightarrow e(t_1)[x:=e(v)] = e(t_1) = e(t')$

- $\Gamma \vdash t:T \iff \Gamma \vdash e(t) : T$

po wyprowadzeniu typu
$$\dfrac{\Gamma \vdash t: T}{\Gamma \vdash (\lambda \_:S.t) : S \rightarrow T}$$

$\Gamma \vdash (\lambda \_:S.t) : S \rightarrow T$

z przesłanki $t:T$, z ZI $\Gamma \vdash e(t) : T$

$e(\lambda \_:S.t) = \lambda x:S.e(t), x \notin FV(e(t))$

$\dfrac{\Gamma, x:S \vdash e(t) : T}{\Gamma \vdash \lambda x:S.e(t) : S \rightarrow T}$

### ZADANIE 3

Z wykładu 1.12.2021:
---
bezpieczeństwo systemu typów

$$
\Gamma \vdash t : T, t \rightarrow^{*} t' \enspace\Rightarrow \neg wrong(t')
$$

#### PROGRESS

Jeśli $\vdash t : T$ to t jest wartością, lub $\exists_{t'} t \rightarrow t'$

(indukcja po wyprowadzeniu typu):

- $\dfrac{\Gamma \vdash t_1: T1}{\Gamma \vdash inl~ t_1 : T1 + T2}$
Rozważamy przypadki:
1) $t_1$ jest wartością, wtedy inl $t_1$ też jest wartością
2) $t_1$ nie jest wartością, z ZI $t_1 \rightarrow t_1'$, wtedy
$inl ~ t_1 \rightarrow inl ~ t_1'$ (z E-INL)
- taki jak wyżej dla inr
- $\dfrac{\Gamma \vdash t_0 : T_1+ T_2 ~~\; \Gamma, x_1: T_1 \vdash t_1: T ~~\; \Gamma, x_2: T_2 \vdash t_2: T }{\Gamma \vdash case~ t_0 ~ t_1 ~t_2 : T}$

1) $t_0$ jest wartością. Z lem. o post. kan. $t_0 = inl~ v$ lub $t_0 = inr~ v$ (E-CASE[INL|INR])
Wtedy $case~t_0 ~t_1 ~t_2 \rightarrow t_i[x \mapsto v]$
2) $t_0$ nie jest wartością, wtedy z ZI $t_0 \rightarrow t_0'$.
Wtedy z (E-CASE) $case ~ t_0 ~t_1 ~t_2 \rightarrow case~ t_0' ~t_1~t_2$

Dlaczego nic się nie psuje w $\lambda$-rachunku:
- bo dokładamy nowe przypadki do indukcji
- pozostale przypadki dowodu nigdy nie patrzyły na tyle dokładnie na typy, żeby się zorientować, że zjadły sumę

#### PRESERVATION
Jeśli $\vdash t :T \wedge t \rightarrow t'$ to $\vdash t' : T$

Indukcja po wyporowadzeniu typu:

- $\dfrac{\Gamma \vdash t_1: T1}{\Gamma \vdash inl~ t_1 : T1 + T2}$

(Przypuśćmy, że $t_1$ się oblicza) Z ZI: $t_1 \rightarrow t_1'$ i $t_1' : T_1$

(tu naszym $t$ z twierdzenia jest $inl~t_1$, $T = T_1 + T_2$)
Wiemy, że $inl~ t_1 \rightarrow inl~t_1'$ (z E-INL oraz z ZI, w dodatku to jedyna reguła ewaluacji inl t)
Cel: $inl~t_1' : T_1+ T_2$
wiemy, że $t_1' : T_1$ (ZI)
więc cel osiągnięty z T-INL

- taki jak wyżej dla inr

- $\dfrac{\Gamma \vdash t_0 : T_1+ T_2 ~~\; \Gamma, x_1: T_1 \vdash t_1: T ~~\; \Gamma, x_2: T_2 \vdash t_2: T }{\Gamma \vdash case~ t_0 ~ t_1 ~t_2 : T}$

(Relacja ewaluacji mówi, że patrzymym tylko na strzałeczki z $t_0$ w ZI)
1) Przypuśćmy, że $t_0$ nie jest wartością. Wtedy: $t_0 \rightarrow t_0'$ i $t_0' : T_1+T_2$
Wiemy z reguły ewaluacji, że $case~ t_0~ t_1 ~ t_2 \rightarrow case~t_0'~t_1~t_2$.
Cel: $case~ t_0' ~ t_1~ t_2 : T$

Z:  (dla $t_0'$)
wiemy, że $case~ t_0' ~ t_1~ t_2 : T$
2) Jeśli $t_0$ jest wartością, to z lm. o post. kan: $t_0 = inl ~v$ lub $t_0 = inr ~v$. Rozpatrzymy tylko inl v.

$case ~ inl ~ v ~t_1~ t_2 \rightarrow t_1[x \mapsto v] : T$ (bo z przesłanek z ostatniego szarego wiemy, że $t_1 : T$, a mamy lemat przy zachowaniu typu przy podstawieniu, który trzeba zmodyfikować)

(Więcej przypadków nie jest potrzebne, bo jak wyżej)

Modyfikacja lematu o zachowaniu typu przy podstawieniu:

Indukcja wzgl. wyprowadzenia typu $\Gamma \vdash t : T$, przypadek:
$\Gamma, x:S \vdash t : T_1 + T_2$, $\emptyset\vdash v : S$ i chcemy $\Gamma \vdash t[x \mapsto v] : T_1 + T_2$

### ZADANIE 5

1. $T \times Unit \cong T$
$forth = \lambda \{x, unit\}. x$
$back = \lambda x. \{x, unit\}$

2. $(S \times T) \rightarrow U \cong S \rightarrow (T \rightarrow U)$

$forth = \lambda f. (\lambda s. (\lambda t. f \{ s, t\}))$
$back = \lambda f. (\lambda \{s, t\}. (f s) t)$

3. $(Unit + Unit) \rightarrow T \cong T \times T$

$forth = \lambda f. \{ f (inl \ unit), f (inr \ unit) \}$
$back = \lambda \{t_1, t_2\}. (\lambda t_0 . case \ t_0 \ \ inl \ x_1 \Rightarrow \ t_1 | inr \ x_2 \Rightarrow \ t_2 )$

---------

# Lista 9

**13.12.2021 r.**
## Zadanie 2

Cycle:
$(l_1 \rightarrow \lambda x: Nat. (!l_2) x, \\
l_2 \rightarrow \lambda x: Nat. (!l_1) x)$

Term:
$(\lambda l_1. [\lambda l_2. [l_1 := (\lambda x: Nat. (!l_2) x)]
(ref~ \lambda x: Nat. (!l_1) x)])(ref~ \lambda x: Nat. x)$

## Zadanie 1

let y = ref 2 in 3 + !l_x ---> 3 + !l_x