Rachunek lambda

Szablon:Dopracować 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. $fxy=(fx)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.a3.$

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.f3)(\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 xy.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ę $\mathrm{\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:

• $\text{true}$ (prawda) to $\lambda xy.x,$
• $\text{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:

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

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

Przykład

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

$\text{and true false}=(\lambda xy.xy\text{false})\text{true false}=\text{true false false}=(\lambda xy.x)\text{false false}=\text{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\text{true},$ natomiast drugi przez $p\text{false}.$

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

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

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

• Szablon:SEP
• Szablon:IEP
• Szablon:Paywall Lambda calculus Szablon:Lang, Routledge Encyclopedia of Philosophy, rep.routledge.com [dostęp 2023-05-10].