Lambda račun

Izvor: Hrvatska internetska enciklopedija
Skoči na:orijentacija, traži

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 sa 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:

  1. <izraz> ::= <identifikator>
  2. <izraz> ::= (λ <identifikator>. <izraz>)
  3. <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:

  1. U izrazu oblika  V,  gdje je V varijabla, ovo V je jedino slobodno pojavljivanje.
  2. 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.
  3. 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 sa 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 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, sa 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

Rekurzija je definicija funkcije rabeći samu funkciju. Naizgled, lambda račun ovo ne dopušta. Međutim, ovaj je utisak pogrešan. Razmotrimo na primjer funkciju faktorijela f(n) rekurzivno definiranu kao

f(n) = 1, ako n = 0; i n·f(n-1), ako n>0.

U lambda se računu ne može definirati funkcija koja uključuje samu sebe. Kako bi se ovo zaobišlo, može se započeti definiranjem funkcije, ovdje zvanom g, koja prima funkciju f kao argument i vraća drugu funkciju koja prima n kao argument:

g := λ f n. (1, ako n = 0; i n·f(n-1), ako n>0).

Funkcija koju g vraća je ili konstanta 1 ili n puta aplikacija funkcije f nad n-1. Rabeći predikat JELINULA, bilo koje bulovske i algebarske definicije gore opisane, funkcija g može biti definirana u lambda računu.

Međutim, sama g još uvijek nije rekurzivna. - kako bismo koristili g za stvaranje rekurzivne funkcije faktorijela, funkcija prosljeđena g kao f mora imati specifična svojstva. Ponajprije, funkcija prosljeđena kao f se mora ekspandirati u funkciju g pozvanu sa jednim argumentom - i taj argument mora biti funkcija koja je opet proslijeđena f!

Drugim riječima, f mora ekspandirati u g(f). Ovaj poziv g će se tad ekspandirati u gornju funkciju faktorijela i izračunati u još jednu razinu rekurzije. U toj će se ekspanziji funkcija f opet pojaviti i opet će se ekspandirati u g(f) i nastaviti rekurziju. Ova se vrsta funkcije, kad vrijedi da je f = g(f), zove fiksna točka od g, i ispada da može biti implementirana u lambda računu onim što je poznato kao paradoksalni kombinator ili operator fiksne točke i predstavljen je kao Y - Y kombinator:

Y = λ g. (λ x. g (x x)) (λ x. g (x x))

U lambda računu, Y g je fiksna točka od g, s obzirom da ekspandira u g (Y g). Sada, da bismo kompletirali naš rekurzivni poziv funkcije faktorijela, jednostavno pozivamo  g (Y g) n,  pri čemu je n broj puta koliko izračunavamo faktorijelu.

Za dan n = 5, na primjer, ovo ekspandira u:

(λ n.(1, ako n = 0; i n·((Y g)(n-1)), ako n>0)) 5
1, ako 5 = 0; i 5·(g(Y g)(5-1)), ako 5>0
5·(g(Y g) 4)
5·(λ n. (1, ako n = 0; i n·((Y g)(n-1)), ako n>0) 4)
5·(1, ako 4 = 0; i 4·(g(Y g)(4-1)), ako 4>0)
5·(4·(g(Y g) 3))
5·(4·(λ n. (1, ako n = 0; i n·((Y g)(n-1)), ako n>0) 3))
5·(4·(1, ako 3 = 0; i 3·(g(Y g)(3-1)), ako 3>0))
5·(4·(3·(g(Y g) 2)))
...

I tako dalje, rekurzivno evaluirajući strukturu algoritma. Svaka rekurzivno definirana funkcija se može shvatiti kao fiksna točka neke druge prikladne funkcije, i stoga, rabeći Y, svaka rekurzivno definirana fukcija može biti ekspandirana kao lambda izraz. Posebice, sad se može čisto definirati oduzimanje, množenje i predikat usporedbe prirodnih brojeva na rekurzivan način.

Izračunljive funkcije i lambda račun

Funkcija F: N → N prirodnih brojeva je izračunljiva funkcija u N,  F(x) = y  ako i samo ako  f x == y,  gdje su x i y Churchevi numerali koji odgovaraju x i y, respektivno. Ovo je jedan od mnogo načina definicije izračunljivosti - vidi Church-Turingova teza za diskusiju drugih pristupa i njihovu istovjetnost.

Neodlučivost ekvivalencije

Ne postoji algoritam koji kao ulaz prima dva lambda izraza i ispisuje na izlazu ISTINA ili LAŽ ovisno o tome jesu li ta dva izraza ekvivalentna ili ne. Ovo je povijesno prvi problem za koji je mogla biti dokazana nerješivost. Naravno, da bi se takvo nešto napravilo, pojam algoritma je trebao biti jasno definiran - Church je koristio definiciju preko rekurzivnih funkcija, za koju je poznato da je ekvivalentna svim ostalim razumnim definicijama pojma.

Churchev dokaz prvo svodi problem na određivanje ima li dani lambda izraz normalni oblik. Normalni je oblik ekvivalentni izraz koji ne može biti dalje reduciran. Potom pretpostavlja da je taj predikat izračunljiv, i stoga može biti izražen u lambda računu. Gradeći nad prethodnim radom Kleeneja i konstruiranjem Gödelovog pobrojanja za lambda izraze, konstruira lambda izraz e koji usko prati dokaz Gödelovog prvog teorema nepotpunosti. Ako je e apliciran na svoj vlastiti Gödelov broj, slijedi kontradikcija.

Lambda račun i programski jezici

Kao što je istaknuo Peter Landin u svom klasiku iz 1965. A Correspondence between ALGOL 60 and Church's Lambda-notation, većina programskih jezika je ukorijenjena u lambda računu, koji pruža osnovne mehanizme proceduralne apstrakcije i proceduralne (potprogramske) aplikacije.

Implementiranje lambda računa na računalu uključuje tretiranje "funkcija" kao prvorazrednih objekata, što dovodi do implementacijskih problema za stogovno zasnovane programske jezika. Ovo je poznato kao Funarg problem.

Većina istaknutih primjena lambda računa u programiranju su funkcijski programski jezici, koji u suštini implementiraju račun proširen nekim konstantama i tipovima podataka. Lisp koristi varijantu lambda notacije za definiranje funkcija, ali samo njegov čisto funkcijski podskup ("čisti Lisp") je uistinu ekvivalentan lambda računu.

Funkcijski jezici nisu samo oni koji podržavaju funkcije kao prvorazredne objekte. Brojni imperativni jezici, npr. Pascal, već dugo podržavaju prosljeđivanje potprograma kao argumenata drugim potprogramima. U C-u i C-nalik podskupu jezika C++ je istovjetna funkcionalnost ostvarena prosljeđivanjem pokazivača kodu funkcija (potprograma). Takvi su mehanizmi ograničeni na potprograme koji su eksplicitno napisani u kodu, i ne podržavaju izravno funkcije višeg reda. Neki imperativni objektno orijentirani jezici imaju konstrukte koji predstavljaju funkcije bilo kojeg reda - takvi su mehanizmi dostupni u jezicima C++, Smalltalk te odnedavno i u Eiffelu ("agenti") i C# ("delegati"). Na primjer, Eiffel "inline agent" izraz 

   agent (x: REAL): REAL do Result := x * x end

označuje objekt koji odgovara lambda izraz λ x . x*x (sa pozivom po vrijednosti). Može biti tretiran kao bilo koji drugi izraz, npr. dodijeljen varijabli ili prosljeđen rutinama. Ako je vrijednost kvadrat jednaka gornjem izrazu agenta, tada je rezultat apliciranja kvadrat na vrijednost a (β-redukcijom) izražena kao kvadrat.stavka ([a]), pri čem je argument prosljeđen kao tuple.

Sljedeći Python primjer koristi lambda oblik funkcija: 

   func = lambda x: x * x

Ovo kreira novu anonimnu funkciju nazvanu func koja može biti prosljeđena drugim funkcijama, pohranjena u varijable, etc. Python također može tretirati bilo koju drugu funkciju stvorenu standardnom def naredbom kao prvorazredni objekt.

Isto vrijedi za Smalltalk izraz 

   [ :x | x * x ]

Ovo je prvorazredni objekt (zatvaranje bloka) koji može biti pohranjen u varijable, prosljeđen kao argument itd.

Sličan C++ primjer (rabeći Boost.Lambda biblioteku): 

    for_each(v.begin(), v.end(), cout << _1 * _1 << endl;);

Ovdje standardna bibliotečna funkcija for_each iterira nad članovima vektora (ili liste) i ispisuje kvadrat svakog elementa. _1 oznaka je korištena u Boost.Lambda biblioteci za predstavljanje placeholder elemenata, predstavljenih kao x drugdje.

Jednostavan C# delegat koji prima varijablu i vraća kvadrat. Ova funkcijska varijabla potom može biti prosljeđena drugim metodama (ili funkcijskim delegatima) 

    // Deklariraj signaturu delegata
    delegate double MatDelegat(double i);
    // Kreiraj instancu delegata
    MatDelegat f = delegate(double i) { return Math.Pow(i, 2); };

    // Prosljeđivanje funkcijske varijable 'f' drugoj metodi, izvršujući
    // i vraćajući rezultat funkcije
    double Izvrsi(MatDelegat funkc)
    {
        return funkc(100);
    }

Konkurentnost i paralelizam

Church-Rosserovo svojstvo lambda računa znači da se evaluacija (β-redukcija) može izvesti u bilo kojem redoslijedu, čak i konkurentno. (Uistinu, lambda račun je referencijski transparentan.) Iako ovo znači da lambda račun može modelirati razne nedeterminističke evaluacijske strategije, ne pruža neku bogatiju notaciju paralelizma, niti može izraziti bilo koji problem konkurentnosti. Aktor model i procesni računi kao što su CSP, CCS, π račun i ambijentalni račun su dizajnirani sa takve svrhe.

Iako je nedeterministički lambda račun sposoban izraziti sve parcijalno rekurzivne funkcije, nije kadar izraziti sva računanja. Na primjer, nije sposoban izraziti neograničeni nedeterminizam (tj. za svaki se nedeterministički lambda izraz jamči terminacija - terminira u konačnom broju izraza). Međutim, postoje konkurentni programi za koje se jamči zaustavljanje i koji terminiraju u beskonačnom broju stanja [Clinger 1981, Hewitt 2006].

Vidjeti također

Izvori

Vanjske poveznice

Dobavljeno iz "https://enciklopedija.cc/index.php?title=Lambda_račun&oldid=46853"