Lambda račun je formalni sustav u matematičkoj logici za izražavanje izračuna temeljenih na apstrakciji i primjenu funkcija korištenjem povezivanja i zamjene varijabli. Ovo je univerzalni model koji se može primijeniti na dizajn bilo kojeg Turingovog stroja. Lambda račun prvi je uveo Church, poznati matematičar, 1930-ih.
Sustav se sastoji od izgradnje lambda članova i izvođenja operacija redukcije na njima.
Objašnjenja i primjene
Grčko slovo lambda (λ) koristi se u lambda izrazima i lambda izrazima za označavanje vezivanja varijable u funkciji.
Lambda račun se može otkucati ili upisati. U prvoj varijanti funkcije se mogu koristiti samo ako su sposobne primati podatke ove vrste. Upisani lambda računi su slabiji, mogu izraziti manju vrijednost. Ali, s druge strane, omogućuju vam da dokažete više stvari.
Jedan od razloga zašto postoji toliko različitih tipova je želja znanstvenika da učine više bez odustajanja od prilike da dokažu jake teoreme lambda računa.
Sustav ima primjene u mnogim različitim područjima matematike, filozofije, lingvistike i informatike. Prije svega, lambda račun je račun koji je odigrao važnu ulogu u razvoju teorije programskih jezika. Sustavi 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 Church 1930-ih kao dio svog istraživanja o temeljima znanosti. Pokazalo se da je izvorni sustav logički nedosljedan 1935. kada su Stephen Kleen i J. B. Rosser razvili Kleene-Rosserov paradoks.
Kasnije, 1936. godine, Church je izdvojio i objavio samo dio koji je relevantan za izračune, što se danas naziva neupisanim lambda računom. Godine 1940. također je uveo slabiju, ali logički konzistentnu teoriju poznatu kao sustav 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.
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 nakon koje slijede dvije tipografske promjene. Primjer za označavanje: za funkciju f s f (y)=2y + 1 je 2ŷ + 1. I ovdje koristimo umetak ("šešir") iznad y za označavanje ulazne varijable.
Crkva je izvorno namjeravala koristiti slične simbole, ali slagači nisu mogli postaviti simbol "šešira" iznad slova. Umjesto toga, ispisali su ga izvorno kao "/\y.2y+1". U sljedećoj epizodi montaže, daktilografi su zamijenili "/ \" vizualno sličnim znakom.
Uvod u lambda račun
Sustav se sastoji od jezika pojmova, koji su odabrani određenom formalnom sintaksom, i skupa pravila transformacije koja dopuštaju da se njima manipulira. Posljednja točka može se smatrati teorijom jednačina ili operativnom definicijom.
Sve funkcije u lambda računu su anonimne, što znači da nemaju imena. Uzimaju samo jednu ulaznu varijablu, a curry se koristi za implementaciju dijagrama s više varijabli.
Lambda uvjeti
Sintaksa računanja neke izraze definira kao valjane, a druge kao nevaljane. Baš kao što su različiti nizovi znakova valjani C programi, a neki nisu. Stvarni izraz lambda računa naziva se "lambda izraz".
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 izraz:
- 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 pojam. Dakle, koncept je valjan ako i samo ako se može dobiti ponavljanom primjenom ova tri pravila. Međutim, neke zagrade mogu biti izostavljene prema drugim kriterijima.
Definicija
Lambda izrazi sastoje se od:
- varijable v 1, v 2, …, v n, …
- simboli apstrakcije 'λ' i točke '.'
- zagrade ().
Skup Λ može se definirati induktivno:
- Ako je x varijabla, tada je x ∈ Λ;
- x nije konstanta i M ∈ Λ, tada (λx. M) ∈ Λ;
- M, N ∈ Λ, zatim (MN) ∈ Λ.
Oznaka
Kako bi zapis lambda izraza bio neopterećen, obično se koriste sljedeće konvencije:
- Vanjske zagrade izostavljene: MN umjesto (MN).
- Pretpostavlja se da aplikacije ostaju asocijativne: može se napisati MNP umjesto ((MN) P).
- Tijelo apstrakcije proteže se 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 gdje god se nalazi u tijelu 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 s dodatkom X x na M. Sve ostale nestabilne nazivaju se slobodnima.
Na primjer, u izrazu λ y. x x y, y - vezan nestalan, a x - slobodan. Također je vrijedno napomenuti da je varijabla grupirana 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 označen je 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 također su poznati kao kombinatori i ekvivalentni su terminima u kombinatornoj logici.
Skraćenica
Značenje lambda izraza određeno je 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 ga takođergovorimo o rezultirajućim ekvivalentnostima: dva izraza su β-ekvivalentna ako se mogu β-transformirati u istu komponentu, a α / η-ekvivalencija je definirana slično.
Izraz redex, skraćeno 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 s x u M. Komponenta na koju se redex reducira zove se njegov redukt. Smanjenje (λ x. M) N je M [x:=N].
Ako x nije slobodan u M, λ x. M x također em-REDEX s regulatorom M.
α-transformacija
Alfa preimenovanja omogućuju vam promjenu naziva vezanih varijabli. Na primjer, x. x može dati λ y. y. Za pojmove koji se razlikuju samo u alfa transformaciji kaže se da su α-ekvivalentni. Često, kada se koristi lambda račun, α-ekvivalenti se smatraju recipročnim.
Točna pravila za alfa konverziju nisu sasvim trivijalna. Prvo, s ovom apstrakcijom, preimenovane su samo one varijable koje su povezane s istim sustavom. Na primjer, alfa transformacija λ x.λ x. x može dovesti do λ y.λ x. x, ali to ne mora dovesti do λy.λx.y Potonje ima drugačije značenje od izvornog. 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 s 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 pretvorba može se koristiti za pojednostavljenje razlučivanja imena. U isto vrijeme, vodeći računa da koncept varijable ne maskira oznaku u području koje sadrži.
U zapisu De Bruyneovog indeksa, bilo koja dva alfa-ekvivalentna pojma su sintaktički identična.
Zamjena
Promjene koje je zapisao E [V:=R] su proces zamjene svih slobodnih pojavljivanja varijable V u izrazu E s prometom R. Zamjena u terminima λ definirana je lambdom 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 uvjetom da je y ∉ FV (N).
Za zamjenu u lambda apstrakciju, ponekad je potrebno α-transformirati izraz. Na primjer, nije toč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 definirana 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 može se promatrati kao isto što i koncept lokalne reducibilnosti prema prirodnoj dedukciji putem Curry-Howardovog izomorfizma.
η-transform
Ova konverzija izražava ideju ekstenzionalnosti, koja je u ovom kontekstu da su dvije funkcije jednake kada daju isti rezultat za sve argumente. Ova pretvorba razmjenjuje se između λ x. (F x) i f kad god se x ne čini slobodnim u f.
Ova se radnja može smatrati istim kao i koncept lokalne potpunosti u prirodnoj dedukciji kroz Curry-Howardov izomorfizam.
Normalni oblici i fuzija
Za netipizirani lambda račun, pravilo β-redukcije općenito nije ni jaka ni slaba normalizacija.
Unatoč tome, može se pokazati da se β-redukcija spaja kada se izvodi prije α-transformacije (tj., dva normalna oblika mogu se smatrati jednakima ako je moguća α-transformacija iz jednog u drugi).
Stoga, i pojmovi koji se jako normaliziraju i pojmovi koji se slabo prilagođavaju imaju jedan normalni oblik. Za prve termine, svaka strategija smanjenja zajamčeno će rezultirati tipičnom konfiguracijom. Dok za slabo normalizirajuće uvjete, neke strategije smanjenja to možda neće pronaći.
Dodatne metode programiranja
Postoji mnogo idioma stvaranja za lambda račun. Mnogi od njih su izvorno razvijeni u kontekstu korištenja sustava kao osnove za semantiku programskog jezika, učinkovito ih primjenjujući kao konstrukciju niske razine. 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.
Nazvane konstante
U lambda računu, biblioteka ima oblik skupa prethodno definiranih funkcija, gdje su pojmovi samo konkretne konstante. Čisti račun nema koncept imenovanih nepromjenjivih vrijednosti budući da su svi atomski lambda pojmovi varijable. Ali oni se također mogu oponašati uzimajući promjenjivo kao ime konstante, korištenjem lambda apstrakcije za vezanje tog hlapljivog elementa u tijelu i primjenom te apstrakcije na namjeravanu definiciju. Dakle, ako upotrijebite f za predstavljanje M u N, mogli biste reći
(λ f. N) M.
Autori često uvode sintaktički koncept kao što je dopustiti da se stvari napiš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 nakon kojih slijedi jedan lambda član, koristeći one definicije koje čine većinu programa.
Uočljivo ograničenje ovog puštanja je da ime f nije definirano u M,budući da je M izvan obvezujućeg opsega lambda apstrakcije f. To znači da se atribut rekurzivne funkcije ne može koristiti kao M s let. Naprednija letrec sintaksa, koja vam omogućuje pisanje rekurzivnih definicija funkcija u ovom stilu, dodatno koristi kombinatore fiksne točke.
Tiskani analozi
Ovaj tip je tipizirani formalizam koji koristi simbol za predstavljanje anonimne apstrakcije funkcije. U tom kontekstu, tipovi su obično objekti sintaktičke prirode koji se pripisuju lambda pojmovima. Točna priroda ovisi o dotičnom proračunu. S određene točke gledišta, tipizirani LI se može smatrati poboljšanjima netipiziranog LI. Ali s druge strane, oni se također mogu smatrati temeljnijom teorijom, a netipizirani lambda račun je poseban slučaj sa samo jednom vrstom.
Typed LI temelj su 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 sustava tipova za programske jezike. Ovdje mogućnost tipkanja obično bilježi željena svojstva programa, na primjer, neće uzrokovati kršenje pristupa memoriji.
Utipkani lambda računi usko su povezani s matematičkom logikom i teorijom dokaza kroz Curry-Howardov izomorfizam i mogu se smatrati internim jezikom klasa kategorija, na primjer, kojijednostavno je stil kartezijanskih zatvaranja.
