Calculul lambda ( λ-calcul ) este un sistem formal dezvoltat de matematicianul american Alonzo Church pentru a formaliza și analiza conceptul de computabilitate .
λ-calcul pur , ai cărui termeni , numiți și obiecte („ambele”), sau termeni λ , sunt construiți exclusiv din variabile folosind aplicație și abstractizare. Inițial, prezența oricăror constante nu este de așteptat.
Calculul λ se bazează pe două operații fundamentale:
Forma de bază a echivalenței definită în termeni lambda este echivalența alfa. De exemplu, și : sunt termeni lambda alfa echivalenti și ambii reprezintă aceeași funcție (funcția de identitate). Termenii și nu sunt echivalenti alfa, deoarece nu sunt într-o abstractizare lambda.
Deoarece expresia denotă o funcție care atribuie o valoare fiecărui , atunci pentru a evalua expresia
care include atat aplicarea cat si abstractizarea , este necesar sa se efectueze inlocuirea numarului 3 in termen in locul variabilei . Rezultatul este . Această idee poate fi scrisă în formă generală ca
și se numește β-reducere . O expresie a formei , adică aplicarea unei abstracții la un anumit termen, se numește redex . Deși β-reducerea este în esență singura axiomă „esențială” a calculului λ, ea conduce la o teorie foarte bogată și complexă. Împreună cu acesta, λ-calcul are proprietatea de completitudine Turing și, prin urmare, este cel mai simplu limbaj de programare .
-conversia exprimă ideea că două funcții sunt identice dacă și numai dacă, aplicate oricărui argument, produc aceleași rezultate. -transformarea traduce formule și unele în altele (doar dacă nu are apariții libere în : altfel, variabila liberă după transformare va deveni o abstractizare externă legată, sau invers).
O funcție a două variabile și poate fi considerată ca o funcție a unei variabile , returnând o funcție a unei variabile , adică ca o expresie . Această tehnică funcționează exact la fel pentru funcții de orice aritate . Aceasta arată că funcțiile multor variabile pot fi exprimate în λ-calcul și sunt „ zahăr sintactic ”. Procesul descris de transformare a funcțiilor mai multor variabile într-o funcție a unei variabile se numește curry (și: currying ), după matematicianul american Haskell Curry , deși a fost propus pentru prima dată de Moses Sheinfinkel ( 1924 ).
Faptul că termenii calculului λ acţionează ca funcţii aplicate termenilor calculului λ (adică, poate pentru ei înşişi) duce la dificultăţi în construirea unei semantici adecvate a calculului λ. Pentru a da λ-calculului orice semnificație, este necesar să se obțină o mulțime în care spațiul său de funcții ar fi încorporat . În cazul general, aceasta nu există din motive de restricții asupra cardinalităților acestor două mulțimi și funcționează de la la : a doua are o cardinalitate mai mare decât prima.
Dana Scott a depășit această dificultate la începutul anilor 1970 prin construirea conceptului de regiune (inițial pe rețele complete [1] , generalizându-l ulterior la o mulțime completă parțial ordonată cu o topologie specială ) și reducându -l la funcții continue în această topologie [1] 2] . Pe baza acestor construcții s-a creat semantica denotațională a limbajelor de programare , în special datorită faptului că cu ajutorul acestora se poate da un sens exact la două constructe importante ale limbajului de programare, cum ar fi ca recursivitate și tipuri de date .
Recursiunea este definirea unei funcții în termenii ei înșiși; la prima vedere, calculul lambda nu permite acest lucru, dar această impresie este înșelătoare. De exemplu, luați în considerare o funcție recursivă care calculează factorialul :
f(n) = 1, dacă n = 0; altfel n × f(n - 1).În calculul lambda, o funcție nu se poate referi direct la ea însăși. Cu toate acestea, unei funcții i se poate transmite un parametru asociat acesteia. De regulă, acest argument este pe primul loc. Asociându-l cu o funcție, obținem o funcție nouă, deja recursivă. Pentru a face acest lucru, un argument care se referă la el însuși (notat aici ca ) trebuie să fie transmis corpului funcției.
g := λr. λn.(1, dacă n = 0; altfel n × (rr (n-1))) f := ggAceasta rezolvă problema specifică a calculării factorialului, dar este posibilă și o soluție generală. Având în vedere un termen lambda reprezentând corpul unei funcții recursive sau al unei bucle, trecându-se ca prim argument, combinatorul în virgulă fixă va returna funcția sau bucla recursivă necesară. Funcțiile nu trebuie să treacă în mod explicit de fiecare dată.
Există mai multe definiții ale combinatorilor de punct fix. Cel mai simplu dintre ele:
Y = λg.(λx.g (xx)) (λx.g (xx))În calculul lambda, este un punct fix ; haideți să demonstrăm:
Y g (λh.(λx.h (xx)) (λx.h (xx))) g (λx.g (xx)) (λx.g (xx)) g((λx.g(xx))(λx.g(xx))) g (Yg)Acum, pentru a defini factorial ca o funcție recursivă, putem scrie pur și simplu , unde este numărul pentru care este calculat factorul. Să , obținem:
g (Y g) 4 (λfn.(1, dacă n = 0; și n (f(n-1)), dacă n>0)) (Y g) 4 (λn.(1, dacă n = 0; și n ((Y g) (n-1)), dacă n>0)) 4 1, dacă 4 = 0; și 4 (g(Y g) (4-1)), dacă 4>0 4 (g(Y g) 3) 4 (λn.(1, dacă n = 0; și n ((Y g) (n-1)), dacă n>0) 3) 4 (1, dacă 3 = 0; și 3 (g(Y g) (3-1)), dacă 3>0) 4 (3 (g(Y g) 2)) 4 (3 (λn.(1, dacă n = 0; și n ((Y g) (n-1)), dacă n>0) 2)) 4 (3 (1, dacă 2 = 0; și 2 (g(Y g) (2-1)), dacă 2>0)) 4 (3 (2 (g(Y g) 1))) 4 (3 (2 (λn.(1, dacă n = 0; și n ((Y g) (n-1)), dacă n>0) 1))) 4 (3 (2 (1, dacă 1 = 0; și 1 ((Y g) (1-1)), dacă 1>0))) 4 (3 (2 (1) ((Y g) 0)))) 4 (3 (2 (1)) ((λn.(1, dacă n = 0; și n ((Y g) (n-1)), dacă n>0) 0)))) 4 (3 (2 (1 (1), dacă 0 = 0; și 0 ((Y g) (0-1)), dacă 0>0)))) 4 (3 (2 (1 (1)))) 24Fiecare definiție recursivă poate fi reprezentată ca un punct fix al funcției corespunzătoare, prin urmare folosind , fiecare definiție recursivă poate fi exprimată ca o expresie lambda. În special, putem defini recursiv scăderea, înmulțirea, compararea numerelor naturale.
În limbajele de programare, „λ-calcul” este adesea înțeles ca mecanismul „ funcțiilor anonime ” - funcții de apel invers care pot fi definite chiar în locul în care sunt utilizate și care au acces la variabilele locale ale funcției curente ( închidere ).