Arytmetyka w rachunku lambda

Arytmetyka w rachunku lambda

Arytmetyka w rachunku lambda opiera się na liczbach naturalnych Churcha.

Następnik

Funkcja następnika, oznaczana jako $S$, jest zdefiniowana jako:
$S\; \backslash equiv\; \backslash lambda\; xyz.y(xyz).$
Funkcja ta dodaje jedno wywołanie do danej liczby, co skutkuje zwiększeniem jej wartości o jeden.

Dodawanie

Dodawanie dwóch liczb naturalnych Churcha $K$ i $L$ realizuje się przez zastosowanie funkcji następnika $K$-krotnie do liczby $L$:
$\backslash oplus\; \backslash equiv\; \backslash lambda\; xy.\; x\; S\; y.$
Z definicji wynika, że funkcja $f$ jest stosowana $K$-krotnie do zmiennej $x$.

Mnożenie

Mnożenie w rachunku lambda definiuje się następująco:
$\backslash otimes\; \backslash equiv\; \backslash lambda\; xyz.x(yz).$
Obliczając iloczyn $\backslash otimes\; x\; y$, powielamy termin $(yz)$ $x$-krotnie, co daje wynik $x\; \backslash times\; y.$

Poprzednik

Poprzednik liczby $K$ określamy jako liczbę $L$, dla której następnikiem jest $K$:
$P(K)\; =\; L\; \backslash iff\; S(L)\; =\; K.$
Funkcję poprzednika $P$ definiujemy jako:
$P\; \backslash equiv\; \backslash lambda\; n.\; (n\; \backslash Psi\; (\; \backslash lambda\; z.z00))F.$
Funkcja $\backslash Psi$ tworzy parę $(a+1,a)$.

Odejmowanie

Odejmowanie realizowane jest przez wielokrotne zastosowanie funkcji poprzednika:
$\backslash ominus\; \backslash equiv\; \backslash lambda\; xy.y\; P\; x.$
Należy pamiętać, że odejmowanie nie jest operacją przemienną.

Potęgowanie

Potęgowanie $x^y$ przeprowadza się przez wielokrotne mnożenie:
$x^y\; =\; \backslash underbrace\{x*x*\backslash ldots*x\}\_\{y\backslash text\{-razy\}\}.$
W rachunku lambda zapis potęgowania można zrealizować jako:
$\backslash mbox\{pow\}\; \backslash equiv\; \backslash lambda\; xy.\; (y\backslash Xi(\backslash lambda\; z.z\; 1\; x))T.$
Funkcja $\backslash Xi$ zwraca parę $(a*x,x)$, a aplikując ją $y$-krotnie do pary $(1,x)$, otrzymujemy wynik $x^y.$

Podsumowanie

Rachunek lambda umożliwia definiowanie podstawowych operacji arytmetycznych, takich jak dodawanie, odejmowanie, mnożenie, dzielenie i potęgowanie, za pomocą funkcji opartych na liczbach naturalnych Churcha.