tags: `jp21`

---

# Postęp i zachowanie typu

## Postęp

$$\Gamma ::= \emptyset ~|~ x:T, \Gamma$$

4Teza: $\emptyset \vdash t : T \Rightarrow t \in V \vee \exists t', t \rightarrow t'$

Dowód: Indukcja względem (struktury) $t$:
- $t = x$:
$\frac{x:T \in \emptyset}{\emptyset \vdash x : T}$, sprzeczność $x:T \in \emptyset$
- $t = \lambda x:T. t' \vee true \vee false$:
t jest wartością :slightly_smiling_face:
- $t = t_1~t_2$:
$t$ się typuje, z lematu o inwersji wiemy, że $t_1$ i $t_2$ się typują (i coś tam jeszcze lemat nam mówi...)
Możemy zastosować ZI do $t_1$:
- $t_1$ jest wartością:
- true/false: nie typuje się :stuck_out_tongue:
- lambdą, $t_1 = \lambda x:S. t_\infty$:
Możemy zastosować ZI do $t_2$:
- $t_2$ jest wartością:
$\frac{}{(\lambda x:S, t_\infty)~t_2 \rightarrow t_\infty[x := t_2]}$
- $t_2 \rightarrow t_2'$ dla pewnego $t_2'$:
$\frac{t_2 \rightarrow t_2'}{t_1~t_2 \rightarrow t_1~t_2'}$ ok!
- $t_1 \rightarrow t_1'$ dla pewnego $t_1'$:
$\frac{t_1 \rightarrow t_1'}{t_1~t_2 \rightarrow t_1'~t_2}$ ok!
- $t = if~t_1~then~t_2~else~t_3$
1. Lemat o inwersji $\Rightarrow$ $t_1, t_2, t_3$ mają typy ($t_1$)
2. ZI dla $t_1$:
- jest wartością:
i Boolem, więc true/false, ewaluuje się do $t_2/t_3$ (odpowiednio)
(lambda nie może)
- robi krok $t_1 \rightarrow t_1'$:
$\frac{t_1 \rightarrow t_1'}{if~t_1 ... \rightarrow if~t_1'...}$

(tutaj w przyszłości będą kolejne przypadki)

$\blacksquare$

## Zachowanie typu

Teza: $? \vdash t : T$ i $t \rightarrow t'$ to $? \vdash t' : T$
Dowód:
Indukcja względem (struktury) $t$:
- $t = x$:
$t \not\rightarrow$, sprzeczność
- $t = \lambda x:T. t' \vee true \vee false$:
t jest wartością, ale $t \rightarrow t'$, sprzeczność
- $t = t_1~t_2$:
Z inwersji $t_1 : B \rightarrow T$, $t_2 : B$.
- $t' = t_1'~t_2$
Z ZI $t_1' : B \rightarrow T$. Wówczas $t' : T : t$.
- $t' = t_1~t_2'$
Z ZI $t_2' : B$. Wówczas $t' : T : t$.
- $t' = t_x[x : = t_2]$ gdzie $t_1 = \lambda x. t_x$

To jest nasze założenie: $? \vdash (\lambda x. t_x)~t_2 : T$.
$\dfrac{\dfrac{?, x:B \vdash t_x : T}{? \vdash \lambda x. t_x : B \rightarrow T}(inwersja) \quad ? \vdash t_2 : B}{? \vdash (\lambda x. t_x)~t_2 : T} (inwersja)$

Pozostaje pokazać $? \vdash t_x[x := t_2] : T$.
Mamy to z lematu o zachowaniu typu przez podstawienie.

- $t = if~t_1~then~t_2~else~t_3$

(tutaj w przyszłości będą kolejne przypadki)

$\blacksquare$



Lemat: $?' \vdash v : S ~\wedge~ \mathbf{\Gamma, x:S \vdash t : T} \Rightarrow~ \Gamma \vdash t [x := v] : T$
Dowód: Indukcja względem wyprowadzenia $\Gamma, x:S \vdash t : T$:
- $t = y$, $\dfrac{y:T \in (\Gamma, x:S)}{\Gamma, x:S \vdash y : T}$

- $y \neq x$
$t [x := v] = y [x := v] = y$
$y:T \in (\Gamma, x:S) \Rightarrow y:T \in \Gamma$

- $t=y=x$
$t [x := v] = x [x := v] = v : S$
$x : S \Rightarrow t : T = S$

- $\dfrac{\Gamma, x:S, y:T_1 \vdash t_2 : T_2}{\Gamma, x:S \vdash \lambda y:T_1.~t_2 : (T_1 \rightarrow T_2)}$

$t = \lambda y:T_1.~t_2$
$t[x := v] = (\lambda y:T_1.~t_2) [x := v] = to zależy$
- $x = y$:
$t[x:= v] = (\lambda y:T_1.~t_2) [x := v] = (\lambda y:T_1.~t_2)=t$
- $x \not= y$:
$t[x := v] = (\lambda y:T_1.~t_2) [x := v] = (\lambda y:T_1.~t_2 [x := v])$

$\dfrac{\Gamma, x:S, y:T_1 \vdash t_2 [x := v] : T_2}{\Gamma, x:S \vdash (\lambda y:T_1.~t_2 [x := v]) : (T_1 \rightarrow T_2)}$

Cel: $\Gamma, x:S, y:T_1 \vdash t_2 [x := v] : T_2$

Jak wygląda założenie indukcyjne?: $\vdash v : S ~\wedge~\Gamma, y:T_1, x:S \vdash t_2 : T_2 \Longrightarrow \Gamma, y : T_1 \vdash t_2[x:=v] : T_2$

z pytania: $\Gamma, y:T_1, x:S \vdash t_2 : T_2$
z czarnej: $\Gamma, x:S, y:T_1 \vdash t_2 : T_2$

> Żeby było pięknie:
> Lemat: $\emptyset \vdash v : S ~\wedge~ \mathbf{\Gamma_1, x:S, \Gamma_2 \vdash t : T} \Rightarrow~ \Gamma_1, \Gamma_2 \vdash t [x := v] : T$

- (aplikacja) prosta

---

### zad 2
Twierdzenie: $t'$ sie typuje oraz $t \rightarrow t'$ to t sie typuje
t = ($\lambda x:Bool.\lambda y:Bool . y)(\lambda z : Bool .z )$

$t \rightarrow \lambda y:Bool . y =t'$
$t' : Bool \rightarrow Bool$

t = if true then true else $(\lambda x : Bool. x)$
t' = true : Bool

$(\lambda x:T. xxx)(\lambda x:T. xxx)$

----
Definicja:

to brzydkie: $c_{n+1} = \lambda s. \lambda z. s^{n+1} z$

ładne: $c_{n+1} = \lambda s. \lambda z. s~(c_n~s~z)$

$$
\Gamma \vdash (\lambda s. \lambda z. z) : T_{Nat}\\
\frac{\Gamma \vdash c_n : T_{Nat}}{\Gamma \vdash (\lambda s. \lambda z.~s (c_n~s~z)) : T_{Nat}}
$$

$$\lambda s. \lambda z.~s (c_n~s~z) = \lambda s. \lambda z.~s ((\lambda s. \lambda z. s^{n} z)~s~z)$$