Arytmetyka w rachunku lambda

Arytmetyka w rachunku lambda – rodzaj arytmetyki związanej z rachunkiem lambda, opierającej się na liczbach naturalnych Churcha.

Następnik

Funkcja $S$ następnika jest zdefiniowana następująco:

$S\equiv \lambda xyz.y(xyz).$

Procedura ta nie robi nic innego jak „dodaje” jeszcze jedno wywołanie funkcji do pewnej liczby, przez co staje się ona liczbą o jeden większą.

Dodawanie

Aby dodać dwie liczby naturalne Churcha $K$ i $L$ należy $K$-krotnie zaaplikować funkcję następnika do liczby $L$ (lub na odwrót, dodawanie jest przemienne):

$\oplus \equiv \lambda xy.xSy.$

Z definicji liczb naturalnych Churcha wiemy, że wywołując funkcję pewnej liczby $K$ na dwóch argumentach – funkcji $f$ i zmiennej $x,$ aplikujemy funkcję $f$ $K$-krotnie do zmiennej $x.$

Mnożenie

Mnożenie w rachunku lambda zdefiniowane jest następująco:

$\otimes \equiv \lambda xyz.x(yz).$

Obliczając według tej funkcji iloczyn $\otimes xy,$ $x$-krotnie powielamy term $(yz),$ po czym podstawiając $y$ przy każdym $x$-owym powieleniu, dostajemy $y$ wywołań – w sumie $x\times y.$

Poprzednik

Poprzednikiem liczby $K$ nazywamy taką liczbę $L,$ że następnikiem liczby $L$ jest $K$ (liczba $0$ nie ma poprzednika, przez co jest ona poprzednikiem siebie samej). W zapisie matematycznym:

$P(K)=L\iff S(L)=K,$

$P(0)=0.$

W rachunku lambda stworzenie takiej funkcji nie jest tak łatwe jak stworzenie funkcji następnika $S.$ Do tego posługujemy się strukturami danych opisanymi w artykule rachunek lambda.

Tworzymy funkcję $\Psi ,$ która z pary $(a,b)$ tworzy parę $(a+1,a){:}$

$\Psi \equiv \lambda pz.z(S(pT))(pT).$

Funkcja poprzednika $P$ liczby $K$ jest zdefiniowana jako $K$-krotna aplikacja funkcji $\Psi$ do pary $\lambda z.z00,$ a potem pobranie drugiego jej elementu:

$P\equiv \lambda n.(n\Psi (\lambda z.z00))F.$

Odejmowanie

Odejmowanie, podobnie jak w przypadku dodawania, jest zdefiniowane jako wielokrotna aplikacja funkcji poprzednika (w tym wypadku pamiętając o przemienności – odejmowanie przemienne nie jest):

$\ominus \equiv \lambda xy.yPx.$

Potęgowanie

Aby policzyć potęgę $x^{y}$ należy wykorzystać to, że $y$ jest naturalne. Wiadomo, że:

$x^{y}=\underbrace {x*x*x*\ldots *x} _{y{\text{-razy}}}.$

Tak więc na przykład $x^{3}$ w rachunku lambda będzie zapisane jako:

$\otimes (\otimes (x)x)x.$

Widzimy, że jest to parokrotna aplikacja funkcji $\otimes$ – można by posłużyć się podobnym algorytmem jak przy dodawaniu lub odejmowaniu, gdyby nie to, że $\otimes$ jest funkcją dwuargumentową. W takim wypadku możemy zdefiniować funkcję $\Xi ,$ która pobiera parę $(a,x)$ i zwraca parę $(a*x,x){:}$

$\Xi \equiv \lambda pz.z(\otimes (pT)(pF))(pF).$

Więc aplikując $y$-krotnie funkcję $\Xi$ do pary $(1,x)$ i zabierając jej pierwszy element otrzymamy $x^{y}{:}$

${\mbox{pow}}\equiv \lambda xy.(y\Xi (\lambda z.z1x))T.$