Rachunek lambda - Polski Serwis Naukowy

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, wartości logicznych, itd. Rachunek lambda został wprowadzony przez Alonzo Churcha i Stephena Cole'a Kleene'ego w 1930 roku.

W językach programowania system typów może być zdefiniowany jako system klasyfikacji wyrażeń w zależności od rodzajów wartości, jakie one generują. Każdej obliczonej wartości przypisywany jest pewien typ, który jednoznacznie definiuje, jakie operacje można na niej wykonać. Śledząc przepływ wartości, system typów stara się udowodnić, że w programie występuje poprawne typowanie, tzn. nie dochodzi do sytuacji, w której na wartości określonego typu próbujemy wykonać niedozwoloną operację.
Definicja intuicyjna: Maszyna Turinga stanowi najprostszy, wyidealizowany matematyczny model komputera, zbudowany z taśmy, na której zapisuje się dane i poruszającej się wzdłuż niej "głowicy", wykonującej proste operacje na zapisanych na taśmie wartościach.

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.

Liczby naturalne – liczby służące podawaniu liczności (trzy osoby, zob. liczebnik główny/kardynalny) i ustalania kolejności (trzecia osoba, zob. liczebnik porządkowy), poddane w matematyce dalszym uogólnieniom (odpowiednio: liczby kardynalne, liczby porządkowe). Badaniem własności liczb naturalnych zajmują się arytmetyka i teoria liczb.
Konwersja α to operacja w rachunku lambda polegająca na zamianie zmiennej określanej przez lambdę oraz wszystkich jej wystąpień w wyrażeniu pod lambdą, na inną, nie kolidującą z żadną z lambd zewnętrznych lub wewnętrzynych.

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

Relacja równoważności – zwrotna, symetryczna i przechodnia relacja dwuargumentowa określona na pewnym zbiorze utożsamiająca ze sobą w pewien sposób jego elementy, co ustanawia podział tego zbioru na rozłączne podzbiory według tej relacji. Podobnie każdy podział zbioru niesie ze sobą informację o pewnej relacji równoważności.
System formalny – w logice i matematyce język formuł (logiki) wraz ze zbiorem reguł wyprowadzania (wywodu) i zwykle zbiorem aksjomatów. Systemy formalne są tworzone i badane zarówno jako samodzielne abstrakcyjne twory, jak i systemy opisu rzeczywistości.

Ponieważ wszystko jest funkcją jednoargumentową, możemy zdefiniować zmienną o 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 lub 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$ .

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

Język programowania – zbiór zasad określających, kiedy ciąg symboli tworzy program (czyli ciąg symboli opisujący obliczenia) oraz jakie obliczenia opisuje.
Programowanie funkcyjne (lub programowanie funkcjonalne) - filozofia programowania będąca odmianą programowania deklaratywnego, w której funkcje należą do wartości podstawowych, a nacisk kładzie się na wartościowanie (często rekurencyjnych) funkcji, a nie na wykonywanie poleceń.

czytaj dalej: [2], [3]

w oparciu o Wikipedię (licencja GFDL, CC-BY-SA 3.0, autorzy, historia, edycja)