Rachunek lambda

Rachunek lambda – 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  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ście stał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 zwanej curryingiem, 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

Wyrażenia lambda 
Niech  będzie nieskończonym, przeliczalnym zbiorem zmiennych. Wyrażenie lambda definiuje się następująco:
 Jeżeli  to  jest wyrażeniem lambda,
 Jeżeli  jest wyrażeniem lambda i  to napis  jest wyrażeniem lambda,
 Jeżeli  oraz  są wyrażeniami lambda, to napis  jest wyrażeniem lambda,
 Wszystkie wyrażenia lambda można utworzyć korzystając z powyższych reguł.

Zbiór wszystkich wyrażeń lambda oznacza się 

Wyrażenia lambda rozpatruje się najczęściej jako klasy abstrakcji relacji alfa-konwersji.

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

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:
  (prawda) to 
  (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:
  (negacja) to 
  (koniunkcja) to 
  (alternatywa) to 

Rozwiniętą implikację „jeśli  to  w przeciwnym razie ” zapisać można jako  czyli

Przykład 
Obliczmy wartość wyrażenia „prawda i fałsz”, czyli w rachunku lambda
 

czyli „fałsz” zgodnie z oczekiwaniami.

Struktury danych 
Para  złożona z elementów  i  to 
Pierwszy element wyciąga się za pomocą  natomiast drugi przez 

Listy można konstruować następującym sposobem:
 NIL to 
 CONS to PARA wartość i lista

Następująca funkcja zwraca  jeśli argumentem jest NIL, oraz  jeśli to CONS:

Rekurencja w rachunku lambda 
Rachunek lambda z pozoru nie ma żadnego mechanizmu, który umożliwiałby rekurencję – nie można odwoływać się w definicji do samej funkcji. A jednak rekurencję można osiągnąć poprzez operator paradoksalny Y.

Paradoks polega na tym że dla każdego F zachodzi:
 Y F = F (Y F)

Tak więc np. funkcja negacji nie jest możliwa do zaimplementowania w postaci ogólnej, gdyż:
 (Y nie) = nie (Y nie)

Funkcja rekurencyjna musi pobrać siebie samą jako wartość.

Działa to w następujący sposób:
 (Y f) n
 f (Y f) n
 λ f. λ n. ciało_f

gdzie ciało_f może się odwoływać do siebie samej

Np.:
 silnia = Y (λ f. λ n. if_then_else (is_zero n) 1 (mult n (f (pred n))))

Zobacz też 
 arytmetyka w rachunku lambda
 konwersja α
 rachunek kombinatorów
 redukcja β
 S-wyrażenie

Linki zewnętrzne 
 
 
  Lambda calculus , Routledge Encyclopedia of Philosophy, rep.routledge.com [dostęp 2023-05-10].