Ciele
- Definovať a vyhodnotiť rekurzívne funkcie v $\lambda$ -kalkule pomocou Churchovho kódovania a Curryho kombinátora $Y$ .
Úvod
Na cvičení budete definovať a vyhodnocovať rekurzívne funkcie v netypovanom $\lambda$-kalkule. Používajte Churchove čísla $\mathbf{0},\mathbf{1},\ldots$ a kombinátory $test$, $iszero$, $equal$, $succ$, $pred$, $plus$ a $times$ z druhej prednášky. V definíciách $\lambda$-termov zapisujte operácie ako aplikácie týchto kombinátorov.
Nasledujúce matematické rekurzívne definície opisujú požadované správanie funkcií na prirodzených číslach; samy ešte nie sú definíciami uzavretých $\lambda$-termov. Čísla v nich patria do metajazyka. Pri prechode do $\lambda$-kalkulu používajte Churchove čísla, podmienky vyjadrite pomocou $test$ a odčítanie jednotky pomocou $pred$.
Rekurzívny odkaz nahraďte parametrom $f$ a zostavte nerekurzívne telo $G$. Výslednú funkciu potom definujte ako $Y\,G$, kde
$$ Y=\lambda f.(\lambda x.f\,(x\,x))(\lambda x.f\,(x\,x)). $$
Názvy kombinátorov sú metajazykové skratky. Uzavretosť termu overujte po ich rozvinutí. Pri výpočtoch rozlišujte jeden krok $\to_\beta$, viac krokov $\to_\beta^*$ a ekvivalenciu $=_\beta$. Prvé rozvinutie rekurzie a výber vetvy ukážte podrobne; opakujúce sa časti môžete skrátiť pomocou $\to_\beta^*$. Na získanie úplného Churchovho výsledku použite normálne poradie. Didakticky zvolený sled iných platných krokov označte ako všeobecnú $\beta$-redukciu.
Poznámka
Riešený príklad faktoriálu s kombinátorom $Y$ nájdete v druhej prednáške. Rekurzívne sčítanie a násobenie v tomto cvičení označujte $plus_{rec}$ a $times_{rec}$, aby sa neplietli s už zavedenými kombinátormi $plus$ a $times$.
Postup
Krok 1
Rekurzívne funkcie
Úloha 1.1
Definujte sčítanie podľa matematickej rekurzívnej definície:
$$ plus(m,n)=\begin{cases} m & \text{ak } n=0,\\ plus(m+1,n-1) & \text{ak } n>0. \end{cases} $$
kde $m,n\in\mathbb{N}$.
- Zapíšte požadovanú rekurzívnu rovnicu v $\lambda$-kalkule pomocou Churchových kombinátorov.
- Rekurzívny odkaz nahraďte parametrom $f$ a definujte uzavreté nerekurzívne telo $G$.
- Definujte výsledný uzavretý $\lambda$-term $plus_{rec}$ pomocou $Y\,G$ a overte, že spĺňa rekurzívnu rovnicu.
- Vypočítajte úplný normálny tvar pre argumenty $\mathbf{3}$ a $\mathbf{2}$. Výsledok zapíšte ako Churchovo číslo.
- Vysvetlite, prečo rekurzívne volania pre Churchove prirodzené vstupy dosiahnu základný prípad a prečo sa nepoužitá vetva pri nestriktnom vyhodnotení nevyhodnotí.
Úloha 1.2
Definujte odčítanie orezané na nule podľa matematickej rekurzívnej definície:
$$ minus(m,n)=\begin{cases} m & \text{ak } n=0,\\ minus(\max(m-1,0),n-1) & \text{ak } n>0. \end{cases} $$
kde $m,n\in\mathbb{N}$.
Overte aj $minus\,\mathbf{2}\,\mathbf{3}\to_\beta^*\mathbf{0}$. Využite, že $pred\,\mathbf{0}\to_\beta^*\mathbf{0}$.
- Zapíšte požadovanú rekurzívnu rovnicu v $\lambda$-kalkule pomocou Churchových kombinátorov.
- Rekurzívny odkaz nahraďte parametrom $f$ a definujte uzavreté nerekurzívne telo $G$.
- Definujte výsledný uzavretý $\lambda$-term $minus$ pomocou $Y\,G$ a overte, že spĺňa rekurzívnu rovnicu.
- Vypočítajte úplný normálny tvar pre argumenty $\mathbf{3}$ a $\mathbf{2}$. Výsledok zapíšte ako Churchovo číslo.
- Vysvetlite, prečo rekurzívne volania pre Churchove prirodzené vstupy dosiahnu základný prípad a prečo sa nepoužitá vetva pri nestriktnom vyhodnotení nevyhodnotí.
Úloha 1.3
Definujte násobenie podľa matematickej rekurzívnej definície:
$$ times(m,n)=\begin{cases} 0 & \text{ak } n=0,\\ m+times(m,n-1) & \text{ak } n>0. \end{cases} $$
kde $m,n\in\mathbb{N}$.
Na sčítanie v tele použite už zavedený kombinátor $plus$.
- Zapíšte požadovanú rekurzívnu rovnicu v $\lambda$-kalkule pomocou Churchových kombinátorov.
- Rekurzívny odkaz nahraďte parametrom $f$ a definujte uzavreté nerekurzívne telo $G$.
- Definujte výsledný uzavretý $\lambda$-term $times_{rec}$ pomocou $Y\,G$ a overte, že spĺňa rekurzívnu rovnicu.
- Vypočítajte úplný normálny tvar pre argumenty $\mathbf{3}$ a $\mathbf{2}$. Výsledok zapíšte ako Churchovo číslo.
- Vysvetlite, prečo rekurzívne volania pre Churchove prirodzené vstupy dosiahnu základný prípad a prečo sa nepoužitá vetva pri nestriktnom vyhodnotení nevyhodnotí.
Úloha 1.4
Definujte Fibonacciho funkciu podľa matematickej rekurzívnej definície:
$$ fib(n)=\begin{cases} 0 & \text{ak } n=0,\\ 1 & \text{ak } n=1,\\ fib(n-1)+fib(n-2) & \text{ak } n>1. \end{cases} $$
kde $n\in\mathbb{N}$.
Výraz $n-2$ vyjadrite dvoma aplikáciami $pred$; na sčítanie použite $plus$.
- Zapíšte požadovanú rekurzívnu rovnicu v $\lambda$-kalkule pomocou Churchových kombinátorov.
- Rekurzívny odkaz nahraďte parametrom $f$ a definujte uzavreté nerekurzívne telo $G$.
- Definujte výsledný uzavretý $\lambda$-term $fib$ pomocou $Y\,G$ a overte, že spĺňa rekurzívnu rovnicu.
- Vypočítajte úplný normálny tvar pre argument $\mathbf{3}$. Výsledok zapíšte ako Churchovo číslo.
- Vysvetlite, prečo rekurzívne volania pre Churchove prirodzené vstupy dosiahnu základný prípad a prečo sa nepoužitá vetva pri nestriktnom vyhodnotení nevyhodnotí.
Úloha 1.5
Definujte umocňovanie podľa matematickej rekurzívnej definície:
$$ power(a,b)=\begin{cases} 1 & \text{ak } b=0,\\ a\cdot power(a,b-1) & \text{ak } b>0. \end{cases} $$
kde $a,b\in\mathbb{N}$.
Na násobenie v tele použite už zavedený kombinátor $times$. Definícia určuje aj $power(0,0)=1$.
- Zapíšte požadovanú rekurzívnu rovnicu v $\lambda$-kalkule pomocou Churchových kombinátorov.
- Rekurzívny odkaz nahraďte parametrom $f$ a definujte uzavreté nerekurzívne telo $G$.
- Definujte výsledný uzavretý $\lambda$-term $power$ pomocou $Y\,G$ a overte, že spĺňa rekurzívnu rovnicu.
- Vypočítajte úplný normálny tvar pre argumenty $\mathbf{2}$ a $\mathbf{3}$. Výsledok zapíšte ako Churchovo číslo.
- Vysvetlite, prečo rekurzívne volania pre Churchove prirodzené vstupy dosiahnu základný prípad a prečo sa nepoužitá vetva pri nestriktnom vyhodnotení nevyhodnotí.
Úloha 1.6
Definujte súčet čísel od nuly po vstup podľa matematickej rekurzívnej definície:
$$ sum(n)=\begin{cases} 0 & \text{ak } n=0,\\ n+sum(n-1) & \text{ak } n>0. \end{cases} $$
kde $n\in\mathbb{N}$.
Na sčítanie v tele použite už zavedený kombinátor $plus$.
- Zapíšte požadovanú rekurzívnu rovnicu v $\lambda$-kalkule pomocou Churchových kombinátorov.
- Rekurzívny odkaz nahraďte parametrom $f$ a definujte uzavreté nerekurzívne telo $G$.
- Definujte výsledný uzavretý $\lambda$-term $sum$ pomocou $Y\,G$ a overte, že spĺňa rekurzívnu rovnicu.
- Vypočítajte úplný normálny tvar pre argument $\mathbf{3}$. Výsledok zapíšte ako Churchovo číslo.
- Vysvetlite, prečo rekurzívne volania pre Churchove prirodzené vstupy dosiahnu základný prípad a prečo sa nepoužitá vetva pri nestriktnom vyhodnotení nevyhodnotí.