U matematičkoj logici i računarstvu, lambda račun, odnosno λ-račun, je formalni sustav dizajniran za ispitivanje definicije funkcije, aplikaciju funkcije, te rekurziju. Uveli su ga Alonzo Church i Stephen Cole Kleene 1930-ih; Church je koristio lambda račun 1936. za davanje negativnog odgovora na Entscheidungsproblem. Lambda račun se može koristiti za precizno definiranje izračunljive funkcije. Pitanje jesu li dva lambda izraza istovjetna ne može biti riješeno općenitim algoritmom. Ovo je bilo prvo pitanje, čak i prije problema zaustavljanja, za kojeg je mogla biti dokazana neodlučivost. Lambda račun je jako utjecao na funkcijske programske jezike, kao što su Lisp, ML i Haskell.
Lambda račun se slobodno može nazvati najmanjim univerzalnim programskim jezikom. Sastoji se od jednog transformacijskog pravila (supstitucija varijable) i jednog načina definicije funkcije. Lambda račun je univerzalan na način da bilo koja izračunljiva funkcija može biti izražena i evaluirana koristeći njegov formalizam. Ovo je stoga istovjetno formalizmu Turingovog stroja. Međutim, lambda račun naglašava transformacijska pravila i ne zamara se stvarnim strojem koji ih ostvaruje. U tom duhu, predstavlja pristup srodniji programskoj podršci nego sklopovlju.
Ovaj se članak bavi "netipiziranim lambda računom", kako ga je izvorno osmislio Church. U međuvremenu su se razvili tipizirani lambda računi.
Povijest Izvorno, Church je pokušao konstruirati potpun formalni sustav kao osnovu matematike - kad se ispostavila podložnost sustava analogonu Russellovog paradoksa, odvojio je lambda račun i koristio ga za proučavanje izračunljivosti, što je pak kulminiralo u davanju negativnog odgovora na Entscheidungsproblem.
Neformalni opis U lambda računu, svaki izraz stoji za funkciju jednog argumenta (argument - ulaz funkcije) - argument je funkcije također funkcija jednog argumenta, a vrijednost je funkcije druga funkcija jednog argumenta. Funkcija je anonimno definirana lambda izrazom koji izražuje djelovanje funkcije na njene argumente. Primjerice, "dodaj-dva" funkcija f takva da f(x) = x + 2 bi mogla u lambda računu biti izražena kao λ x. x + 2 (ili ekvivalentno kao λ y. y + 2; ime formalnog argumenta ne igra ulogu) a broj f(3) bi bio zapisan kao (λ x. x + 2) 3. Aplikacija funkcije je asocijativna ulijevo: f x y = (f x) y. Neka se razmotri funkcija koja prima funkciju kao argument i aplicira je se na broj 3: λ f. f 3. Ova bi potonja funkcija mogla biti aplicirana na prethodnu "dodaj-dva" funkciju na sljedeći način: (λ f. f 3) (λ x. x + 2). Ova tri izraza : (λ f. f 3)(λ x. x + 2) i (λ x. x + 2) 3 i 3 + 2 su ekvivalentni. Funkcija dvaju varijabli je u lambda računu izražena kao funkcija jednog argumenta koja vraća funkciju jednog argumenta (vidi currying). Primjerice, funkcija f(x, y) = x - y bi bila zapisana kao λ x. λ y. x - y. Uobičajena je konvencija skratiti curried funkcije kao, na primjer, λ x y. x - y.
Ne može svaki lambda izraz biti reduciran na konačnu vrijednost poput onih gore. Na primjer
(λ x. x x) (λ x. x x) ili (λ x. x x x) (λ x. x x x) i pokušajmo vizualizirati što se dogodi kad se aplicira prva funkcija na svoj argument. (λ x. x x) je također poznat kao ω kombinator; ((λ x. x x) (λ x. x x)) je poznat kao Ω, ((λ x. x x x) (λ x. x x x)) kao Ω2, itd.
Iako sam lambda račun ne sadrži simbole za cijele brojeve ili zbrajanje, ovi mogu biti definirani kao kratice unutar računa i aritmetika može biti izražena kao što će dolje biti pokazano.
Izrazi lambda računa mogu sadržavati slobodne varijable, tj. varijable koje ne veže nijedna λ. Na primjer, varijabla y je slobodna u izrazu (λ x. y) , koji predstavlja funkciju koja uvijek daje rezultat y . Povremeno, ovo stvara potrebu za preimenovanjem formalnih argumenata, na primjer kako bi se reducirao (λ x y. y x) (λ x. y) na λ z. z (λ x. y)
Ako se pojam aplikacije funkcije formalizira pri čemu se ne dozvole lambda izrazi, dobije se kombinatorna logika.
Formalna definicija
Formalno, započinje se s prebrojivo beskonačnim skupom identifikatora, npr. {a, b, c, ..., x, y, z, x1, x2, ...}. Skup svih lambda izraza može biti opisan sljedećom kontekstno neovisnom gramatikom u BNF:
<izraz> ::= <identifikator> <izraz> ::= (λ <identifikator>. <izraz>) <izraz> ::= (<izraz> <izraz>)
Prva dva pravila generiraju funkcije, dok treće opisuje aplikaciju funkcije na argument. Obično su zagrade za lambda apstrakciju (pravilo 2) i aplikaciju funkcije (pravilo 3) izostavljene ako ne postoji nejednoznačnost pod pretpostavkom da je (1) lambda aplikacija asocijativna ulijevo i (2) lambda veže cijeli izraz koji slijedi. Na primjer, izraz ((λ x. (x x)) (λ y. y)) se može jednostavno napisati kao (λ x. x x) λ y. y.
Lambda izrazi kao što je λ x. (x y) ne definiraju funkcije jer je pojavljivanje varijable y slobodno, tj. nije vezano nijednom λ u izrazu. Vezanje pojavljivanja varijabli je (matematičkom indukcijom nad strukturom lambda izraza) definirano sljedećim pravilima:
U izrazu oblika V, gdje je V varijabla, ovo V je jedino slobodno pojavljivanje. U izrazu oblika λ V. E, slobodna pojavljivanja su ona u E osim onih od V. U ovom se slučaju za pojavljivanja V u E kaže da su vezana sa λ prije V. U izrazu oblika (E E′), slobodna pojavljivanja su slobodna pojavljivanja u E i E′.
Nad skupom lambda izraza je definirana relacija ekvivalencije (ovdje označena kao ==) koja obuhvaća intuitivan koncept da izrazi označuju istu funkciju. Ova relacija ekvivalencije je definirana pravilom α-konverzije i pravilom β-redukcije. Ponekad se definira alternativna relacija ekvivalencije, dobivena prihvaćanjem trećeg pravila zvanog η-konverzija.
α-konverzija
Pravilo alfa-konverzije je namijenjeno izražavanju ideje da su imena vezanih varijabli nevažna - a primjer da su λx.x i λy.y iste funkcije. Međutim, pravilo nije jednostavno kao što se na prvi pogled čini (vidi lambda uzdizanje) za praktičnu implementaciju). Postoji nekoliko ograničenja na to kad vezana varijabla može biti zamijenjena drugom. Primjerice, ako se zamijeni x s y u λx.λy.x, dobije se λy.λy.y, što nije u potpunosti isto.
Pravilo alfa-konverzije iskazuje da ako su V i W varijable, E je lambda izraz i
E[V := W]
znači izraz E sa svakim slobodnim pojavljivanjem V u E zamijenjenim sa W, i tada λ V. E == λ W. E[V := W] ako se W ne pojavljuje slobodno untar E i W nije vezan sa λ unutar E kadgod zamjenjuje V. Ovo pravilo na primjer govori da λ x. (λ x. x) x je isto kao i λ y. (λ x. x) y.
Kao primjer uočavamo da je
for (int i = 0; i < max; i++) { proc(i); }
istovjetno
for (int j = 0; j < max; j++) { proc(j); }
β-redukcija
Pravilo beta-redukcije izražava ideju aplikacije funkcije.
Kaže da vrijedi ((λ V. E) E′) == E[V := E′] ako sva slobodna pojavljivanja u E′ ostaju slobodna u E[V := E′].
Relacija == je tad definirana kao najmanja relacija ekvivalencije koja zadovoljava ova dva pravila.
Više operacijska definicija relacija ekvivalencije može biti dana apliciranjem pravila samo slijeva na desno. Izraz oblika ((λ V. E) E′) se zove beta redeks. Lambda izraz koji ne dopušta nijednu beta redukciju, tj. nema beta redeksa kao podizraza, se zove normalni oblik. Nije svaki lambda izraz ekvivalentan normalnom obliku, ali ako jest, taj je normalan oblik jedinstven do na imenovanje vezanih varijabli. Nadalje, postoji algoritam za računanje normalnih oblika: zamjenjuj prvu (krajnje lijevu) varijablu odgovarajućim stvarnim argumentom, sve dok daljnja redukcija nije moguća. Ovaj algoritam zaustavlja ako i samo ako lambda izraz posjeduje normalni oblik. Church-Rosserov teorem tada kaže da dva izraza rezultiraju u istom normalnom obliku do na preimenovanje vezanih varijabli ako i samo ako su ekvivalnetni.
η-konverzija
Postoji i treće pravilo, eta-konverzija, koje može biti dodano ovim dvama kako bi se oformila nova relacija ekvivalencije. Eta-konverzija izražuje ideju ekstenzionalnosti (opsegovnosti), koja je u ovom konstekstu ta da su dvije funkcije jednake ako i samo ako daju isti rezultat za sve argumente. Eta-konverzija pretvara između λ x. f x i f kadgod se x ne pojavljuje slobodno u f. Ovo se može shvatiti kao istovjetno ekstenzionalnosti kako slijedi:
Ako su f i g ekstenzionalno ekvivalentne, tj. ako f a==g a za sve lambda izraze a, tada posebice uzimanjem a kao varijable a koja se ne pojavljuje slobodna u f i g imamo f x == g x te stoga λ x. f x == λ x. g x, te stoga eta-konverzijom slijedi f == g. Stoga ako uzmemo eta-konverziju kao validnu, iznalazimo da je ekstenzionalnost također validna.
Vrijedi i obratno, ako je ekstenzionalnost uzeta kao validna, tada s obzirom na to da beta redukcijom slijedi da za sve y imamo (λ x. f x) y == f y, imamo λ x. f x == f; tj. eta-converzija je validna.
Aritmetika u lambda računu
Nekoliko je mogućih načina za definirati prirodne brojeve u lambda računu, ali daleko najuobičajeniji su Churchovi numerali, koji mogu biti definirani na sljedeći način: 0 := λ f x. x 1 := λ f x. f x 2 := λ f x. f (f x) 3 := λ f x. f (f (f x)) i tako dalje. Intuitivno, broj n u lambda računu je funkcija koja prima funkciju f kao argument i vraća n-tu kompoziciju od f. Drugim riječima, Churchov je numeral funkcija višeg reda - prihvaća jednoargumentnu funkciju f i vraća drugu jednoargumentnu funkciju.
(Valja uočiti da se u izvornom Churchovom lambda računu zahtijevalo bar jedno pojavljivanje formalnog parametra lambda izraza u tijelu funkcije, što gornju definiciju broja 0 čini nemogućom.)
Za ovu definiciju Churchovih numerala, može se definirati funkcija sljedbenika, koja uzima broj n i vraća n + 1: SLJED := λ n f x. f ((n f) x) Zbrajanje je definirano na sljedeći način: PLUS := λ m n f x. n f (m f x) PLUS se može shvatiti kao funkcija koja uzima dva prirodna broja kao argumente i vraća prirodni broj. Zabavno je provjeriti da su PLUS 2 3 i 5 ekvivalentni lambda izrazi. Množenje može biti definirano kao: MNOŽ := λ m n. m (PLUS n) 0, ideja množenja m i n je ista kao i m puta dodavanja n nuli. Alternativno, MNOŽ := λ m n f. m (n f) Prethodnik PRED n = n - 1 pozitivnog cijelog broja n je nešto teži: PRED := λ n f x. n (λ g h. h (g f)) (λ u. x) (λ u. u) i alternativno: PRED := λ n. n (λ g k. (g 1) (λ u. PLUS (g k) 1) k) (λ v. 0) 0 Valja uočiti trik (g 1) (λ u. PLUS (g k) 1) k koji evaluira u k ako je g(1) nula i u g(k) + 1 inače.
Logika i predikati
Po konvenciji, sljedeće su dvije definicije (poznate kao Churchovi booleani) korištene za bulovske vrijednosti ISTINA i LAŽ: ISTINA := λ x y. x LAŽ := λ x y. y (Uočimo da je LAŽ ekvivalentan Churchovom numeralu nula definiranog gore) Tada, s ovim dvama λ-terminima, možemo definirati neke logičke operatore (ovo su samo moguće formulacije; drugi izrazi su jednako ispravni): I := λ p q. p q LAŽ ILI := λ p q. p ISTINA q NE := λ p. p LAŽ ISTINA AKOTADAINAČE := λ p x y. p x y Sada se mogu izračunati neke logičke funkcije, poput na primjer:
I ISTINA LAŽ ≡ (λ p q. p q LAŽ) ISTINA LAŽ →β ISTINA LAŽ LAŽ ≡ (λ x y. x) LAŽ LAŽ →β FALSE sad se lako vidi je da je I ISTINA LAŽ ekvivalentan LAŽ.
Predikat je funkcija koja vraća bulovsku vrijednost. Najfundamentalniji predikat je JELINULA koji vraća ISTINA ako je njegov argument Churchov numeral 0, i LAŽ ako je njegov argument neki drugi Churchov numeral: JELINULA := λ n. n (λ x. LAŽ) ISTINA Dostupnost predikate i gornje definicije vrijednosti ISTINA i LAŽ čine zgodnim napisati "ako-tada-inače" naredbe u lambda računu.
Parovi Par (dvojka) kao tip podataka može biti definiran u terminima vrijednosti ISTINA i LAŽ. CONS := λf.λs. λb. b f s CAR := λp. p ISTINA CDR := λp. p LAŽ NIL := λx.ISTINA NULL := λp. p (λx y.LAŽ)
Vezana lista kao tip podataka može biti definirana ili kao NIL za praznu listu, ili kao CONS elementa i manje liste.
Rekurzija