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

Ponieważ wszystko jest funkcją jednoargumentową, możemy zdefiniować zmienną o zadanej wartości – nazwijmy ją ${\displaystyle a.}$ Funkcja ${\displaystyle a}$ jest oczywiście stała, choć nic nie stoi na przeszkodzie, aby była to dowolna inna funkcja. W rachunku lambda ${\displaystyle a}$ jest dane wzorem ${\displaystyle \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 ${\displaystyle f\circ a=f(a).}$ Niech ${\displaystyle f}$ będzie dana jak poprzednio, wtedy: ${\displaystyle (\lambda \,f\,.\,f\,3)(\lambda \,x\,.\,x+2)}$ i dalej ${\displaystyle (\lambda \,x\,.\,x+2)\,3,}$ a więc otrzymujemy po prostu ${\displaystyle 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ę ${\displaystyle f(x,y)=x-y,}$ której zapis w rachunku lambda ma postać ${\displaystyle \lambda \,x\,.\,\lambda \,y\,.\,x-y.}$ Aby uprościć zapis stosuje się powszechnie konwencję, aby funkcje „curried” zapisywać według wzoru ${\displaystyle \lambda \,x\,y\,.\,x-y.}$

Wyrażenia lambda

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

• Jeżeli ${\displaystyle x\in X}$ to ${\displaystyle x}$ jest wyrażeniem lambda,
• Jeżeli ${\displaystyle M}$ jest wyrażeniem lambda i ${\displaystyle x\in X,}$ to napis ${\displaystyle \lambda x.M}$ jest wyrażeniem lambda,
• Jeżeli ${\displaystyle M}$ oraz ${\displaystyle N}$ są wyrażeniami lambda, to napis ${\displaystyle (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ę ${\displaystyle \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:

• ${\displaystyle FV(x)=\{x\}}$
• ${\displaystyle FV(MN)=FV(M)\cup FV(N)}$
• ${\displaystyle 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:

• ${\displaystyle {\mbox{true}}}$ (prawda) to ${\displaystyle \lambda xy.x,}$
• ${\displaystyle {\mbox{false}}}$ (fałsz) to ${\displaystyle \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:

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

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

Przykład

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

${\displaystyle {\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 ${\displaystyle p}$ złożona z elementów ${\displaystyle x}$ i ${\displaystyle y}$ to ${\displaystyle \lambda z.zxy}$ Pierwszy element wyciąga się za pomocą ${\displaystyle p\;{\mbox{true}},}$ natomiast drugi przez ${\displaystyle p\;{\mbox{false}}.}$

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

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

Następująca funkcja zwraca ${\displaystyle {\mbox{true}},}$ jeśli argumentem jest NIL, oraz ${\displaystyle {\mbox{false}},}$ jeśli to CONS: ${\displaystyle \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].

Kontrola autorytatywna (modelowanie matematyczne):

• LCCN: sh85074174
• GND: 4166495-4
• BnF: 119586908
• SUDOC: 027576345
• J9U: 987007553113905171
• LNB: 000131277

Encyklopedie internetowe:

• Britannica: topic/lambda-calculus
• SEP: lambda-calculus
• DSDE: lambdakalkyle