Ciele
- Syntaktická analýza termov
- Voľné a viazané premenné
- Vyhodnotenie termov $\beta,\alpha,\eta-redukcia$
- Churchove kódovanie
Úvod
V rámci cvičenia bude Vašou úlohou si predcvičiť syntaktickú aj sémantickú manipuláciu s termami $\lambda$-kalkulu.
Poznámka
Všetky potrebné pojmy aj postupy ako aj riešené príklady sú prezentované v prvej resp. druhej prednáške.
Postup
Krok 1
Syntaktická analýza termov
Pridajte to nasledujúcich termov čo najviac zátvoriek tak, aby ste nezmenili jeho sémantiku
Úloha 1.1
$$\lambda x.x\ z\ \lambda y. x\ y$$
Riešenie
$$\lambda x.(\ (\ x\ z\ ) (\ \lambda y. (\ x\ y\ )\ )\ )$$
Úloha 1.2
$$ (\lambda x.x\ z)\ \lambda y.w\ \lambda w.w\ y\ z\ x $$
Riešenie
$$ (\lambda x.(\ x\ z\ )\ )\ \lambda y.(\ w\ \lambda w.(\ (\ (\ w\ y\ )\ z\ )\ x\ ) \ ) $$
Úloha 1.3
$$ (\lambda z.z) \ (\lambda y.y\ y) \ (\lambda x.x\ a) $$
Riešenie
$$ (\ (\lambda z.z) \ (\lambda y.(\ y\ y\ )\ )\ ) \ (\lambda x.(\ x\ a\ )\ ) $$
Krok 2
Voľné a viazané premenné
Určte, ktoré premenné sú voľné a ktoré viazané v následujúcich $\lambda$-termoch
Úloha 2.1
$$\lambda x.x\ z\ \lambda y. x\ y$$
Úloha 2.2
$$ (\lambda x.x\ z)\ \lambda y.w\ \lambda w.w\ y\ z\ x $$
Úloha 2.3
$$ (\lambda z.z) \ (\lambda y.y\ y) \ (\lambda x.x\ a) $$
Krok 3
Vyhodnotenie $\lambda$-termov
Využitím $\beta$-redukcie, prípadne $\alpha$-redukcie či $\eta$-redukcie nájdite normálnu formu termov $\lambda$-kalkulu.
Poznámka
Sémantiku $\lambda$-kalkulu sme definovali na základe redukčnej stratégie volania hodnotou.
Úloha 3.1
$$ (\lambda z.z) \ (\lambda y.y\ y) \ (\lambda x.x\ a) $$
Riešenie
$$ a\ a $$
Úloha 3.2
$$ (\lambda x.\ \lambda y.x\ y) \ y $$
Riešenie
Nutná $\alpha$-redukcia $y$ za $z$, následne $\eta$-redukcia $$ y $$
Úloha 3.3
$$ (\lambda z.z) \ (\lambda z.z\ z) \ (\lambda z.z\ y) $$
Riešenie
$$ y\ y $$
Úloha 3.4
$$ (\lambda x.\lambda y.x\ y\ y) \ (\lambda a.a) \ b $$
Riešenie
$$ b\ b $$
Úloha 3.5
$$ (\lambda x.\lambda y.x\ y\ y) \ (\lambda y.y) \ y $$
Riešenie
$$ y\ y $$
Úloha 3.6
$$ (\lambda x.x\ x) \ (\lambda y.y\ x) \ z $$
Riešenie
$$ x\ x\ z $$
Úloha 3.7
$$ (\lambda x.\ (\lambda y.\ (x\ y))\ y) \ z $$
Riešenie
Nutná $\alpha$-redukcia. $$ z\ y $$
Úloha 3.8
$$ ((\lambda x.x\ x) \ (\lambda y.y)) \ (\lambda y.y) $$
Riešenie
$$ \lambda y.y $$
Úloha 3.9
$$ ((\lambda x.\ \lambda y.(x\ y)) \ (\lambda y.y)) \ w $$
Riešenie
$$ w $$
Krok 4
Programovanie v $\lambda$-kalkule
V rámci druhej prednášky bol predstavený spôsob ako je možné definovať viaceré programovacie konštrukcie a hodnoty ako kombinátory $\lambda$-kalkulu.
Nájdite normálnu formu následujúcich termov:
Úloha 4.1
$$ test\ true\ true\ false$$
Úloha 4.2
$$ test\ false\ true\ false$$
Úloha 4.3
$$ and\ false\ true$$
Úloha 4.4
$$ test\ (or\ true\ false)\ true\ false$$
Úloha 4.5
$$ and\ (iszero\ 0)\ (test\ (iszero\ 0)\ true\ false)$$
Úloha 4.6
$$plus\ 1\ 0$$
Úloha 4.7
$$plus\ 3\ 1$$
Úloha 4.8
$$plus\ 0\ 3$$
Úloha 4.9
$$times\ 0\ 2$$
Úloha 4.10
$$times\ 2\ 0$$
Úloha 4.11
$$snd\ (pair\ (and\ true\ false)\ 3)$$
Definícia nových funkcií
Úloha 4.12
Definujte operáciu implikácie ako $\lambda$-term.
Úloha 4.13
Definujte operáciu XOR ako $\lambda$-term.
Úloha 4.14
Definujte operáciu, ktorá priráta ku každému číslu 2 ako $\lambda$-term.
Úloha 4.15
Definujte operáciu, ktorá vynásobí každé číslo 2 krát a priráta 1 ako $\lambda$-term.
Úloha 4.16
Definujte operáciu dvojitej negácie ako $\lambda$-term.