Lambda-kalkulus
From Wikipedia, the free encyclopedia
A lambda-kalkulus (vagy λ-kalkulus) egy formális rendszer, amit eredetileg matematikai függvények tulajdonságainak (definiálhatóság, rekurzió, egyenlőség) vizsgálatára vezettek be. Az elmélet kidolgozói Alonzo Church és Stephen Cole Kleene voltak az 1930-as években. Church, 1936-ban, a λ-kalkulus segítségével bizonyította, hogy nem létezik algoritmus a híres Entscheidungsproblem (döntési probléma) megoldására. A λ-kalkulus (akárcsak a Turing-gép) lehetővé teszi, hogy pontosan (formálisan) definiáljuk, mit is értünk kiszámítható függvény alatt.
A λ-kalkulust nyugodtan nevezhetjük a legegyszerűbb általános célú programozási nyelvnek. Csak egyfajta értéket ismer: a függvényt (absztrakciót), és csak egyfajta művelet van benne: a függvény alkalmazás (változó-behelyettesítés). Ezen látszólagos egyszerűsége ellenére minden algoritmus, ami Turing-gépen megvalósítható, az megvalósítható tisztán a λ-kalkulusban is. Ez az azonosság a λ-kalkulus és a Turing-gép kifejező ereje (expressive power) között adja egyébként a Church–Turing-tézis alapját.
Míg korábban a λ-kalkulus elsősorban a kiszámíthatóságelmélet (Theory of Computation) miatt volt érdekes, napjainkban ez már kevésbé hangsúlyos, és sokkal inkább a funkcionális programozási nyelvek elméleti és gyakorlati megalapozásában játszott jelentős, mondhatni központi szerepe került előtérbe.
A szócikk tárgya a λ-kalkulus, eredeti, típus nélküli változata. A λ-kalkulus bevezetése óta számos típusos lambda-kalkulus került kifejlesztésre, és valójában ezek a típusos változatok adják a mai funkcionális programozási nyelvek alapját.