---
# System prepended metadata

title: Lista 11
tags: [jp21]

---

# Lista 11
###### tags: `jp21`

$$
\newcommand{\ov}[1]{\overline{#1}}
\newcommand{\dg}[1]{{#1}^\dagger}
$$

## (opcjonalne) Continuation-passing style

ELI5: Zamiast zwracać wynik, dostajemy funkcję którą wywołujemy z naszym wynikiem jako argumentem.

# Zadanie 1

Translacja termów:
\begin{align}
\ov{v} &= \lambda k.\ k\ \dg{v} \\
\ov{t_1\ t_2} &= \lambda k. \ov{t_1}\ (\lambda f.\ov{t_2}\ (\lambda x. f\ x\ k)) \\
\dg{x} &= x \\
\dg{(\lambda x. t)} &= \lambda x. \bar{t}
\end{align}


1. $\ov{x(yz)} = \lambda k. \ov{x} (\lambda f. \ov{yz}(\lambda a. f a k)) = \lambda k. (\lambda k. kx) (\lambda f. [ \lambda k. (\lambda k. ky) (\lambda f. (\lambda k. kz)(\lambda b. f b k))](\lambda a. f a k))$

To teraz redukujemy. [] <- to jest w przykładzie
$\lambda k. (\lambda k. kx) (\lambda f. [ \lambda k_1. yz k_1 ](\lambda a. f a k)) \rightarrow \lambda k. y z (\lambda a. x a k)$

2. 

$\ov{(\lambda a. \lambda b. a b)} = \lambda k''. k'' (\lambda a. (\lambda k'''. k''' (\lambda b. \ov{ab})))$

$\ov{(\lambda a. \lambda b. a b) c d} = \lambda k. [\lambda k'. \{\lambda k''. k'' (\lambda a. (\lambda k'''. k''' (\lambda b. \ov{ab})))\} (\lambda f. (\lambda k''. k''c)(\lambda x. f x k'))] (\lambda f'. (\lambda k''. k'' d)(\lambda x'. f' x' k))$


Po redukcji:

$$\lambda k. [\lambda k'. \{\lambda k''. k'' (\lambda a. (\lambda k'''. k''' (\lambda b. \ov{ab})))\} (\lambda f. (\lambda k''. k''c)(\lambda x. f x k'))] (\lambda f'. (\lambda k''. k'' d)(\lambda x'. f' x' k))\\
\rightarrow \\
\lambda k. [\lambda k'. \{\lambda k''. k'' (\lambda a. (\lambda k'''. k''' (\lambda b. \ov{ab})))\} (\lambda f. (\lambda k''. k''c)(\lambda x. f x k'))] (\lambda f'. (\lambda x'. f' x' k)d)\\
\rightarrow \\
\lambda k. [\lambda k'. \{\lambda k''. k'' (\lambda a. (\lambda k'''. k''' (\lambda b. \ov{ab})))\} (\lambda f. (\lambda k''. k''c)(\lambda x. f x k'))] (\lambda f'.  f' d k)\\
\rightarrow \\
\lambda k. [\lambda k'. \{\lambda k''. k'' (\lambda a. (\lambda k'''. k''' (\lambda b. \ov{ab})))\} (\lambda f. (\lambda x. f x k') c)] (\lambda f'.  f' d k)\\
\rightarrow \\
\lambda k. [\lambda k'. \{\lambda k''. k'' (\lambda a. (\lambda k'''. k''' (\lambda b. \ov{ab})))\} (\lambda f. f  c k')] (\lambda f'.  f' d k)\\
\rightarrow \\
\lambda k. [\lambda k'. \{(\lambda f. f  c k') (\lambda a. (\lambda k'''. k''' (\lambda b. \ov{ab})))\} ] (\lambda f'.  f' d k)\\
\rightarrow \\
\lambda k. [\lambda k'. \{   (\lambda a. (\lambda k'''. k''' (\lambda b. \ov{ab})))c k'\} ] (\lambda f'.  f' d k)\\
\rightarrow \\
\lambda k. [   (\lambda a. (\lambda k'''. k''' (\lambda b. \ov{ab})))c (\lambda f'.  f' d k) ]\\
\rightarrow \\
\lambda k. [   (\lambda a. (\lambda k'''. k''' (\lambda b. (\lambda m. a b m))))c (\lambda f'.  f' d k) ] $$


symulacja i niezależność. Przykłady.

$t = II = (\lambda x. x)(\lambda y. y)$
$\ov{t} = \lambda k. (\ov{\lambda x. x})(\lambda f. (\ov{\lambda y.y}) (\lambda z. f z k)) =  
\lambda k. (\lambda k'. k' (\lambda x. (\lambda k''. k''x)))(\lambda f. (\lambda k'. k' (\lambda y. (\lambda k''. k''y)))(\lambda z. f z k))$

$$\ov{t}(\lambda a. a) \to_v\\
(\lambda k'. k' (\lambda x. (\lambda k''. k''x)))(\lambda f. (\lambda k'. k' (\lambda y. (\lambda k''. k''y)))(\lambda z. f z (\lambda a. a)))\to_v\\
[\lambda k'. k' (\lambda x. (\lambda k''. k''x))][\lambda f. ((\lambda z. f z (\lambda a. a)) (\lambda y. (\lambda k''. k''y)))]\to_v\\
[\lambda f. ((\lambda z. f z (\lambda a. a)) (\lambda y. (\lambda k''. k''y)))] (\lambda x. (\lambda k''. k''x))\to_v\\
[\lambda z. (\lambda x. (\lambda k''. k''x)) z (\lambda a. a)] (\lambda y. (\lambda k''. k''y))\to_v\\
 (\lambda x. (\lambda k''. k''x)) (\lambda y. (\lambda k''. k''y)) (\lambda a. a) \to_v\\
  (\lambda k''. k'' (\lambda y. (\lambda k''. k''y)))  (\lambda a. a)   \to_v\\
    (\lambda a. a) (\lambda y. (\lambda k''. k''y))  \to_v\\
   (\lambda y. (\lambda k''. k''y))  = \dg{I}$$
   
   $$\ov{t}(\lambda a. a) \to_n\\
(\lambda k'. k' (\lambda x. (\lambda k''. k''x)))(\lambda f. (\lambda k'. k' (\lambda y. (\lambda k''. k''y)))(\lambda z. f z (\lambda a. a))) \to_n\\
[\lambda f. (\lambda k'. k' (\lambda y. (\lambda k''. k''y)))(\lambda z. f z (\lambda a. a))](\lambda x. (\lambda k''. k''x))\to_n\\
 [\lambda k'. k' (\lambda y. (\lambda k''. k''y))](\lambda z. (\lambda x. (\lambda k''. k''x)) z (\lambda a. a))\to_n\\
 [\lambda z. (\lambda x. (\lambda k''. k''x)) z (\lambda a. a)](\lambda y. (\lambda k''. k''y))\to_n\\
 (\lambda x. (\lambda k''. k''x)) (\lambda y. (\lambda k''. k''y))(\lambda a. a)\to_n\\
  (\lambda k''. k''(\lambda y. (\lambda k''. k''y))) (\lambda a. a) \to_n\\
 (\lambda a. a)(\lambda y. (\lambda k''. k''y))\to_n\\
 \lambda y. (\lambda k''. k''y) =  \dg{I}$$
# Zadanie 2

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


# Zadanie 3

Translacja typów:
$$
\ov{T_0 \rightarrow T_1} = \ov{T_0} \rightarrow ((\ov{T_1} \rightarrow o) \rightarrow o)
$$
$$
\ov{\tau} = \tau
$$

Translacja kontekstów:
$$
\ov{\Gamma} =\{ x \ : \ov{T} \ dla \ x \ : T \in \Gamma \} \\
\ov{\emptyset} = \emptyset \quad \ov{x:T, \Gamma} = x:\ov{T}, \ov{\Gamma}
$$

---

**Założenia**: $\Gamma \vdash t : T$
**Teza**: $\ov{\Gamma} \vdash \bar{t} : (\ov{T} \to o) \to o$
**Dowód**:
Indukcja względem struktury $t$.

1)$t = x$ 
$\ov{t} = \lambda k \ : \ (\ov{T} \rightarrow o). k \ x$

$\ov{\Gamma} \vdash \ov{t}  \ : (\ov{T} \rightarrow o) \rightarrow o$

2)$t = \lambda x. t'$

Jeżeli $\Gamma \vdash t : T$ to z inwersji $T = T_0 \rightarrow T_1$ oraz  $\Gamma \vdash t' : T_1$ oraz $\Gamma \vdash t' : T_1$ czyli z ZI $x \ : \ov{T_0},\ov{\Gamma} \vdash \ov{t'} : (\ov{T_1} \rightarrow o )\rightarrow o$

3)$t = t_1t_2$

Z inwersji $\Gamma \vdash t_1 : T_0 \rightarrow T_1$ oraz $\Gamma \vdash t_2 : T_0$. Z tego z ZI $\ov{\Gamma} \vdash \ov{t_1} : (\ov{T_0 \rightarrow T_1} \rightarrow o) \rightarrow o$ oraz $\ov{\Gamma} \vdash t_2 : (\ov{T_0} \rightarrow o) \rightarrow o$

$\blacksquare{}$

---

![](https://i.imgur.com/XykjxyL.jpg)

![](https://i.imgur.com/sZE2jOb.jpg)
![](https://i.imgur.com/wnd5FdX.jpg)
![](https://i.imgur.com/hLG5A8N.jpg)



# Zadanie 4

Przypomnienie:
$$
\dfrac{\Gamma \vdash t : Cont\ T \to T}{\Gamma \vdash letcc\ t : T}\qquad
\dfrac{\Gamma \vdash t_1 : Cont\ T \quad \Gamma \vdash t_2 : T}{
\Gamma \vdash throw\ t_1\ t_2 : S
}
$$

Rozszerzenie translacji termów:

\begin{align}
\ov{letcc\ t} &=\ ? \\
\ov{throw\ t_1\ t_2} &=\ ?
\end{align}

Rozszerzenie translacji typów:
$$
\ov{Cont\ T} =\ ?
$$

---

**Założenia**: $\Gamma \vdash t : T$
**Teza**: $\ov{\Gamma} \vdash \bar{t} : (\ov{T} \to o) \to o$
**Dowód**:
...

$\blacksquare{}$

--

> Zilustruj następnie na przykładzie redukcję termów powstałych przez translację termów używających operatorów $letcc$ i $throw$.

# Zadanie 5

$$\ov{t_1\ t_2} = \lambda k. \ov{t_1}\ (\lambda f.\ov{t_2}\ (\lambda x. f\ x\ k))$$

$$\ov{t_1\ t_2} = \lambda k. \ov{t_1}\ (\lambda f. f\ (\lambda \_.\ov{t_2} (\lambda y.y))\ k))$$

$$\dg{x} = (x \ (\lambda y. y))$$