---
# System prepended metadata

title: Postęp i zachowanie typu

---

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$

![](https://i.imgur.com/bW5BBrP.png)

![](https://i.imgur.com/O31K0n8.png)


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)$$