Rachunek lambda

Rachunek lambda – system formalny używany do badania zagadnień związanych z podstawami matematyki jak rekurencja, definiowalność funkcji, obliczalność, podstawy matematyki np. definicja liczb naturalnych, wartości logicznych itd. Rachunek lambda został wprowadzony przez Alonzo Churcha w 1930 roku. Jest uniwersalną reprezentacją obliczeń i równoznaczny maszynie Turinga, tzn. dowolne wyrażenie w rachunku lambda można przedstawić jako program na maszynie Turinga i odwrotnie. Został użyty do udowodnienia hipotezy, nazwanej później hipotezą Churcha-Turinga.

Rachunek lambda jest przydatny do badania algorytmów. Wszystkie algorytmy, które dadzą się zapisać w rachunku lambda, dadzą się zaimplementować na maszynie Turinga i odwrotnie.

Istnieje wiele rodzajów rachunku lambda, z czego najprostszym jest rachunek lambda bez typów, stanowiący pierwotną inspirację dla powstania programowania funkcyjnego (Lisp). Rachunek lambda z typami jest podstawą dzisiejszych systemów typów w językach programowania.

Opis nieformalny

W rachunku lambda każde wyrażenie określa funkcję jednoargumentową. Z kolei argumentem tej funkcji jest również funkcja jednoargumentowa, wartością funkcji jest znów funkcja jednoargumentowa. Funkcja jest definiowana anonimowo przez wyrażenie lambda, które opisuje, co funkcja robi ze swoim argumentem.

Funkcja $f$ zwracająca argument powiększony o dwa, którą można by matematycznie zdefiniować jako $f(x)=x+2,$ w rachunku lambda ma postać $\lambda \ x\,.\,x+2$ (nazwa parametru formalnego jest dowolna, więc $x$ można zastąpić inną zmienną). Z kolei wartość funkcji w punkcie, np. $f(3)$ ma zapis $(\lambda \,x\,.\,x+2)\,3.$ Warto wspomnieć o tym, że funkcja jest łączna lewostronnie względem argumentu, tzn. $f\,x\,y=(f\,x)\,y.$

Ponieważ wszystko jest funkcją jednoargumentową, możemy zdefiniować zmienną o zadanej wartości – nazwijmy ją $a.$ Funkcja $a$ jest oczywiście stała, choć nic nie stoi na przeszkodzie, aby była to dowolna inna funkcja. W rachunku lambda $a$ jest dane wzorem $\lambda \,a\,.\,a\,3.$

Teraz jesteśmy w stanie dokonać klasycznego otrzymania wartości w punkcie lub też lepiej rzecz ujmując, wykonać złożenie funkcji, mianowicie $f\circ a=f(a).$ Niech $f$ będzie dana jak poprzednio, wtedy: $(\lambda \,f\,.\,f\,3)(\lambda \,x\,.\,x+2)$ i dalej $(\lambda \,x\,.\,x+2)\,3,$ a więc otrzymujemy po prostu $3+2.$

Funkcję dwuargumentową można zdefiniować za pomocą techniki zwanej curryingiem, mianowicie jako funkcję jednoargumentową, której wynikiem jest znowu funkcja jednoargumentowa. Rozpatrzmy funkcję $f(x,y)=x-y,$ której zapis w rachunku lambda ma postać $\lambda \,x\,.\,\lambda \,y\,.\,x-y.$ Aby uprościć zapis stosuje się powszechnie konwencję, aby funkcje „curried” zapisywać według wzoru $\lambda \,x\,y\,.\,x-y.$

Wyrażenia lambda

Niech $X$ będzie nieskończonym, przeliczalnym zbiorem zmiennych. Wyrażenie lambda definiuje się następująco:

• Jeżeli $x\in X$ to $x$ jest wyrażeniem lambda,
• Jeżeli $M$ jest wyrażeniem lambda i $x\in X,$ to napis $\lambda x.M$ jest wyrażeniem lambda,
• Jeżeli $M$ oraz $N$ są wyrażeniami lambda, to napis $(NM)$ jest wyrażeniem lambda,
• Wszystkie wyrażenia lambda można utworzyć korzystając z powyższych reguł.

Zbiór wszystkich wyrażeń lambda oznacza się $\Lambda .$

Wyrażenia lambda rozpatruje się najczęściej jako klasy abstrakcji relacji alfa-konwersji.

Zmienne wolne

Zbiór zmiennych wolnych definiuje się następująco:

• $FV(x)=\{x\}$
• $FV(MN)=FV(M)\cup FV(N)$
• $FV(\lambda x.M)=FV(M)-\{x\}$

Logika

Użycie wartości liczbowych do oznaczania wartości logicznych może prowadzić do nieścisłości przy operowaniu relacjami na liczbach, dlatego też należy wyraźnie oddzielić logikę od obiektów, na których ona operuje. Z tego powodu oczywistym staje się fakt, że wartości logiczne prawdy i fałszu muszą być elementami skonstruowanymi z wyrażeń tego rachunku.

Wartościami logicznymi nazwiemy funkcje dwuargumentowe, z których jedna zawsze będzie zwracać pierwszy argument, a druga – drugi:

• ${\mbox{true}}$ (prawda) to $\lambda xy.x,$
• ${\mbox{false}}$ (fałsz) to $\lambda xy.y.$

Teraz chcąc ukonstytuować operacje logiczne stosujemy nasze ustalone wartości tak, by wyniki tych operacji były zgodne z naszymi oczekiwaniami, mamy:

• ${\mbox{not}}$ (negacja) to $\lambda x.x\;{\mbox{false true}},$
• ${\mbox{and}}$ (koniunkcja) to $\lambda xy.xy\;{\mbox{false}},$
• ${\mbox{or}}$ (alternatywa) to $\lambda xy.x\;{\mbox{true}}\;y.$

Rozwiniętą implikację „jeśli $A,$ to $B,$ w przeciwnym razie $C$” zapisać można jako $A\;B\;C,$ czyli $(A\;B)\;C.$

Przykład

Obliczmy wartość wyrażenia „prawda i fałsz”, czyli w rachunku lambda

${\mbox{and true false}}=(\lambda xy.xy\;{\mbox{false}})\;{\mbox{true false}}={\mbox{true false false}}=(\lambda xy.x)\;{\mbox{false false}}={\mbox{false}},$

czyli „fałsz” zgodnie z oczekiwaniami.

Struktury danych

Para $p$ złożona z elementów $x$ i $y$ to $\lambda z.zxy$ Pierwszy element wyciąga się za pomocą $p\;{\mbox{true}},$ natomiast drugi przez $p\;{\mbox{false}}.$

Listy można konstruować następującym sposobem:

• NIL to $\lambda x.{\mbox{true}}$
• CONS to PARA wartość i lista

Następująca funkcja zwraca ${\mbox{true}},$ jeśli argumentem jest NIL, oraz ${\mbox{false}},$ jeśli to CONS: $\lambda x.x(\lambda ab.{\mbox{false}})$

Rekurencja w rachunku lambda

Rachunek lambda z pozoru nie ma żadnego mechanizmu, który umożliwiałby rekurencję – nie można odwoływać się w definicji do samej funkcji. A jednak rekurencję można osiągnąć poprzez operator paradoksalny Y.

Paradoks polega na tym że dla każdego F zachodzi:

Y F = F (Y F)

Tak więc np. funkcja negacji nie jest możliwa do zaimplementowania w postaci ogólnej, gdyż:

(Y nie) = nie (Y nie)

Funkcja rekurencyjna musi pobrać siebie samą jako wartość.

Działa to w następujący sposób:

(Y f) n

f (Y f) n

λ f. λ n. ciało_f

gdzie ciało_f może się odwoływać do siebie samej

Np.:

silnia = Y (λ f. λ n. if_then_else (is_zero n) 1 (mult n (f (pred n))))

Zobacz też

• arytmetyka w rachunku lambda
• konwersja α
• rachunek kombinatorów
• redukcja β
• S-wyrażenie

Linki zewnętrzne

• JesseJ. Alama JesseJ., The Lambda Calculus, [w:] Stanford Encyclopedia of Philosophy, CSLI, Stanford University, 21 marca 2018, ISSN 1095-5054 [dostęp 2018-08-07]  (ang.). (Rachunek lambda)
• ShaneS. Steinert-Threlkeld ShaneS., Lambda Calculi, Internet Encyclopedia of Philosophy, ISSN 2161-0002 [dostęp 2018-06-27]  (ang.).
• Lambda calculus (ang.), Routledge Encyclopedia of Philosophy, rep.routledge.com [dostęp 2023-05-10].