Arytmetyka w rachunku lambda

Szablon:Dopracować 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 zastosować 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,$ stosujemy 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⟺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ę $\mathrm{\Psi },$ która z pary $(a,b)$ tworzy parę $(a+1,a):$

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

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

$P\equiv \lambda n.(n\mathrm{\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=\underset{y\text{-razy}}{\underbrace{x*x*x*\dots *x}}.$

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ę $\mathrm{\Xi },$ która pobiera parę $(a,x)$ i zwraca parę $(a*x,x):$

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

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

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