Lambda račun je formalni sistem u matematičkoj logici za izražavanje kalkulacija zasnovanih na apstrakciji i primjenu funkcija korištenjem povezivanja i zamjene varijabli. Ovo je univerzalni model koji se može primijeniti na dizajn bilo koje Turingove mašine. Lambda račun je prvi uveo Church, poznati matematičar, 1930-ih.
Sistem se sastoji od izgradnje lambda članova i izvođenja operacija redukcije na njima.
Objašnjenja i aplikacije
Grčko slovo lambda (λ) se koristi u lambda izrazima i lambda terminima za označavanje vezivanja varijable u funkciji.
Lambda račun se može otkucati ili otkucati. U prvoj varijanti, funkcije se mogu koristiti samo ako su sposobne primati podatke ovog tipa. Otkucani lambda računi su slabiji, mogu izraziti manju vrijednost. Ali, s druge strane, oni vam omogućavaju da dokažete više stvari.
Jedan razlog zašto postoji toliko različitih tipova je želja naučnika da urade više bez odustajanja od prilike da dokažu jake teoreme lambda računa.
Sistem ima primjene u mnogim različitim oblastima matematike, filozofije, lingvistike i računarstva. Prije svega, lambda račun je račun koji je odigrao važnu ulogu u razvoju teorije programskih jezika. Sistemi implementiraju stilove funkcionalne kreacije. Oni su također vruća tema istraživanja u teoriji ovih kategorija.
Za lutke
Lambda račun uveo je matematičar Alonzo Čerč 1930-ih kao dio svog istraživanja osnova nauke. Originalni sistem se pokazao kao logički nekonzistentan 1935. godine kada su Stephen Kleen i J. B. Rosser razvili Kleene-Rosser paradoks.
Kasnije, 1936. godine, Church je izdvojio i objavio samo dio koji je relevantan za proračune, ono što se danas zove netipizirani lambda račun. Godine 1940. on je također uveo slabiju, ali logički konzistentnu teoriju poznatu kao sistem prvog tipa. U svom radu on objašnjava cijelu teoriju jednostavnim riječima, pa se može reći da je Church objavio lambda račun za lutke.
Sve do 1960-ih, kada je njegov odnos prema programskim jezicima postao jasan, λ je bio samo formalizam. Zahvaljujući primjenama Richarda Montagua i drugih lingvista u semantici prirodnog jezika, račun je zauzeo ponosno mjesto i u lingvistici i u informatici.
Porijeklo simbola
Lambda ne znači riječ ili akronim, dolazi iz reference u Russell's Principal Mathematics praćenoj dvije tipografske promjene. Primjer notacije: za funkciju f sa f (y)=2y + 1 je 2ŷ + 1. I ovdje koristimo karet (“šešir”) iznad y da označimo ulaznu varijablu.
Crkva je prvobitno nameravala da koristi slične simbole, ali slagači nisu mogli da stave simbol "šešir" iznad slova. Umjesto toga, oni su ga originalno ispisali kao "/\y.2y+1". U sljedećoj epizodi montaže, daktilografi su zamijenili "/ \" vizualno sličnim karakterom.
Uvod u lambda račun
Sistem se sastoji od jezika pojmova, koji su odabrani određenom formalnom sintaksom, i skupa pravila transformacije koja omogućavaju da se njima manipuliše. Posljednja tačka se može smatrati teorijom jednačina ili kao operativna definicija.
Sve funkcije u lambda računu su anonimne, što znači da nemaju imena. Oni uzimaju samo jednu ulaznu varijablu, a curry se koristi za implementaciju dijagrama sa više varijabli.
Lambda uslovi
Sintaksa računanja neke izraze definira kao važeće, a druge kao nevažeće. Baš kao što su različiti nizovi znakova važeći C programi, a neki nisu. Stvarni izraz lambda računa naziva se "lambda termin".
Sljedeća tri pravila daju induktivnu definiciju koja može bitiprimijeniti na konstrukciju svih sintaktički valjanih koncepata:
Sama varijabla x je važeći lambda termin:
- ako je T LT i x nije konstantan, tada se (lambda xt) naziva apstrakcija.
- ako su T kao i s koncepti, tada se (TS) naziva aplikacija.
Ništa drugo nije lambda termin. Dakle, koncept je valjan ako i samo ako se može dobiti ponovljenom primjenom ova tri pravila. Međutim, neke zagrade mogu biti izostavljene prema drugim kriterijima.
Definicija
Lambda izrazi se sastoje od:
- varijable v 1, v 2, …, v n, …
- simboli apstrakcije 'λ' i tačke '.'
- zagrade ().
Skup Λ se može definirati induktivno:
- Ako je x varijabla, tada je x ∈ Λ;
- x nije konstanta i M ∈ Λ, tada (λx. M) ∈ Λ;
- M, N ∈ Λ, zatim (MN) ∈ Λ.
Designation
Da bi notacija lambda izraza ostala nesmetana, obično se koriste sljedeće konvencije:
- Spoljne zagrade su izostavljene: MN umjesto (MN).
- Pretpostavlja se da aplikacije ostaju asocijativne: može se napisati MNP umjesto ((MN) P).
- Telo apstrakcije se proteže dalje udesno: λx. MN znači λx. (MN), ne (λx. M) N.
- Slijed apstrakcija je smanjen: λx.λy.λz. N može biti λxyz. N.
Slobodne i vezane varijable
Operator λ povezuje svoju nekonstantu gde god da se nalazi u telu apstrakcije. Varijable koje spadaju u opseg nazivaju se vezane. U izrazu λ x. M, λ x dio se često naziva vezivom. Kao da nagovještava da varijable postaju grupa sa dodatkom X x na M. Sve ostale nestabilne se nazivaju slobodnima.
Na primjer, u izrazu λ y. x x y, y - vezano nestalno, a x - slobodno. Takođe je vredno napomenuti da je varijabla grupisana prema svojoj „najbližoj“apstrakciji. U sljedećem primjeru, rješenje lambda računa predstavljeno je jednim pojavljivanjem x, što je povezano s drugim pojmom:
λ x. y (λ x. z x)
Skup slobodnih varijabli M je označen kao FV (M) i definiran je rekurzijom preko strukture pojmova kako slijedi:
- FV (x)={x}, gdje je x varijabla.
- FV (λx. M)=FV (M) {x}.
- FV (MN)=FV (M) ∪ FV (N).
Formula koja ne sadrži slobodne varijable naziva se zatvorena. Zatvoreni lambda izrazi su također poznati kao kombinatori i ekvivalentni su terminima u kombinatornoj logici.
Skraćenica
Značenje lambda izraza je određeno načinom na koji se mogu skratiti.
Postoje tri vrste rezova:
- α-transform: promjena vezanih varijabli (alfa).
- β-redukcija: primjena funkcija na njihove argumente (beta).
- η-transform: pokriva pojam ekstenzivnosti.
Evo i njegagovorimo o rezultirajućim ekvivalentnostima: dva izraza su β-ekvivalentna ako se mogu β-transformirati u istu komponentu, a α / η-ekvivalentnost je definisana slično.
Izraz redex, skraćenica za reducibilni promet, odnosi se na podteme koje se mogu smanjiti jednim od pravila. Lambda račun za lutke, primjeri:
(λ x. M) N je beta redex u izrazu za zamjenu N sa x u M. Komponenta na koju se redex reducira zove se njegov redukt. Smanjenje (λ x. M) N je M [x:=N].
Ako x nije slobodno u M, λ x. M x također em-REDEX sa regulatorom M.
α-transformacija
Alfa preimenovanja vam omogućavaju da promijenite imena vezanih varijabli. Na primjer, x. x može dati λ y. y. Za termine koji se razlikuju samo u alfa transformaciji se kaže da su α-ekvivalentni. Često, kada se koristi lambda račun, α-ekvivalenti se smatraju recipročnim.
Tačna pravila za alfa konverziju nisu sasvim trivijalna. Prvo, sa ovom apstrakcijom, samo one varijable koje su povezane sa istim sistemom se preimenuju. Na primjer, alfa transformacija λ x.λ x. x može dovesti do λ y.λ x. x, ali to ne mora dovesti do λy.λx.y. Ovo posljednje ima drugačije značenje od originala. Ovo je analogno konceptu programiranja varijabilnog sjenčanja.
Drugo, alfa transformacija nije moguća ako bi rezultirala hvatanjem nestalne druge apstrakcije. Na primjer, ako zamijenite x sa y u λ x.λ y. x, onda možete dobitiλy.λy. u, što uopće nije isto.
U programskim jezicima sa statičkim opsegom, alfa konverzija se može koristiti za pojednostavljenje rezolucije imena. Istovremeno, vodeći računa da koncept varijable ne maskira oznaku u oblasti koja sadrži.
U zapisu De Bruyneovog indeksa, bilo koja dva alfa-ekvivalentna termina su sintaktički identična.
Zamjena
Promjene koje je zapisao E [V:=R] su proces zamjene svih slobodnih pojavljivanja varijable V u izrazu E sa prometom R. Zamjena u terminima λ je definirana lambda rekurzije račun o strukturi koncepta kako slijedi (napomena: x i y - samo varijable, a M i N - bilo koji λ-izraz).
x [x:=N] ≡ N
y [x:=N] ≡ y ako je x ≠ y
(M 1 M 2) [x:=N] ≡ (M 1 [x:=N]) (M 2 [x:=N])
(λ x. M) [x:=N] ≡ λ x. M
(λ y. M) [x:=N] y λ y. (M [x:=N]) ako je x ≠ y, pod uslovom da je y ∉ FV (N).
Za supstituciju u lambda apstrakciju, ponekad je potrebno α-transformirati izraz. Na primjer, nije tačno da (λ x. Y) [y:=x] rezultira (λ x. X) jer je zamijenjeni x trebao biti slobodan, ali je na kraju bio vezan. Ispravna zamjena u ovom slučaju je (λ z. X) do α-ekvivalencije. Imajte na umu da je zamjena jedinstveno definirana do lambda.
β-smanjenje
Beta smanjenje odražava ideju primjene funkcije. Beta-redukcija je definisana terminimazamjena: ((X V. E) E ') je E [V:=E'].
Na primjer, uz pretpostavku nekog kodiranja 2, 7, ×, postoji sljedeća β-redukcija: ((λ n. N × 2) 7) → 7 × 2.
Beta redukcija se može posmatrati kao isto što i koncept lokalne reducibilnosti prema prirodnoj dedukciji preko Curry-Howard izomorfizma.
η-transform
Ova konverzija izražava ideju ekstenzivnosti, koja je u ovom kontekstu da su dvije funkcije jednake kada daju isti rezultat za sve argumente. Ova konverzija se razmjenjuje između λ x. (F x) i f kad god se x ne čini slobodnim u f.
Ova akcija se može smatrati istim konceptom lokalne potpunosti u prirodnoj dedukciji kroz Curry-Howard izomorfizam.
Normalni oblici i fuzija
Za netipizirani lambda račun, pravilo β-redukcije općenito nije ni jaka ni slaba normalizacija.
Ipak, može se pokazati da se β-redukcija spaja kada se izvodi prije α-transformacije (tj., dva normalna oblika se mogu smatrati jednakima ako je moguća α-transformacija iz jednog u drugi).
Stoga, i termini koji se jako normalizuju i pojmovi koji se slabo prilagođavaju imaju jednu normalnu formu. Za prve termine, svaka strategija smanjenja garantovano će rezultirati tipičnom konfiguracijom. Dok za slabo normalizirajuće uslove, neke strategije smanjenja ga možda neće pronaći.
Dodatne metode programiranja
Postoji mnogo kreacionih idioma za lambda račun. Mnogi od njih su prvobitno razvijeni u kontekstu korišćenja sistema kao osnove za semantiku programskog jezika, efektivno ih primenjujući kao konstrukciju niskog nivoa. Budući da neki stilovi uključuju lambda račun (ili nešto vrlo slično) kao isječak, ove tehnike se također koriste u praktičnom stvaranju, ali se tada mogu smatrati nejasnim ili stranim.
Imenovane konstante
U lambda računu, biblioteka ima oblik skupa prethodno definisanih funkcija, gde su termini samo konkretne konstante. Čisti račun nema koncept imenovanih nepromjenjivih vrijednosti jer su svi atomski lambda pojmovi promjenljive. Ali oni se također mogu oponašati uzimanjem promjenjivog kao imena konstante, korištenjem lambda apstrakcije da se veže taj volatile u tijelu i primjenom te apstrakcije na predviđenu definiciju. Dakle, ako koristite f za predstavljanje M u N, mogli biste reći
(λ f. N) M.
Autori često uvode sintaktički koncept kao što je dozvoliti da se stvari pišu na intuitivniji način.
f=M do N
Ulančavanjem takvih definicija, može se napisati "program" lambda računa kao nula ili više definicija funkcija praćenih jednim lambda članom, koristeći one definicije koje čine najveći dio programa.
Primetno ograničenje ove oznake je da ime f nije definirano u M,pošto je M izvan obvezujućeg opsega lambda apstrakcije f. To znači da se atribut rekurzivne funkcije ne može koristiti kao M sa let. Naprednija letrec sintaksa, koja vam omogućava da pišete rekurzivne definicije funkcija u ovom stilu, dodatno koristi kombinatore fiksne tačke umjesto toga.
Štampani analozi
Ovaj tip je otkucani formalizam koji koristi simbol za predstavljanje anonimne apstrakcije funkcije. U ovom kontekstu, tipovi su obično objekti sintaktičke prirode koji se dodeljuju lambda terminima. Tačna priroda zavisi od računa o kojem je riječ. Sa određene tačke gledišta, tipizirani LI se može smatrati poboljšanjima netipiziranog LI. Ali s druge strane, oni se također mogu smatrati fundamentalnijom teorijom, a netipizirani lambda račun je poseban slučaj sa samo jednim tipom.
Typed LI su osnova programskih jezika i okosnica funkcionalnih jezika kao što su ML i Haskell. I, posrednije, imperativni stilovi stvaranja. Tipizirani lambda računi igraju važnu ulogu u razvoju sistema tipova za programske jezike. Ovdje tipizacija obično bilježi željena svojstva programa, na primjer, neće uzrokovati kršenje pristupa memoriji.
Utipkani lambda računi su usko povezani sa matematičkom logikom i teorijom dokaza kroz Curry-Howard izomorfizam i mogu se smatrati internim jezikom klasa kategorija, na primjer, kojijednostavno je stil kartezijanskog zatvaranja.
