# JP 8

[JP 7](https://hackmd.io/at5WsD3BTlmuM-6dJdh42Q)

## Zadanie 1

Typowanie: $\frac{t_1 : T_1}{\lambda \_:S.\ t_1 : S \rightarrow T_1}$

Ewaluacja: $\frac{}{(\lambda \_:S.\ t_1)\ v_2 \rightarrow t_1}$

#### Szkic dowodu:

Rozważmy mapowanie z rzeczy z _wildcardami_ w normalny język lambda z $\texttt{Unit}$, $e : \lambda^{W} \rightarrow \lambda^{N}$ (poprzez $\lambda \, \_:S.t$ jest równoznaczna $\lambda x:S.t$, gdzie $x$ nie występuje w $t$). Wtedy:
* $t \rightarrow_{W} t'$ wtw. $e(t) \rightarrow_{N} e(t')$
* $\Gamma \vdash^W t:T$ wtw. $\Gamma \vdash^N e(t) : T$

Indukcja strukturalna (względem struktury rozważanych termów) w obie strony (trywialna).

Dowód (jakiś przypadek):

##### Pierwszy wtw. w obie strony:
$t = (\lambda \_:S.\ t_1) \, v$ -- ewaluuje się do $t_1$ z zasady typowania dla $\rightarrow_{W}$.
$e(t) = (\lambda x. e(t_1)) \, e(v) \rightarrow_{N} [x \mapsto e(v)] e(t_1)$, a ponieważ $x$ nie występuje w $e(t_1)$, to jest to równe $e(t_1)$.

## Zadanie 2


Zdefiniujmy pomocniczy predykat $matchT(x, T)$.

Notacja $(\{l_1=p_1,\ldots \}:\{l_1=T_1, \ldots \}) := \cup\ p_i:T_i$

$$
\frac{\Gamma\,\vdash\, t_1:T_1 \hspace{20pt} matchT(p,\, T_1)\hspace{20pt} \Gamma, p:T_1\,\vdash\, t_2 : T}{\Gamma \, \vdash \, \texttt{let } p = t_1 \texttt{ in } t_2 : T}
$$

$$
\frac{}{matchT(x, T)}
$$

$$
\frac{\forall_i matchT(p_i, T_i)}{matchT(\{l_1=p_1, \ldots, l_n=p_n\}, \{l_1:T_1, \ldots, l_n:T_n\})}
$$

### Progress

#### Lemat (AA o matchach)

Jeśli $matchT(p, T)$ i $v:T$, to $match(p, v)$ istnieje -- dowód: (indukcja strukturalna po $matchT$).

#### Szkic dowodu progress

Indukcja strukturalna po typie:
* $\frac{\Gamma\,\vdash\, t_1:T_1 \hspace{20pt} matchT(p,\, T_1)\hspace{20pt} \Gamma, p:T_1\,\vdash\, t_2 : T_2}{\Gamma \, \vdash \, \texttt{let } p = t_1 \texttt{ in } t_2 : T}$, rozważmy term $t = \texttt{let } p = t_1 \texttt{ in } t_2 : T$.
* Rozważmy $t_1 = v_1$. Wówczas korzystając z reguły $\text{E-LetV}$, otrzymujemy w jednym kroku $match(p, v_1) \ t_2$.
* Wpp. z indukcji istnieje $t_1'$, że $t_1 \rightarrow t_1'$. Wówczas z reguły $\text{E-Let}$ możemy wykonać krok.
* Pozostałe przypadki powinniśmy sprawdzić, ale zakładamy że są w porządku (bo to szkic i ktoś to pewnie już udowodnił). Może się coś popsuć jeśli wcześniej korzystaliśmy z lematów dowodzonych indukcyjnie (nie rozpatrzyliśmy w nich termów w postaci `let...`)

### Preservation

#### Lemat o podstawieniu

* Rozważmy $t = \texttt{let } p = t_1 \texttt{ in } t_2$. Wówczas przy podstawiniu $[x \mapsto v]t = \texttt{let } p = [x \mapsto v] t_1 \texttt{ in } [x \mapsto v] t_2$, nie zmienimy typu. Z indukcji nie zmieniamy typu $t_1$, nie zmieniamy typu $t_2$, więc typ się nie zmienia.
* Pozostałe przypadki analogicznie

#### Szkic dowodu preservation

Indukcja względem wyprowadzenia typu $T$:

* $\frac{\Gamma\,\vdash\, t_1:T_1 \hspace{20pt} matchT(p,\, T_1)\hspace{20pt} \Gamma, p:T_1\,\vdash\, t_2 : T_2}{\Gamma \, \vdash \, \texttt{let } p = t_1 \texttt{ in } t_2 : T}$, rozważmy term $t = \texttt{let } p = t_1 \texttt{ in } t_2 : T$.
* Rozważmy przypadek $t_1 = v_1$. Wówczas z reguły $\text{E-LetV}$ otrzymamy $(\sigma_1 \circ \ldots \circ \sigma_n) \ t_2$, a z lematu o podstawieniu wiemy, że podstawienia zachowują typ.
* Jeśli $t_1$ nie jest wartością, to istnieje $t_1'$, że $t_1 \rightarrow t_1'$. Wówczas korzystamy z dowodu indukcyjnego i mamy, że $t_1'$ ma ten sam typ co $t_1$. Z reguły $\text{E-Let}$ widzimy, że $t$ zachowa typ po jednym kroku.

## Zadanie 3


### Progress

Indukcja względem struktury termu:

* $t = \texttt{case } t_o \texttt{ of inl } x_1 \implies t_1 \texttt{ | inr } x_2 \implies t_2$
* Jeśli istnieje $t_o'$, że $t_o \rightarrow t_o'$, to możemy zrobić krok z $\text{E-Case}$.
* Wpp. $t_o = \texttt{inl } v_0$. Robimy krok z $\text{E-CaseInl}$
* Analogicznie dla $t_o = \texttt{inr } v_0$.
* $t = \texttt{inl } t_1$ -- korzystamy z $\text{E-Inl}$, albo $t_1$ jest wartością (z indukcji)
* $t = \texttt{inr } t_1$ -- analogicznie

### Preservation

#### Lemat o podstawieniu

Lemat się trywialnie rozszerza (każdy przypadek albo korzysta z indukcji, albo zachowuje się jak $\lambda$).

#### Dowód preservation

Indukcja względem struktury termu:
* $t = \texttt{inl } t_1$ -- Krok możemy wykonać, jeśli $t_1$ nie jest wartością, wtedy korzystamy z reguły $\text{E-Inl}$. Z indukcji $t_1$ ma ten sam typ co $t_1'$, czyli możemy $t' = \texttt{inl } t_1'$ otypować w ten sam sposób co $t$. (Ale istnieje też inne typowanie ze względu na to, że nie wiemy jaki typ został by użyty przy konstruktorze $\texttt{inl}$.)
* $t = \texttt{inr } t_1$ -- Analogicznie
* $t = \texttt{case } t_o \texttt{ of inl } x_1 \implies t_1 \texttt{ | inr } x_2 \implies t_2$
* $t_o = \texttt{inl } v_o$. Z $\text{T-Case } t_0 : T_1 + T_2$, a z $\text{T-Inl } v_0 : T_1$, a to ewaluuje się z $\text{E-CaseInl}$ do $[x \mapsto v_o] t_1$. Z lematu o podstawieniu, to typuje się do tego samego typu co $t_1$ ($T$), a z reguły $\text{T-Case}$ $t_1$ i $t$ mają ten sam typ.
* $t_o = \texttt{inr } v_o$. Analogicznie.
* Wpp. istnieje $t_o'$, że $t_o \rightarrow t_o'$. Z indukcji wiemy, że $t_o' : T_1 + T_2$. Więc $t'$ ma ten sam typ co $t$.

## Zadanie 4


:::spoiler Przydatne?
* $\mathcal{T}_A(t)$ wtw. jeśli $t$ się ewaluuje do $v$, że $\mathcal{V}_A(v)$.
* $\mathcal{T}_{T_1 \rightarrow T_2}(t)$ wtw. jeśli $t$ się ewaluuje do $v$, że $\mathcal{V}_{T_1 \rightarrow T_2}(v)$
:::

* $\mathcal{T}_T(t)$ wtw. jeśli $t$ się ewaluuje do $v$, że $\mathcal{V}_T(v)$.
* $\mathcal{V}_{\texttt{Unit}}(v)$ (zachodzi zawsze)
* $\mathcal{V}_{T_1 \rightarrow T_2}(v)$ wtw. jeśli dla dowolnego $s$ (wartości), że $\mathcal{V}_{T_1}(s)$, to $\mathcal{T}_{T_2}(v \ s)$
* $\mathcal{V}_{T_1 \times T_2}(v)$, wtw. gdy $v = \{ v_1, v_2 \}$, $\mathcal{V}_{T_1}(v_1)$ i $\mathcal{V}_{T_2}(v_2)$
* $\mathcal{V}_{T_1 + T_2}(v)$ wtw, gdy:
* Dla $v = \texttt{inl } v_1$, to $\mathcal{V}_{T_1}(v_1)$
* Dla $v = \texttt{inr } v_2$, to $\mathcal{V}_{T_2}(v_2)$

### Lemat o ewaluuacji

Jeśli $t : T$ i $t \rightarrow t'$, to $\mathcal{T}_T(t) \iff \mathcal{T}_T(t')$.

Dowód jest oczywisty z definicji $\mathcal{T}_T$.

### Lemat o termach z podstawieniami

Jeśli $x_1 : T_1, \ldots, x_n : T_n \vdash t : T$ oraz $v_1, \ldots, v_n$ są zamkniętymi wartościami typów $T_1, \ldots, T_n$ spełniającymi $\mathcal{V}_{T_i}(v_i)$, to $\mathcal{T}_T ([x_1 \mapsto v_1] \ldots [x_n \mapsto v_n] \ t)$. Jeśli $t$ jest wartością $v$, to $\mathcal{V}_{T}([x_1 \mapsto v_1] \ldots [x_n \mapsto v_n] \ v)$.

* $t = x_i$, to mamy $\mathcal{T}_{T}([x_1 \mapsto v_1] \ldots [x_n \mapsto v_n] \ t) \iff \mathcal{T}_T(v_i) \iff \mathcal{V}_T(v_i)$, ostatnie zachodzi z założenia indukcyjnego.
* $t = \lambda x:S_1.s_2$, oczywiście $t$ jest wartością $v$, więc chcemy pokazać $\mathcal{V}_{T}([x_1 \mapsto v_1] \ldots [x_n \mapsto v_n] \ v)$. Jako, że $T = T_1 \rightarrow T_2$, to chcemy pokazać, że dla dowolnego $s$, że $\mathcal{V}_{T_1}(s)$ mamy $\mathcal{T}_{T_2}(([x_1 \mapsto v_1] \ldots [x_n \mapsto v_n] \ v) \ s)$, a to sprowadza się do $\mathcal{T}_{T_2}([x_1 \mapsto v_1] \ldots [x_n \mapsto v_n] [x \mapsto s] \ s_2)$, co z tezy indukcyjnej kończy dowód tego przypadku.
* $t = t_1 \ t_2$ -- z tezy indukcyjnej otrzymujemy $\mathcal{T}_{T_{11} \rightarrow T_{12}}([x_1 \mapsto v_1] \ldots [x_n \mapsto v_n] \ t_1)$ i $\mathcal{T}_{T_{11}}([x_1 \mapsto v_1] \ldots [x_n \mapsto v_n] \ t_2)$. W takim razie, sprowadza się $t_1$ do $v_{11}$, a $t_2$ do $v_{12}$. Stąd mamy, że zachodzi $\mathcal{V}_{T_{11} \rightarrow T_{12}}([x_1 \mapsto v_1] \ldots [x_n \mapsto v_n] \ v_{11})$ i $\mathcal{V}_{T_{11}}([x_1 \mapsto v_1] \ldots [x_n \mapsto v_n] \ v_{12})$. A tu z definicji $\mathcal{V}_{T_{11} \rightarrow T_{12}}$ mamy, że $\mathcal{V}_{T_{12}}([x_1 \mapsto v_1] \ldots [x_n \mapsto v_n] \ (v_{11} \ v_{12}))$, czyli (z lematu o ewaluuacji) $\mathcal{T}_{T_{12}}([x_1 \mapsto v_1] \ldots [x_n \mapsto v_n] \ (t_{11} \ t_{12}))$.
* $t = \{ t_1, t_2 \}$ -- indukcyjnie wchodzimy pod $\{ \}$ (musimy przejść do $\mathcal{V}$ i z lematu o ewaluuacji się później cofnąć)
* $t = t_1.1$ -- Schodzimy do wartości $\mathcal{V}$, a następnie korzystamy z definicji produktu dla $\mathcal{V}$ i cofamy się z lematu o ewaluuacji
* $t = t_2.2$ -- Analogicznie jak poprzednio
* $t = \texttt{case } t_0 \texttt{ of inl } x \implies t_1 \ | \texttt{ of inr } x \implies t_2$ -- Schodzimy w $t_0$ aż do wartości, a następnie korzystamy z definicji $\mathcal{V}$ (dla sumy), z której uzyskujemy $\mathcal{V}_{T_{11}}(v_0)$, a więc możemy pod $x$ podstawić $v_0$ w $t_1$ i $t_2$. Później cofając się z lematu o ewaluuacji pokazujemy żądaną tezę.
* $t = \texttt{inl } t_1$ -- Schodzimy do wartości, a następnie korzystamy z definicji sumy dla $\mathcal{V}$, a następnie cofamy się z lematu o ewaluuacji.
* $t = \texttt{inr } t_2$ -- Analogicznie jak poprzedni

## Zadanie 5


$$
\texttt{Unit} \sim \texttt{Unit}
$$

$$
\frac{
v_{11} \sim v_{21} \hspace{20pt}
v_{12} \sim v_{22} }
{\{ v_{11}, v_{12} \} \sim
\{ v_{21}, v_{22} \}}
$$

$$
\frac{v_1 \sim v_2}
{\texttt{inl } v_1 \sim \texttt{inl } v_2}
$$

$$
\frac{v_1 \sim v_2}
{\texttt{inr } v_1 \sim \texttt{inr } v_2}
$$

$$
\frac{
\forall_v (v : T_{\lambda} \hspace{20pt}
[x \mapsto v] t_1 \sim [y \mapsto v] t_2)}
{\lambda x:T_{\lambda}.t_1 \sim \lambda y:T_{\lambda}.t_2}
$$

$$
\frac{
t_1 \rightarrow^{*} v_1 \hspace{20pt}
t_2 \rightarrow^{*} v_2 \hspace{20pt}
v_1 \sim v_2}
{t_1 \sim t_2}
$$

* $S = T \times \texttt{Unit}$, $S \cong T$
* $forth = \lambda x:S. \ x.1$
* $back = \lambda x:T. \ \{ x, \texttt{unit} \}$
* $forth \ (back \ v) = forth \ \{ v, \texttt{unit} \} = v$
* $back \ (forth \ \{ v, \texttt{unit} \}) = back \ v = \{ v, \texttt{unit} \}$
* $(S \times T) \rightarrow U \cong S \rightarrow (T \rightarrow U)$, $A = (S \times T) \rightarrow U$, $B = S \rightarrow (T \rightarrow U)$
* $forth = \lambda x:A. \ (\lambda s:S. \ \lambda t:T. x \ \{ s, t \})$
* $back = \lambda x:B. \ (\lambda y:(S \times T). \ (x \ y.1) \ y.2)$
* $forth \ (back \ (\lambda x:S. t_B)) = forth \ (\lambda y:(S \times T). \ [x \mapsto y.1] t_B \ y.2) =\\ = \lambda s:S. \ \lambda t:T. \ ([x \mapsto s]t_B \ t)$
* W pierwszym kroku wstawiamy wartość $v$ do obu wyrażeń i uzyskujemy $[x \mapsto v] t_B$, a w tym drugim wyrażeniu mamy $\lambda t:T. \ [s \mapsto v]([x \mapsto s]t_B \ t)$. Ponieważ $t$ jest zamkniętą wartością, to jest to równoważne $\lambda t:T. \ ([x \mapsto v] t_B \ t)$
* Z definicji $\sim$ na termach, zredukujmy $[x \mapsto v] t_B$ to wartości, jako że ma to typ $T \rightarrow U$, to musi to być $\lambda t:T. t_u$. Teraz chcemy porównać to z poprzednią wartością $\lambda t:T. \ ([x \mapsto v] t_B \ t)$. Z reguły dla $\lambda$ wstawmy dowolną wartość $v_t$. Z lewej strony uzyskamy $[t \mapsto v_t] t_u$, a z prawej $[x \mapsto v] t_B \ v_t$. Ale wiemy, że $[x \mapsto v]t_B \rightarrow^{*} \lambda t:T. t_u$. Stąd otrzymujemy, że prawa strona, to $[t \mapsto v_t] t_u$. Skoro uzyskujemy te same termy, to z pewnością są one w relacji $\sim$.
* $back \ (forth \ (\lambda x:(S \times T). t_A)) = back \ (\lambda s:S. \ \lambda t:T. \ [x \mapsto \{s, t\}]t_A) =\\ = \lambda y:(S \times T). \ [x \mapsto y] \ t_A$
* Równość izomorficzna jest oczywista -- pierwsze jest $[x \mapsto v] t_A$, a drugie to $[y \mapsto v] [x \mapsto y] t_A$, co oczywiście jest równoważne.

* $(\texttt{Unit} + \texttt{Unit}) \rightarrow T \cong T \times T$, $A = (\texttt{Unit} + \texttt{Unit}) \rightarrow T, B = T \times T$
* $forth = \lambda x:A. \ \{x\ (\texttt{inl } \texttt{unit}),\ x\ (\texttt{inr } \texttt{unit})\}$
* $back = \\\lambda t : T\times T. \\ \lambda u : (\texttt{Unit} + \texttt{Unit}). \\ \texttt{case }u\texttt{ of inl } x \implies t.1 \ | \ \texttt{inr } x \implies t.2$
* $back (forth (\lambda u: (\texttt{Unit} + \texttt{Unit}). t)) =\\ = back (\{[u\mapsto \texttt{inl unit}] \ t, [u\mapsto \texttt{inr unit}] \ t\})=\\ = \lambda v :(\texttt{Unit} + \texttt{Unit}). \\\texttt{case } v \texttt{ of inl } x \implies [u\mapsto \texttt{inl unit}] t \ | \ \texttt{inr } x \implies [u\mapsto \texttt{inr unit}] \ t$
* Podstawmy dowolną wartość do obu wyrażeń. Wówczas oba wyrażenia zwrócą nam to samą wartość (ponieważ $x$ nie występuje w $t$, więc to podstawienie możemy zignorować), więc są w relacji $\sim$.
* $forth (back (\{v_1, v_2\})) \\= forth (\lambda\ u.\ \texttt{case}\ u\ \texttt{of inl}\ x \implies v_1 | \texttt{inr}\ x \implies v_2) \\= \{(\lambda\ u.\ \texttt{case}\ u\ \texttt{of inl}\ x \implies v_1 | \texttt{inr}\ x \implies v_2)\ (\texttt{inl}\ \texttt{unit}), \\ \hspace{14pt} (\lambda\ u.\ \texttt{case}\ u\ \texttt{of inl}\ x \implies v_1 | \texttt{inr}\ x \implies v_2)\ (\texttt{inr}\ \texttt{unit})\}$
* W dwóch krokach zewaluujemy się do $\{v_1, v_2\}$, to jest to samo co było początkowym argumentem, więc oczywiście jest z nim w relacji $\sim$.