Rachunek lambda

Z Wikipedii

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 Stephen Cole Kleene 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. Rachunek lambda z typami jest podstawą funkcyjnych języków programowania.

[edytuj] 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 wartości 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 albo 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$ .

[edytuj] 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 $λ x . M$ jest lambda-wyrażeniem,
Jeżeli $M$ oraz $N$ są lambda wyrażeniami, to napis $(N M)$ 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-termy rozpatruje się najczęściej jako klasy abstrakcji relacji alfa-konwersji.

[edytuj] Zmienne wolne

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

$F V (x) = {x}$
$FV(MN) = FV(M) \cup FV(N)$
$FV(\lambda x . M) = FV(M) \backslash \{x\}$

[edytuj] 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$ .

[edytuj] 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}$ ,