Rachunek lambda

Ten artykuł od 2021-03 zawiera treści, przy których brakuje odnośników do źródeł.

Należy dodać przypisy do treści niemających odnośników do źródeł. Dodanie listy źródeł bibliograficznych jest problematyczne, ponieważ nie wiadomo, które treści one uźródławiają.
Sprawdź w źródłach: Google Books • Google Scholar • BazHum • BazTech • RCIN • Internet Archive (texts / inlibrary)
Dokładniejsze informacje o tym, co należy poprawić, być może znajdują się w dyskusji tego artykułu.
Po wyeliminowaniu niedoskonałości należy usunąć szablon {{Dopracować}} z tego artykułu.

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 w 1930 roku. Jest uniwersalną reprezentacją obliczeń i równoznaczny maszynie 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óźniej hipotezą Churcha-Turinga.

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.

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 {\displaystyle f} zwracająca argument powiększony o dwa, którą można by matematycznie zdefiniować jako f ( x ) = x + 2 , {\displaystyle f(x)=x+2,} w rachunku lambda ma postać λ   x . x + 2 {\displaystyle \lambda \ x\,.\,x+2} (nazwa parametru formalnego jest dowolna, więc x {\displaystyle x} można zastąpić inną zmienną). Z kolei wartość funkcji w punkcie, np. f ( 3 ) {\displaystyle f(3)} ma zapis ( λ x . x + 2 ) 3. {\displaystyle (\lambda \,x\,.\,x+2)\,3.} Warto wspomnieć o tym, że funkcja jest łączna lewostronnie względem argumentu, tzn. f x y = ( f x ) y . {\displaystyle f\,x\,y=(f\,x)\,y.}

Ponieważ wszystko jest funkcją jednoargumentową, możemy zdefiniować zmienną o zadanej wartości – nazwijmy ją a . {\displaystyle a.} Funkcja a {\displaystyle a} jest oczywiście stała, choć nic nie stoi na przeszkodzie, aby była to dowolna inna funkcja. W rachunku lambda a {\displaystyle a} jest dane wzorem λ a . a 3. {\displaystyle \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 ∘ a = f ( a ) . {\displaystyle f\circ a=f(a).} Niech f {\displaystyle f} będzie dana jak poprzednio, wtedy: ( λ f . f 3 ) ( λ x . x + 2 ) {\displaystyle (\lambda \,f\,.\,f\,3)(\lambda \,x\,.\,x+2)} i dalej ( λ x . x + 2 ) 3 , {\displaystyle (\lambda \,x\,.\,x+2)\,3,} a więc otrzymujemy po prostu 3 + 2. {\displaystyle 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 , {\displaystyle f(x,y)=x-y,} której zapis w rachunku lambda ma postać λ x . λ y . x − y . {\displaystyle \lambda \,x\,.\,\lambda \,y\,.\,x-y.} Aby uprościć zapis stosuje się powszechnie konwencję, aby funkcje „curried” zapisywać według wzoru λ x y . x − y . {\displaystyle \lambda \,x\,y\,.\,x-y.}

Niech X {\displaystyle X} będzie nieskończonym, przeliczalnym zbiorem zmiennych. Wyrażenie lambda definiuje się następująco:

• Jeżeli x ∈ X {\displaystyle x\in X} to x {\displaystyle x} jest wyrażeniem lambda,
• Jeżeli M {\displaystyle M} jest wyrażeniem lambda i x ∈ X , {\displaystyle x\in X,} to napis λ x . M {\displaystyle \lambda x.M} jest wyrażeniem lambda,
• Jeżeli M {\displaystyle M} oraz N {\displaystyle N} są wyrażeniami lambda, to napis ( N M ) {\displaystyle (NM)} 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ę Λ . {\displaystyle \Lambda .}

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

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

• F V ( x ) = { x } {\displaystyle FV(x)=\{x\}}
• F V ( M N ) = F V ( M ) ∪ F V ( N ) {\displaystyle FV(MN)=FV(M)\cup FV(N)}
• F V ( λ x . M ) = F V ( M ) − { x } {\displaystyle FV(\lambda x.M)=FV(M)-\{x\}}

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 {\displaystyle {\mbox{true}}} (prawda) to λ x y . x , {\displaystyle \lambda xy.x,}
• false {\displaystyle {\mbox{false}}} (fałsz) to λ x y . y . {\displaystyle \lambda xy.y.}

Teraz chcąc ukonstytuować operacje logiczne stosuje się nasze ustalone wartości tak, by wyniki tych operacji były zgodne z naszymi oczekiwaniami, mamy:

• not {\displaystyle {\mbox{not}}} (negacja) to λ x . x false true , {\displaystyle \lambda x.x\;{\mbox{false true}},}
• and {\displaystyle {\mbox{and}}} (koniunkcja) to λ x y . x y false , {\displaystyle \lambda xy.xy\;{\mbox{false}},}
• or {\displaystyle {\mbox{or}}} (alternatywa) to λ x y . x true y . {\displaystyle \lambda xy.x\;{\mbox{true}}\;y.}

Rozwiniętą implikację „jeśli A , {\displaystyle A,} to B , {\displaystyle B,} w przeciwnym razie C {\displaystyle C} ” zapisać można jako A B C , {\displaystyle A\;B\;C,} czyli ( A B ) C . {\displaystyle (A\;B)\;C.}

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

and true false = ( λ x y . x y false ) true false = true false false = ( λ x y . x ) false false = false , {\displaystyle {\mbox{and true false}}=(\lambda xy.xy\;{\mbox{false}})\;{\mbox{true false}}={\mbox{true false false}}=(\lambda xy.x)\;{\mbox{false false}}={\mbox{false}},}

czyli „fałsz” zgodnie z oczekiwaniami.

Para p {\displaystyle p} złożona z elementów x {\displaystyle x} i y {\displaystyle y} to λ z . z x y {\displaystyle \lambda z.zxy} Pierwszy element wyciąga się za pomocą p true , {\displaystyle p\;{\mbox{true}},} natomiast drugi przez p false . {\displaystyle p\;{\mbox{false}}.}

Listy można konstruować następującym sposobem:

• NIL to λ x . true {\displaystyle \lambda x.{\mbox{true}}}
• CONS to PARA wartość i lista

Następująca funkcja zwraca true , {\displaystyle {\mbox{true}},} jeśli argumentem jest NIL, oraz false , {\displaystyle {\mbox{false}},} jeśli to CONS: λ x . x ( λ a b . false ) {\displaystyle \lambda x.x(\lambda ab.{\mbox{false}})}

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))))

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

• JesseJ. Alama JesseJ., The Lambda Calculus, [w:] Stanford Encyclopedia of Philosophy, CSLI, Stanford University, 21 marca 2018, ISSN 1095-5054 [dostęp 2018-08-07]  (ang.). (Rachunek lambda)
• ShaneS. Steinert-Threlkeld ShaneS., Lambda Calculi, Internet Encyclopedia of Philosophy, ISSN 2161-0002 [dostęp 2018-06-27]  (ang.).
• Lambda calculus (ang.), Routledge Encyclopedia of Philosophy, rep.routledge.com [dostęp 2023-05-10].