Rachunek lambda

Z Wikipedii

Masz nowe wiadomości (różnica z poprzednią wersją).

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

[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ć $\lambda\ x\, .\, x + 2$ (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 $(\lambda\, x\, .\, x + 2)\, 3$ . Warto wspomnieć o tym, że funkcja jest łączna lewostronnie względem argumentu, tzn. $f\, x\, y = (f\, x)\, y$ .

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 $\lambda\, a\, .\, a\, 3$ .

Teraz jesteśmy w stanie dokonać klasycznego otrzymania wartości w punkcie albo też lepiej rzecz ujmując, wykonać złożenie funkcji, mianowicie $f \circ a=f(a)$ . Niech $f$ będzie dana jak poprzednio, wtedy: $(\lambda\,f\,.\,f\, 3) (\lambda\,x\,.\,x + 2)$ i dalej $(\lambda\,x\,.\,x + 2)\, 3$ , a więc otrzymujemy po prostu $3 + 2$ .

Jeżeli chcielibyśmy zdefiniować funkcję dwuargumentową, to może być to wykonane za pomocą techniki zwanej kuryfikacją, mianowicie funkcja jednoargumentowa, której wynikiem jest znowu funkcja jednoargumentowa. Rozpatrzmy funkcję $f (x, y) = x - y$ , której zapis w rachunku lambda ma postać $\lambda\, x\, .\, \lambda\, y\, .\, x - y$ . Aby uprościć zapis stosuje się powszechnie konwencję, aby funkcje "curried" zapisywać wg wzoru $\lambda\, x\, y\, .\, x - y$ .

[edytuj] λ-wyrażenia

λ-wyrażenie ma postać:

zmienna
λ-wyrażenie λ-wyrażenie
λ zmienna . λ-wyrażenie

W rachunku lambda pojawia się problem nazewnictwa zmiennych, który można rozwiązać np. wymuszając nazwy postaci indeksowej:

λ-wyrażenie = M_i, gdzie i jest liczbą zmiennych wolnych (M₀ jeśli nie ma zmiennych wolnych)

M_i =

x_j dla j naturalna ∧ 0 ≤ j < i
M_i M_i
λ x_i . M_i+1

[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 $\lambda\;x\;.\;\lambda\;y\;.\;x$ ,
false (fałsz) to $\lambda\;x\;.\;\lambda\;y\;.\;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 (negacja) to $\lambda\;x\;.\;x\;\mbox{false true}$ ,
and (koniunkcja) to $\lambda\;x\;.\;\lambda\;y\;.\;x\;y\;\mbox{false}$ ,
or (alternatywa) to $\lambda\;x\;.\lambda\;y\;.\;x\;\mbox{true}\;y$ .

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

[edytuj] Przykład

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

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