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.
Spis treści |
[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ć (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 . Warto wspomnieć o tym, że funkcja jest łączna lewostronnie względem argumentu, tzn. .
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 .
Teraz jesteśmy w stanie dokonać klasycznego otrzymania wartości w punkcie albo też lepiej rzecz ujmując, wykonać złożenie funkcji, mianowicie . Niech f będzie dana jak poprzednio, wtedy: i dalej , 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ć . Aby uprościć zapis stosuje się powszechnie konwencję, aby funkcje "curried" zapisywać wg wzoru .
[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 to x jest lambda-wyrażeniem,
- Jeżeli M jest lambda wyrażeniem i , to napis λ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-termy rozpatruje się najczęściej jako klasy abstrakcji relacji alfa-konwersji.
[edytuj] Zmienne wolne
Zbiór zmiennych wolnych definiuje się następująco:
- FV(x) = {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 ,
- false (fałsz) to .
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 ,
- and (koniunkcja) to ,
- or (alternatywa) to .
Rozwiniętą implikację "jeśli A, to B, w przeciwnym razie C" zapisać można jako , czyli .
[edytuj] Przykład
Obliczmy wartość wyrażenia "prawda i fałsz", czyli w rachunku lambda
- ,
czyli "fałsz" zgodnie z naszymi oczekiwaniami.
[edytuj] 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
- CONS to PARA wartość i lista
następująca funkcja zwraca true jeśli argumentem jest NIL i false jeśli to CONS: