Rachunek lambda

Z Wikipedii, wolnej encyklopedii
Skocz do: nawigacja, szukaj

Rachunek lambdasystem 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[edytuj | edytuj kod]

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.

Lambda-wyrażenia[edytuj | edytuj kod]

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[edytuj | edytuj kod]

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[edytuj | edytuj kod]

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:

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[edytuj | edytuj kod]

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 oczekiwaniami.

Struktury danych[edytuj | edytuj kod]

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ż[edytuj | edytuj kod]