Rachunek lambda –system formalny używany do badania zagadnień związanych z podstawamimatematyki jakrekurencja, definiowalność funkcji, obliczalność, podstawy matematyki np.definicjaliczb naturalnych, wartości logicznych itd. Rachunek lambda został wprowadzony przezAlonzo Churcha w 1930 roku. Jest uniwersalną reprezentacją obliczeń i równoznacznymaszynie 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óźniejhipotezą Churcha-Turinga.
Rachunek lambda jest przydatny do badaniaalgorytmów. Wszystkie algorytmy, które dadzą się zapisać w rachunku lambda, dadzą się zaimplementować namaszynie Turinga i odwrotnie.
Istnieje wiele rodzajów rachunku lambda, z czego najprostszym jestrachunek lambda bez typów, stanowiący pierwotną inspirację dla powstaniaprogramowania funkcyjnego (Lisp).Rachunek lambda z typami jest podstawą dzisiejszychsystemów typów wjęzykach programowania.
W rachunku lambda każde wyrażenie określafunkcję 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 zwracająca argument powiększony o dwa, którą można by matematycznie zdefiniować jako w rachunku lambda ma postać (nazwa parametru formalnego jest dowolna, więc można zastąpić inną zmienną). Z kolei wartość funkcji w punkcie, np. 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 zadanej wartości – nazwijmy ją Funkcja jest oczywiściestała, choć nic nie stoi na przeszkodzie, aby była to dowolna inna funkcja. W rachunku lambda jest dane wzorem
Teraz jesteśmy w stanie dokonać klasycznego otrzymania wartości w punkcie lub też lepiej rzecz ujmując, wykonaćzłożenie funkcji, mianowicie Niech będzie dana jak poprzednio, wtedy: i dalej a więc otrzymujemy po prostu
Funkcję dwuargumentową można zdefiniować za pomocą techniki zwanejcurryingiem, mianowicie jako funkcję jednoargumentową, której wynikiem jest znowu funkcja jednoargumentowa. Rozpatrzmy funkcję której zapis w rachunku lambda ma postać Aby uprościć zapis stosuje się powszechnie konwencję, aby funkcje „curried” zapisywać według wzoru
Niech będzie nieskończonym,przeliczalnym zbiorem zmiennych. Wyrażenie lambda definiuje się następująco:
Zbiór wszystkich wyrażeń lambda oznacza się
Wyrażenia lambda rozpatruje się najczęściej jakoklasy abstrakcji relacjialfa-konwersji.
Zbiór zmiennych wolnych definiuje się następująco:
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, żewartoś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:
Teraz chcąc ukonstytuować operacje logiczne stosuje się nasze ustalone wartości tak, by wyniki tych operacji były zgodne z naszymi oczekiwaniami, mamy:
Rozwiniętąimplikację „jeśli to w przeciwnym razie” zapisać można jako czyli
Obliczmy wartość wyrażenia „prawda i fałsz”, czyli w rachunku lambda
czyli „fałsz” zgodnie z oczekiwaniami.
Para złożona z elementów i toPierwszy element wyciąga się za pomocą natomiast drugi przez
Listy można konstruować następującym sposobem:
Następująca funkcja zwraca jeśli argumentem jest NIL, oraz jeśli to CONS:
Rachunek lambda z pozoru nie ma żadnego mechanizmu, który umożliwiałbyrekurencję – nie można odwoływać się w definicji do samej funkcji. A jednak rekurencję można osiągnąć poprzezoperator paradoksalny Y.
Paradoks polega na tym że dlakażdego F zachodzi:
Tak więc np. funkcja negacji nie jest możliwa do zaimplementowania w postaci ogólnej, gdyż:
Funkcja rekurencyjna musi pobrać siebie samą jako wartość.
Działa to w następujący sposób:
gdzie ciało_f może się odwoływać do siebie samej
Np.:
Lambda calculus(ang.),Routledge Encyclopedia of Philosophy, rep.routledge.com [dostęp 2023-05-10].