tags: `jp21`


$$
\dfrac{}{\Gamma \vdash unit : Unit}
$$

W logice

$$
\dfrac{}{\top}
$$

Po co `Unit` w programowaniu?

1. Po co w STLC (w czystych językach programowania)?
No raczej nic. Daje nam to, że wiemy że się skończyła.

$$
\dfrac{\bot}{\phi}
$$

Obserwacja: $g$ na $y$ się zatrzymuje, wtw. gdy $\alpha~g~y$ zwraca unit.
$$
\alpha := (\lambda f. \lambda x. (f~x;~unit))
$$

# zadanie 2

$$\dfrac{\Gamma \vdash \phi_1 \wedge \phi_2 }{\Gamma \vdash \phi_1}~E_1$$

$$\dfrac{\Gamma \vdash \phi_1 \wedge \phi_2 }{\Gamma \vdash \phi_2}~E_2$$

$$\dfrac{\Gamma \vdash \phi_1 \qquad \Gamma \vdash \phi_2}{\Gamma \vdash \phi_1 \wedge \phi_2 }~I$$

$$\dfrac{\Gamma \vdash \phi_1 \wedge \phi_2 \qquad \Gamma, \phi_1, \phi_2 \vdash \psi}{\Gamma \vdash \psi}~E_{II}$$

tutaj:
$$\dfrac{\Gamma, \phi_1, \phi_2 \vdash \psi \qquad \dfrac{\Gamma \vdash \phi_1 \wedge \phi_2}{\Gamma \vdash \phi_1} \qquad \dfrac{\Gamma \vdash \phi_1 \wedge \phi_2}{\Gamma \vdash \phi_24}}{\Gamma \vdash \psi}$$

---

$$\dfrac{\Gamma \vdash p : (\phi_1 \wedge \phi_2) }{\Gamma \vdash p.1 : \phi_1}~E_1$$

$$\dfrac{\Gamma \vdash p : (\phi_1 \wedge \phi_2) }{\Gamma \vdash p.2 : \phi_2}~E_2$$

$$\dfrac{\Gamma \vdash x : \phi_1 \qquad \Gamma \vdash y: \phi_2}{\Gamma \vdash \{x, y\} : \phi_1 \wedge \phi_2 }~I$$

$$\dfrac{\Gamma \vdash p : \phi_1 \wedge \phi_2 \qquad \Gamma, x : \phi_1, y :\phi_2 \vdash t : \psi}{\Gamma \vdash let~\{x, y\} = p~in~t : \psi}~E_{II}$$

---

$$
let~x~=~t_1~in~t_2 \\
(\lambda~x.~t_2)~t_1
$$

$$
let~\{x,y\}~=~p~in~t_2 \\
(\lambda~x.~\lambda y.~t_2)~p.1~p.2
$$

---

# Zadanie 3


### Postęp

$$
v := ... ~|~ \{v, v\}
$$

Założenie: $\Gamma \vdash t : T$
Teza: $t$ jest wartością lub $t \rightarrow t'$
Dowód:
Indukcja względem drzewa wyprowadzenia typu $t$ ($\Gamma \vdash t : T$):

- $\dfrac{}{\Gamma \vdash unit : Unit}$, $unit$ jest wartością
- reguła dla lambdy
- $\dfrac{\Gamma \vdash t_1 : T_1 \rightarrow T_2 \quad \Gamma \vdash t_2 : T_1}{\Gamma \vdash t_1 t_2 : T_2}$
- $\dfrac{\Gamma \vdash t_1 : T_1 \quad \Gamma \vdash t_2 : T_2}{\Gamma \vdash \{t_1, t_2\} : T_1 \times T_2}$
1. Jeśli $t_1$ jest wartością i $t_2$ wartością, to $\{t_1, t_2\}$ jest wartością czyli koniec.
2. Jeśli $t_1$ jest wartością (i $t_2$ nie jest), to:
Z ZI dla $t_2$ mamy, że $t_2 \rightarrow t_2'$, więc
$$
\dfrac{t_2 \rightarrow t_2'}{\{t_1, t_2\} \rightarrow \{t_1, t_2'\}} (E-Pair_2)
$$

3. Jeśli $t_1$ nie jest wartością, to:
Z ZI dla $t_1$ mamy, że $t_1 \rightarrow t_1'$, więc
$$
\dfrac{t_1 \rightarrow t_1'}{\{t_1, t_2\} \rightarrow \{t_1', t_2\}} (E-Pair_1)
$$

- $\dfrac{\Gamma \vdash p : T_1 \times T_2}{\Gamma \vdash p.i : T_i}$
Zauważmy, że $p.i$ nigdy nie jest wartością. Rozważamy, czy $p$ jest:
- wartością, to z lematu o postaciach kanonicznych, jest postaci $\{v_1, v_2\}$, wtedy:
$$
\dfrac{}{\{v_1, v_2\}.i \rightarrow v_i} (E-PairBeta_i)
$$
- nie jest wartością, z ZI dla $p$, skoro nie jest wartością to $p \rightarrow p'$, więc:
$$
\dfrac{p \rightarrow p'}{p.i \rightarrow p'.i} (E-Proj_i)
$$

$\blacksquare{}$

#### Lemat o postaciach kanonicznych


3. Jeśli $p$ jest wartością typu $T_1 \wedge T_2$, to $p = \{v_1, v_2\}$.
Indukcja...

### Zachowanie typu

Założenie: $\Gamma \vdash t : T$ i $t \rightarrow t'$
Teza: $\Gamma \vdash t' : T$
Dowód:
Indukcja względem drzewa wyprowadzenia $t \rightarrow t'$:
- $\dfrac{}{\{v_1, v_2\}.1 \rightarrow v_1} (E-PairBeta_1)$
Dopasowujemy tą regułę, mamy $t = \{v_1, v_2\}.1$, $t' = v_1$.

Wiemy, że $\Gamma \vdash \{v_1, v_2\}.1 : T$, chcemy $\Gamma \vdash v_1 : T$.
Stosujemy lemat o inwersji dla $\Gamma \vdash \{v_1, v_2\}.1 : T$ (X1), otrzymujemy $\Gamma \vdash \{v_1, v_2\} : T \wedge T_?$, ponownie stosując inwersję(Y1), otrzymujemy $\Gamma \vdash v_1 : T$. Koniec.
- $\dfrac{t \rightarrow t'}{t.1 \rightarrow t'.1} (E-Proj_1)$
ZI = $\Gamma \vdash t : T \wedge T_? \Rightarrow (t \rightarrow t') \Rightarrow \Gamma \vdash t' : T \wedge T_?$

Wiemy, że $\Gamma \vdash t.1 : T$, chcemy $\Gamma \vdash t'.1 : T$.
Z inwersji dla $\Gamma \vdash t.1 : T$, mamy $\Gamma \vdash t : T \wedge T_?$.
Z założenia indukcyjnego, mamy $\Gamma \vdash t' : T \wedge T_?$.
$$
\dfrac{\Gamma \vdash t' : T \wedge T_?}{\Gamma \vdash t'.1 : T}
$$
Koniec

- $\dfrac{t_1 \rightarrow t_1'}{\{t_1, t_2\} \rightarrow \{t_1', t_2\}}$

- $\dfrac{t_2 \rightarrow t_2'}{\{v_1, t_2\} \rightarrow \{v_1, t_2'\}}$
Wiemy, że $\Gamma \vdash \{v_1, t_2\} : T$, chcemy $\Gamma \vdash \{v_1, t_2'\} : T$.
Z (*) dla $\Gamma \vdash \{v_1, t_2\} : T$, wiemy że $T = T_1 \wedge T_2$ i $\Gamma \vdash t_2 : T_2$.
Mając powyższe i $t_2 \rightarrow t_2'$ dostajemy $\Gamma \vdash t_2' : T_2$

$$
\dfrac{\Gamma \vdash v_1 : T_1 \quad \Gamma \vdash t_2' : T_2}{\Gamma \vdash \{v_1, t_2'\} : T_1 \wedge T_2}
$$
Koniec

$\blacksquare{}$

#### Lemat o inwersji

X1. Jeśli $\Gamma \vdash t.1 : T$, to $\Gamma \vdash t : T \wedge T_2$
Y1. Jeśli $\Gamma \vdash \{x, y\} : T_1 \wedge T_2$, to $\Gamma \vdash x : T_1$ i $\Gamma \vdash y :T_2$
Z1. Jeśli $\Gamma \vdash \{x, y\} : T$, to $T = T_1 \wedge T_2$, $\Gamma \vdash x : T_1$ i $\Gamma \vdash y :T_2$