# JP Kolokwium

## Lista 2 Zadanie 5

Reguły małych kroków:
$$
\frac{}{false \texttt{ AND } t_2 \rightarrow false}
$$

$$
\frac{}{true \texttt{ AND } t_2 \rightarrow t_2}
$$

$$
\frac{t_1 \rightarrow t_1'}{t_1 \texttt{ AND } t_2 \rightarrow t_1' \texttt{ AND } t_2}
$$

Reguły dużych kroków:
$$
\frac{t_1 \Downarrow false}{t_1 \texttt{ AND } t_2 \Downarrow false}
$$

$$
\frac{t_1 \Downarrow true
\hspace{20pt}
t_2 \Downarrow v_2
}{t_1 \texttt{ AND } t_2 \Downarrow v_2}
$$

### Lemat o determinizmie małych kroków

Jeśli $t \rightarrow t'$ i $t \rightarrow t''$ to $t'= t''$.

**Dowód** -- Dla każdej postaci termu $t$ jest on w postaci normalnej, bądź pasuje dokładnie jedna reguła redukcji.

**Postać normalna termu** - wartość albo stuck term

### Lemat o determinizmie dużych kroków

Jeśli $t \Downarrow t'$ i $t \Downarrow t''$, to $t' = t''$.

**Dowód** -- Analogiczny jak dla małych kroków.

### Dowód

($\Rightarrow$) Jeśli $t \rightarrow^{*} v$, to $t \Downarrow v$

Indukcja po strukturze termu $t$.

* Dla $t = v$, teza jest oczywista
* Dla $t = t_1 \texttt{ AND } t_2$, to z zał. indukcyjnego jeśli $t_1 \rightarrow^{*} v_1$, to $t_1 \Downarrow v_1$, analogicznie dla $t_2$ i $v_2$:
* Jeśli $v_1 = false$, to dla małych kroków otrzymujemy $t \rightarrow^{*} false \texttt{ AND } t_2 \rightarrow false$, analogicznie dla dużych kroków z pierwszej reguły. Warto wspomnieć o tym, że możemy tak iterować $t$ (np. osobny lemat).
* Wpp. $v_1 = true$, to dla małych kroków otrzymujemy $t \rightarrow^{*} (true \texttt{ AND } t_2) \rightarrow t_2 \rightarrow^{*} v_2$, analogicznie wychodzi dla dużych kroków z drugiej reguły.

($\Leftarrow$) Jeśli $t \Downarrow v$, to $t \rightarrow^{*} v$

Indukcja po strukturze termu $t$.

* Dla $t = v$ teza jest oczywista
* Dla $t = t_1 \texttt{ AND } t_2$, to z zał. indukcyjnego jeśli $t_1 \Downarrow v_1$, to $t_1 \rightarrow^{*} v_1$, analogicznie dla $t_2$ i $v_2$
* Jeśli $v_1 = false$, to dla małych kroków otrzymujemy $t \rightarrow^{*} false \texttt{ AND } t_2 \rightarrow false$, analogicznie dla dużych kroków z pierwszej reguły.
* Wpp. $v_1 = true$, to dla małych kroków otrzymujemy $t \rightarrow^{*} (true \texttt{ AND } t_2) \rightarrow t_2 \rightarrow^{*} v_2$, analogicznie wychodzi dla dużych kroków z drugiej reguły.

## 5.1


$$
t ::= \texttt{ true } | \texttt{ false } | \, x \, | \, \lambda (x:T).t \, | \, t \, t \, | \, \texttt{if } t \texttt{ then } t \texttt{ else } t
$$

$$
v ::= \texttt{true } | \texttt{ false } | \, \lambda (x:T).t
$$

### Indukcja strukturalna (Progress):

* $t ::= \texttt{true } | \texttt{ false } | \, \lambda (x : T).t$
$t$ jest wartością o konkretnym typie $T$ (typuje się do Bool albo $T\rightarrow T'$)
* $t = \texttt{if } t_1 \texttt{ then } t_2 \texttt{ else } t_3$
$t_1 : \texttt{Bool}$, $t_2 : T$, $t_3 : T$ -- bo $t$ jest dobrze otypowane
Z założenia indukcyjnego $t_1$ musi być wartością bądź $t_1$ redukuje się (jest progres). W przypadku gdy $t_1$ jest wartością (z otypowania jest to $\texttt{true}$ bądź $\texttt{false}$), możemy zastosować jedną z dwóch zasad redukcji ifa -- redukcja do $t_2$ bądź redukcja do $t_3$.
* $t = x$ (przypadek nie może wystąpić -- brak zmiennych wolnych)
* $t = t_1 \, t_2$
Z otypowania mamy, że $t_1 : T_1 \rightarrow T_2$, a $t_2 : T_1$.
* Jeśli $t_1$ bądź $t_2$ nie jest wartością, to z założenia indukcyjnego możemy wykonać progres na $t_1$ bądź $t_2$.
* W przeciwnym przypadku, $t_1, t_2$ są wartościami, z otypowania $t_1$ wiemy więc, że jest to $\lambda$ (lemat o postaciach kanonicznych), więc możemy wykonać podstawienie.

### Indukcja strukturalna (Preservation):

#### Lemat o prezerwacji typów przy podstawieniu

$\Gamma, x : S \vdash t : T \, \land \, \Gamma \vdash s : S \implies \Gamma \vdash [x \rightarrow s]t : T$

* $t = x$, stąd typ $S$ i typ $T$ są takie same. $[x \rightarrow s]t=s$, a więc po podstawieniu uzyskujemy typ $S$, a z poprzedniego faktu wiemy, że jest on równy typowi $T$.
* $t = z \neq x$, po podstawieniu nie zmienimy $t$, więc typ pozostanie niezmieniony.
* $t : T = \lambda z:T_2.t_1$, zgodnie z konwencją zakładamy, że $z$ jest nową zmienną różną od $x$ i $z \notin FV(s)$. Zauważmy, że po rozszerzeniu kontekstu przez $z : T_2$, nie zmieni to otypowania $s$, więc możemy z założenia indukcyjnego skorzystać dla $t_1$. $\Gamma, z:T_2 , x : S \vdash t_1 : T_1 \, \land \, \Gamma, z:T_2 \vdash s : S \implies \Gamma, z:T_2 \vdash [x \rightarrow s]t_1 : T_1$
* $t = \texttt{true } | \texttt{ false}$ (patrz punkt $2$)
* $t = t_1 \, t_2$, z indukcji pokazujemy, że $t_1$ i $t_2$ zachowują typy, więc $t$ również zachowuje typ.
* $t = \texttt{if } t_1 \texttt{ then } t_2 \texttt{ else } t_3$, z indukcji pokazyjemy, że $t_1, t_2, t_3$ zachowują typy, więc $t$ również zachowuje typ.

Dokładnie tak samo, jak progres (przy aplikacji korzystamy z lematu).

* $t ::= \texttt{true } | \texttt{ false } | \, \lambda (x : T).t$ Nieważne, bo nie ma kroku
* $t = \texttt{if } t_1 \texttt{ then } t_2 \texttt{ else } t_3$
$t_1 : \texttt{Bool}$, $t_2 : T$, $t_3 : T$ -- bo $t$ jest dobrze otypowane
Jeśli $t_1$ robi krok, to z zał. indukcyjnego ok.
Jeśli znikamy ifa, to $t_2:T, t_3:T$, więc typ wyrażenia zostaje taki sam
* $t = x$ (przypadek nie może wystąpić -- brak zmiennych wolnych)
* $t = t_1 \, t_2$
Jeśli $t_1, t_2$ robi krok, to z zał. ind. typ zostaje.
Jeśli $t_1, t_2$ to wartości, to $t_1 = \lambda x:T_2. t_3 : T_2 \rightarrow T$ z inwersji, bo $t$ był dobrze otypowany. Z dobrego otypowania lambdy wiemy, że $x:T_2 \vdash t_3:T$. A z dobrego otypowania $t_2$ wiemy, że $\vdash t_2:T_2$. Mamy załozenia lematu o prezerwacji typów. Więc $\vdash [x \rightarrow t_2]t_3 : T$.

## Lista rzeczy o które chcemy dopytać:
- inwersja vs postać kanoniczna
- zapytać o feedback jakiegoś dowodu progress i preservation
- zad. 5.4

## Zadania z konsów powtórkowych

### Progress/preservation (zadanie 9.3)

Najważniejsze rzeczy o których trzeba pamiętać:
- odpowiednio skwantyfikowane obiekty (np. jak powołujemy się na założenie indukcyjne, i rozważamy jakąś gammę/mi/cokolwiek)
- lemat o postaciach kanonicznych/inwersja: one działają w inne strony, stosujemy je zależnie od kierunku rozumowania; nie trzeba ich dowodzić, ale trzeba się powołać tam gdzie ich używamy. Lemat o postaciach kanonicznych mówi o tym jak mogą wyglądać postacie normalne danych typów, a inwersja mówi jaki typ musi mieć term który wygląda w dany sposób.
- ma być niby tylko kawałek dowodu do zrobienia, więc liczy się żeby to co napiszemy było jasne i precyzyjne (można pisać ze coś jest analogiczne, jeśli się już w jednym przypadku to rozpisało dokładnie)

### Rachunek lambda z możliwością leniwej ewaluacji wybranych termów
Jakie są nowe regły?

Składnia:

$$
t :=\ ... | Lt
$$

Reguły:

$$
\frac{t \rightarrow_L t'}{Lt \rightarrow_G Lt'}
$$

$$
\frac{}{Lv \rightarrow_G v}
$$

$$
\frac{}{Lt \rightarrow_L t}
$$

### Izomorfizm typów (zadanie 8.5)

Musimy dokładnie powiedzieć co pokazujemy i jak zachowują się definicje dla pojawiających się u nas typów (np. jak definiujemy ekstensjonalną równość par), a następnie wskazać odpowiednie funkcje $forth$ i $back$. Pewnie też wypada uzasadnić dlaczego ich złożenia dają to co chcemy jeśli nie jest to oczywiste (my tego nie robiliśmy, ale rozważyliśmy tylko pierwszy przykład, gdzie było to widać).

### Generalne uwagi
- piszemy od 10 do 12, ale ma być jakiś dodatkowy czas na wysłanie (chyba 15 min)
- będzie prawdopodobnie wspólne dla obu grup spotkanie na teamsie, gdzie będzie można zadawać pytania do zadań itd.
- mają być 4 zadania: jedno trudniejsze, trzy standardowe
- trudnością ma być czas oraz klarowne zapisanie wszystkiego, dobrze sobie rozplanować jakoś na początku na co ile czasu chcemy wstępnie poświęcić
- zadania należy pisać ręcznie na kartce i wrzucić zdjęcia/skany/itp. na skosa