Rachunek lambda

Rachunek lambda to 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 i Stephena Cole'a Kleene'ego w 1930 roku.

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ć wg wzoru $\lambda\, x\, y\, .\, x - y$.

lambda-wyrażenia

Niech $X$ będzie nieskończonym, przeliczalnym zbiorem zmiennych. Lambda-wyrażenie (lambda-term) definiuje się następująco:

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

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

Lambda-termy 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:

• true (prawda) to $\lambda\;x\;.\;\lambda\;y\;.\;x$,
• false (fałsz) to $\lambda\;x\;.\;\lambda\;y\;.\;y$.

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

• not (negacja) to $\lambda\;x\;.\;x\;\mbox{false true}$,
• and (koniunkcja) to $\lambda\;x\;.\;\lambda\;y\;.\;x\;y\;\mbox{false}$,
• or (alternatywa) to $\lambda\;x\;.\lambda\;y\;.\;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\;x\;y\;.\;x\;y\;\mbox{false})\;\mbox{true}\;\mbox{false} =$$\mbox{true false false} = (\lambda\;x\;y\;.\;x)\;\mbox{false false}\;=\;\mbox{false}$,

czyli "fałsz" zgodnie z naszymi oczekiwaniami.

Struktury danych

Para złożona z Y i Z to λ x . x Y Z Pierwszy element wyciąga się za pomocą PARA PRAWDA, drugi przez PARA FAŁSZ.

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

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

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

Zobacz też

• konwersja α
• redukcja β
• arytmetyka w rachunku lambda
• Rachunek kombinatorów