Rachunek lambda


Rachunek lambda w encyklopedii

Z Wikipedii, wolnej encyklopedii Przejdź do nawigacji Przejdź do wyszukiwania

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.

Spis treści

Opis nieformalny | 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 {\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.}

Wyrażenia lambda | edytuj kod

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.

Zmienne wolne | edytuj kod

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\}}

Logika | 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 {\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 stosujemy 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.}

Przykład | edytuj kod

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.

Struktury danych | edytuj kod

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

Rekurencja w rachunku lambda | edytuj kod

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

Linki zewnętrzne | edytuj kod

Kontrola autorytatywna (system formalny):
Na podstawie artykułu: "Rachunek lambda" pochodzącego z Wikipedii
OryginałEdytujHistoria i autorzy