ResponseEve, a responsive template by SiGa

Ten artykuł od 2020-12 wymaga zweryfikowania podanych informacji. Należy podać wiarygodne źródła w formie przypisów bibliograficznych. Część lub nawet wszystkie informacje w artykule mogą być nieprawdziwe. Jako pozbawione źródeł mogą zostać zakwestionowane i usunięte. Sprawdź w źródłach: Encyklopedia PWN • Google Books • Google Scholar • Federacja Bibliotek Cyfrowych • BazHum • BazTech • RCIN • Internet Archive (texts / inlibrary) Po wyeliminowaniu niedoskonałości należy usunąć szablon {{Dopracować}} z tego artykułu.

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

Następnik

Funkcja ${\displaystyle S}$ następnika jest zdefiniowana następująco:

${\displaystyle 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 ${\displaystyle K}$ i ${\displaystyle L}$ należy ${\displaystyle K}$-krotnie zaaplikować funkcję następnika do liczby ${\displaystyle L}$ (lub na odwrót, dodawanie jest przemienne):

${\displaystyle \oplus \equiv \lambda xy.xSy.}$

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

Mnożenie

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

${\displaystyle \otimes \equiv \lambda xyz.x(yz).}$

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

Poprzednik

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

${\displaystyle P(K)=L\iff S(L)=K,}$

${\displaystyle P(0)=0.}$

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

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

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

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

${\displaystyle 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):

${\displaystyle \ominus \equiv \lambda xy.yPx.}$

Potęgowanie

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

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

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

${\displaystyle \otimes (\otimes (x)x)x.}$

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

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

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

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