Lambda račun

Lambda račun (oznaka λ-račun) je formalni sistem u matematičkoj logici za predstavljanje računanja baziranog na apstrakciji funkcija i aplikacija koristeći vezivanje i supstituciju promenljive. Uveo ga je Alonzo Čerč da formuliše koncept efektivnog računanja, lambda račun je naišo na prve uspehe na polju teorije računanja, kao što je negativan odgovor na Hilbertov problem odluke. Lambda račun je konceptualno jednostavan univerzalni model računanja (Tjuring je pokazao 1937. godine da Tjuringova mašina jednaka lambda računu u ekspresivnosti). Ime potiče od grčkog slova lambda (λ) korišćenog da označi vezivanje promenljivih u funkciji. Slovo je samo po sebi proizvoljno i nema nikakvo specijalno značenje. Lambda račun se uči i koristi u računarstvu zbog svoje korisnosti u prikazivanju funkcionalnog razmišljanja i iterativne redukcije.

Zbog važnosti pojma vezivanja promenljive i substitucije, ne postoji samo jedan sistem lambda računa, i u praksi postoje "tipske" i "netipske" varijante. Istorijski gledano, najvažniji sistem je bio netipski lambda račun, u kojem funkcija aplikacije nema restrikcija (pojam domena funkcije nije ugrađen u sistem. U Čerč-Tjuringovoj tezi, netipski lambda račun je podešen da bude moguće izračunati sve efektivno izračunive funkcije. Tipski lambda račun je varijacija koja ima restrikcije za funkciju aplikacije, tako da se funkcija može primeniti samo ako se prihvati ulazni tip podataka.

Danas, lambda račun ima ulogu u mnogo različitih svera, kao npr. u matematici, filozofiji, lingvistici, i računarstvu. Još uvek se koristi u oblasti teorije računanja, kao i Tjuringova mašina koja je vrlo važan model za računanje. Lambda račun je odigrao veoma važnu ulou u razvoju teorije programskih jezika. Delovi brojača, u lambda računu u računarstvu, su funkcionalni programi, koji implementiraju lambda račun (povećati neke konstante i tipove podataka). Pored programskih jezika, labmda račun igra ulogu u teoriji dokaza. Glavni primer toga je Kari-Hauardova korespondencija, koja daje korespondenciju između različitih sistema tipova lambda računa i sistema formalne logike.

Istorija lambda računa u matematici

Lambda račun je uveo Alonzo Čerč u 1930—im godinama kao deo istrage o osnovama matematike. Originalni sistem je pokazan kao logički protivrečan 1935. godine kada su Stiven Klin i J. B. Roser razvili Klin-Roserov paradoks.

Nakon toga, u 1936. godini, Čerč je izolovao i objavio samo deo bitan za računanje, koji se danas zove netipski lambda račun. U 1940. godini, on je takođe uveo računski slabiji, ali logički dosledniji sistem, znan kao jednostavni tipski lambda račun.

Motivacija

Računske funkcije predstavljaju krucijalan koncept u računarstvu i matematici. Lambda račun daje jednostavu semantiku za izračunavanje, omogućavajući osobine izračunavanja da budu formalno učene. Lambda račun uključuje dva uprošćavanja koja čine semantiku jednostavnom. Prvo pojednostavljenje je to da Lambda račun tretira funkciju "anonimno", bez davanja eksplicitnih imena. Na primer, funkcija 

$\operatorname {square\_sum} (x,y)=x\times x+y\times y$

može se ponovo napisati u anonimnoj formi kao

$(x,y)\mapsto x\times x+y\times y$

(čita se kao "par x i y je mapiran u ${\textstyle x\times x+y\times y}$"). Slično,

$\operatorname {id} (x)=x$

se može napisati u anonimnoj formi ${\textstyle x\mapsto x}$, gde je ulaz jednostavno mapiran u samog sebe 

Drugo pojednostavljenje je to da lambda račun koristi samo funkcije jednog ulaza. Obična funkcija koja zahteva dva ulaza , za instancu ${\textstyle \operatorname {square\_sum} }$ (zbir kvadrata) funkcije, može se napisati kao jedna ekvivalentna funkcija koja prima jedan ulaz, a da izlaz vraća drugu funkciju, koja zauzvrat prima jedan ulaz. Na primer,

$(x,y)\mapsto x\times x+y\times y$

se može napisati kao

$x\mapsto (y\mapsto x\times x+y\times y)(y)$

Ova metoda, poznata i kao kariing, transformiše funkciju koja uzima više argumenata u lanac funkcija, gde svaka ima jedan argument.

Funkcionalno okruženje  ${\textstyle \operatorname {square\_sum} }$ funkcije sa argumentima (5, 2), dobijeno odjednom

${\textstyle ((x,y)\mapsto x\times x+y\times y)(5,2)}$

${\textstyle =5\times 5+2\times 2}$

${\textstyle =29}$,

dok procena karijeve verzije zahteva još jedan korak

${\textstyle ((x\mapsto (y\mapsto x\times x+y\times y))(5))(2)}$

${\textstyle =(y\mapsto 5\times 5+y\times y)(2)}$

${\textstyle =5\times 5+2\times 2}$

${\textstyle =29}$

dobija se isti rezultat.

Lambda račun

Lambda račun se sastoji od programa lambda uslova, koji su definisani određenom formalnom sintaksom, i setom transformacijskih pravila, koji dopuštaju manipulaciju lambda uslova. Ova transformacijska pravila se mogu predstaviti kao ekvivalentna teorija ili kao operacionalizam.

Kao što je već opisano, sve funkcije u lambda računu su u stvari anonimne funkcije, tj. nemaju ime. Dozvoljavaju samo jednu ulaznu promenljivu, sa karijevom verzijom da se ubace funkcije sa nekoliko promenljivih.

Lambda pravila

Sintaksa lambda računa definiše neke izraze kao dozvoljene izraze lambda računa i neke nevažeće, kao što su na primer stringovi koji se sastoje od karaktera validnih C programa a neki ipak nisu. Dozvoljeni izraz lambda računa se naziva lambda izraz.

Sledeća tri pravila daju induktivnu definiciju koja se mogu iskoristiti za pravljenje sintatički ispravnih lambda izrazi:

• promenljiva, $x$, je sam po sebi validan lambda izraz
• ako je $t$ lambda izraz, a $x$ je promenljiva, onda je $(\lambda x.t)$ lambda izraz (naziva se i  lambda apstrakcijom);
• ako su $t$ i $s$ lambda izrazi, onda je i $(ts)$ lambda izraz (aplikacija).

Ništa drugo nije lambda uslov. Lambda uslov je validan ako i samo ako se može dobiti primenom ova tri pravila. Međutim, neke zagrade mogu biti izostavljene u skladu sa nekim pravilima. Na primer, spoljašnje zagrade se obično ne pišu. 

Lambda apstrakcija $\lambda x.t$ je definicija anonimne funkcije koja može da uzme jedan ulaz $x$ i zameni ga u izraz $t$. Na taj način se definišu anonimne funkcije koje uzimaju x a vraćaju t. Na primer, $\lambda x.x^{2}+2$ je lambda apstrakcija funkcije $f(x)=x^{2}+2$ koristeći izraz $x^{2}+2$ za $t$. Definicija funkcije sa lambda abrstrakcijom samo "postavlja" funkciju ali je ne uvodi. Abrstrakcija vezuje promenljivu $x$ u izraz $t$.

Aplikacija $ts$ predstavlja primenu funkcije $t$ na ulaz $s$, koji predstavlja čin poziva funkcije $t$ u odnosu na ulaz $s$ da bi se dobio $t(s)$.

Ne postoji koncept promenljivih deklaracija u lambda računu. U definiciji kao što je $\lambda x.x+y$ (i.e. $f(x)=x+y$), lambda račun tretira $y$ promenljivu koja još uvek nije definisana. Lambda abrstrakcija $\lambda x.x+y$ je sintatički ispravna, i predstavlja funkciju koja dodaje svoje unose za još uvek nepoznatu $y$.

Zagrade se mogu koristiti tj. mogu biti potrebne nekim izrazima. Na primer, $\lambda x.((\lambda x.x)x)$ and $(\lambda x.(\lambda x.x))x$ označava reziličite izraze (iako se slučajno sređivanjem dobija isti rezultat). Evo prvog primera definisanja funkcije koja definiše funkciju i vraća rezultat uzimajući h iz dečije-funkcije (primeni funkciju a zatim vrati), dok drugi primer definiše funkciju koja vraća funkciju za bilo koji ulaz vraća njegovu vrednost uzete h (vraća funkciju a onda je primeni).

Funkcije koje operišu (vrše neku radnju) na druge funkcije

U lambda računu, funkcije su uzete da budu vrednosti prve klase, pa tako funkcije mogu biti korišćene kao ulazi, ili biti vraćene kao izlazi iz drugih funkcija.

Na primer, $\lambda x.x$ predstavlja identičnu funkciju, $x\rightarrow x$, a  $(\lambda x.x)y$ predstavlja identičnu funkciju primenjenu na  $y$. Dakle, $(\lambda x.y)$ predstavlja konstantnu funkciju $x\rightarrow y$, funkciju koja uvek vraća $y$, bez obzira na ulaz. U lambda računu, aplikacija funkcije se smatra levo-asocijativnom, što znači da $stx$ znači $(st)x$.

Potoji nekoliko pojmova "ekvivalencije" i "redukcije" koja dozvoljava lambda izrazima da budu "pojednostavljeni" svojim "ekvivalentnim" lambda izrazima.

Alfa ekvivalencija

Osnovna forma ekvivalencije, definisana na osnovu lambda uslova . Ona nam kazuje da partikulatan izbor ograničene promenljive nije bitan. Instance, $\lambda x.x$ i $\lambda y.y$ su alfa-ekvivalentni izrazi, i predstavljaju iste funkcije (identične funkcije). Izrazi $x$ i $y$ nisu alfa-ekvivalentni, zato što nisu ograničene lambda apstrakcijom. U dosta slučajeva, obično se prvo indetifikuju alfa-ekvivalentni izrazi.

Ove definicije su neophodne u odredđivanju beta redukcije.

Slobodne promenljive

Slobodne promenljive su one promenljive koje nisu ograničene labda apstrakcijom. Niz izraza, koji je sačinjen od slobodnih promenljivih, je definisan induktivno:

• Slobodne promenljive $x$ su samo $x$
• Skup slobodnih promenljivih $\lambda x.t$ je skup od slobodnih promenljivih  $t$, ali sa brisanjem $x$
• Skup slobodnih promenljivih $ts$ je unija svih skupova slobodnih promenljivih $t$ i skupova slobodnih promenljivih $s$.

Na primer, lambda izraz predstavljen identitetom $\lambda x.x$ nema slobodne promenljive , ali funkcija $\lambda x.x+y$ ima jednu slobodnu promenljivu, $y$.

Izbegavanje-utvrđenih izmena

Pretpostavimo da su $t$, $s$ i $r$ lambda izrazi a $x$ i $y$ da su promenljive. Oznaka $t[x:=r]$ označava zamenu $r$ za $x$ u $t$ u maniru uhvatiti-izbegnuto. Ovo je definisano kao:

• $x[x:=r]=r$;
• $y[x:=r]=y$ if $x\neq y$;
• $(ts)[x:=r]=(t[x:=r])(s[x:=r])$;
• $(\lambda x.t)[x:=r]=\lambda x.t$;
• $(\lambda y.t)[x:=r]=\lambda y.(t[x:=r])$ ako je $x\neq y$, $y$ nije u slobodnoj promenljivoj $r$. Za promenljivu $y$ se kaže da je sveža za r.

Na primer, $(\lambda x.x)[y:=y]=\lambda x.(x[y:=y])=\lambda x.x$, i $((\lambda x.y)x)[x:=y]=((\lambda x.y)[x:=y])(x[x:=y])=(\lambda x.y)y$.

Uslov svežine (zahteva da $y$ nije u slobodnoj promenljivoj $r$) je krucijalan u smislu da osigurava da zamena ne menja značenje funkcija. Na primer, zamena je napravljena tako da ignoriše uslov svežine: $(\lambda x.y)[y:=x]=\lambda x.(y[y:=x])=\lambda x.x$. Ova zamena pretvara konstantnu funkciju $\lambda x.y$ u identitet $\lambda x.x$ uz pomoć izmene.

Generalno, neuspeh u uspostavljanju uslova svežine se može ispraviti uz pomoć alfa-preimenovanja sa odgovorajućom svežom promenljivom. Na primer, vraćajući se nazad na našu tačnu notaciju zamene, u $(\lambda x.y)[y:=x]$ lambda apstrakcija se može preimenovati uz pomoć nove promenljive $z$, da se dobije $(\lambda z.y)[y:=x]=\lambda z.(y[y:=x])=\lambda z.x$, i značenje funkcije je zaštićeno zamenom.

Beta redukcija

Pravilo beta redukcije kaže da se $(\lambda x.t)s$ redukuje na izraz $t[x:=s]$. Oznaka $(\lambda x.t)s\to t[x:=s]$ se koristi da označi da se $(\lambda x.t)s$ beta redukuje do $t[x:=s]$. Na primer, za svako $s$, $(\lambda x.x)s\to x[x:=s]=s$. Ovo znači da je $\lambda x.x$ stvarno identitet. Slično, $(\lambda x.y)s\to y[x:=s]=y$, što pokazuje da je $\lambda x.y$ konstantna funkcija.

Lambda račun se može predstaviti kao idealizovani funkcionalni program, kao što je Haskel ili Standard ML. Prema tome, beta redukcija odgovara matematičkom koraku. Ovaj korak može biti ponovljen u odgovarajućoj beta konverziji sve dok se ne istroše sve aplikacije. U netipskom lambda računu, kao što je ovde pokazano, ova redukcija se možda ne bi izvršila. Na primer, posmatrati izraz $\Omega =(\lambda x.xx)(\lambda x.xx)$. Here $(\lambda x.xx)(\lambda x.xx)\to (xx)[x:=\lambda x.xx]=(x[x:=\lambda x.xx])(x[x:=\lambda x.xx])=(\lambda x.xx)(\lambda x.xx)$. Izraz se uprošćava u jednoj beta redukciji, a samim tim se proces redukcije nikada neće izvršiti.

Drugi aspekt netipskog lambda računa je ta da ne pravi razliku između različitih dipova podataka. Na primer, može se tražiti da se napiše funkcija koja vrši određenu operaciju samo na brojeve. Međutim, u netipskom lambda računu, ne postoji način da se sačuva funkcija od primenjivanja istinitosnih vredonsti, stringova ili drugih objekata koji nisu brojevi.

Definicija

Lambda izrazi se sastoje od

• promenljivih v₁, v₂, ..., v_n, ...
• apstraktnih simbola labda 'λ' i tačke '.'
• zagrada ( )

Skup lambda izraza, Λ, mogu biti induktivno definisani:

1. Ako je x promenljiva, onda x ∈ Λ
2. Ako je h promenljiva i M ∈ Λ, onda (λx.M) ∈ Λ
3. Ako M, N ∈ Λ, onda (M N) ∈ Λ

Instance pravila 2 su poznate kao abrstrakcija a instance pravila 3 su poznate kao aplikacije

Oznaka

Da bi se zadržala oznaka lambda izraza, obično se primenjuju sledeće konvencije.

• Krajnje zagrade se odbacuju: M N umesto (M N)
• Pretpostavljeno je du su aplikacije asocijativne: M N P se može napisati kao ((M N) P)
• Telo abrstrakcije se proširuje koliko god je moguće: λx.M N znači λx.(M N) a ne znači (λx.M) N
• Niz apstrakcija je povezano: λx.λy.λz.N je skraćeno kao λxyz.N

Slobodne i ograničene promenljive

Za apstrakcioni operator, λ, se kaže da vezuje svoje promenljive kad god se pojave u telu apstrakcije. Promenljive koje spadaju u apstrakciju su ograničene . Sve ostale su slobodne. Na primer, u pratećim izrazima y je ograničena promenljiva a x slobodna: λy.x x y. Takođe se primećuje da je promenljiva ograničena "najbližom apstrakcijom". U sledećim primerima jedno pojavljivanje x u izrazima je ograničeno drugim lambda: λx.y (λx.z x)

Skup slobodnih promenljivih lambda izraza, M, je označen kao FV(M) i definisan je rekurzijom strukture izraza, kao što je dato:

1. FV(x) = {x}, gde je h promenljiva
2. FV(λx.M) = FV(M) \ {x}
3. FV(M N) = FV(M) ∪ FV(N)

Za izraze koji ne sadrže slobodne promenljive, kaže se da su zatvoreni. Zatvoreni lambda izrazi su takođe poznati i kao kombinacije i ekvivalentne su izrazima u kombinatoričkoj logici.

Redukcija

Značenje lambda izraza je definisano prema tome kako ti izrazi mogu biti redukovani.

Postoje tri tipa redukcija:

• α-konverzija: menjanje ograničenih promenljivih (alfa);
• β-redukcija: uzimanje funkcija za njihove argumente (beta);
• η-konverzija: koja obuhvata oznaku za ekstenzije (eta).

Govorili smo takođe o nastalim jednakostima : dva izraza su  β-ekvivalentna, ako se mogu β-konvertovati u isti izraz, takođe je i α/η-ekvivalencija definisana slično.

Termin redeks, skraćenica od uprostiti izraz, se odnosi na podtermine koji mogu biti redukovani uz pomoć jednog redukcionog praila. Na primer, (λx.M) N je beta-redeks za izražavanje zamene N za x in M; ako x nije slobodno u  M, λx.M x je eta-redeks. Izraz gde se primenjuje redeks redukcija; koristeći prethodni primer, uprosšćava date redom date izraze M[x:=N]i M.

α-konverzija

Alfa-konverzija, poznata i kao alfa-preimenovanje, dozvoljava promenu imena ograničenim promenljivim. Na primer, alfa-konverzija  λx.x glasi λy.y. Izrazi koji se razlikuju samo po alfa-konverziji se nazivaju a-ekvivalentno. Često, u korišćenju lambda računa, a-ekvivalentni izrazi se smatraju ekvivalentnim.

Precizna pravila za alfa-konverziju nisu baš jednostavna. Prvo, kada alfa-konvertuje apstrakciju, jedina promenljiva koja se pojavljuje  i koja je preimenovana je ta koja je ogranilena istom apstrakcijom. Na primer, alfa-konverzija  λx.λx.x  daje  λy.λx.x, ali ne daje λy.λx.y. Ovaj drugi primer daje drugačije značenje od originala.

Drugo, alfa-konverzija nije moguća ako će rezultat biti promenljiva koja je pod kontrolom druge apstrakcije . Na primer, ako zamenimo x sa y u λx.λy.x, dobijamo λy.λy.y, što nije isto.

U programima koji imaju statičko jezgro, alfa-konverzija se može koristiti da se napravi ime rezolucije jednostavnije obezbeđujući da ime promenljive maskira ime u odgovarajućem jezgru (videti alfa preimenovanje da se napravi trivijalna rezolucija

U De Bružinovoj indeksnoj oznaci, bilo koja dva alfa-ekvivalentna izraza su identična.

Zamena

Zamena, napisana kao E[V := R], je proces zamene svih bitnijih slučajeva promenljive V u izrazu E sa izrazom R. Substitucija izraza λ-računa je definisana na osnovu rekurzije struktura izraza, kao što je dato (primetiti: x i y su jedine promenljive dok su M i N bilo koji λ izrazi).

x[x := N]       ≡ N
y[x := N]       ≡ y, if x ≠ y
(M1 M2)[x := N] ≡ (M1[x := N]) (M2[x := N])
(λx.M)[x := N]  ≡ λx.M
(λy.M)[x := N]  ≡ λy.(M[x := N]), if x ≠ y, дефинисано y ∉ FV(N)

Da bi se transformisalo u lambda apstrakciju, ponekad treba α-konvertovati izraz. Na primer, nije tačno da (λx.y)[y := x] daje (λx.x), zato što je zamenjena vrednost x pretpostavljena da bude slobodna ali na kraju i ograničena. Ispravna zamena u ovom slučaju je (λz.x), sve do α-ekvivalencije. Primetiti da je zamena definisana unikatno do α-ekvivalencije.

β-redukcija

Beta-redukcija pamti ideju aplikacije funkcije. Beta-redukcija je definisana u okvirima zamene: beta-redukcija od((λV.E) E′) je  E[V := E′].

Na primer, pretpostavimo šivrovanje  2, 7, ×, imamo sledeću β-redukciju: ((λn.n×2) 7) → 7×2.

η-konverzija

Eta-konverzija izražava ideju ekstenzije, koja se u ovom kontekstu sastoji od dve funcije koje su iste ako i samo ako daju isti rezultat za sve argumente . Eta-konverzija konvertuje između λx.(f x) i f  kad god se x ne pojavljuje slobodno u f.

Normalne forme i ušće

Za netipski lambda račun, β-redukcija kao povratno pravilo, niti normalizuje snažno niti normalizuje slabo

Međutim, može se pokazati da je β-redukcija spojena. (Naravno, radimo do α-konverzije, tj. smatramo da su dve normalne forme jednake, ako je moguće da se α-konvertuje dualno.)

Dakle, oba snažno normalizujuća izraza i slabo normalizujuća izraza imaju unikatnu normalnu formu. Za snažne normalizujuće sisteme, bilo koja redukciona strategija garantuje pozivanje normalne forme, dok za slabo normalizujuće izraze, neke redukcione strategije se možda neće izvršiti.

Šifrovanje tipova podataka

Osnove lambda računa se mogu koristiti za istinitosne vrednosti, aritmetiku, strukture podataka i rekurziju, kao što je ilustrovano u narednim podeljcima.

Aritmetika u lambda računu

Postoji nekoliko mogućih načina da se definišu prirodni brojevi u lambda računu, ali u skoro većini slučajeva su Čerčovi brojevi, koji se mogu definisati kao:

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. Ili koristiti alternativnu sintaksu:

0 := λfx.x

1 := λfx.f x

2 := λfx.f (f x)

3 := λfx.f (f (f x))

Čerčova cifra je funkcija višeg reda—koja uzima jednu funkciju f, a vraća drugu funkciju. Čerčov broj n je funkcija koja uzima funkciju f kao argument i vraća n-tu kompoziciju f, tj. funkcija f se poziva sama n puta. Ovo je označeno sa f⁽ⁿ⁾ u odnosu n-ti stepen f (smatrati operatorom); f⁽⁰⁾ je definisana da bude identična funkcija. Takve ponovljene kompozicije (jedne funkcije f) poštuju zakone eskponata, zbog kojeg ovi brojevi mogu biti korišćeni u aritmetici. (U Čerčovom originalnom lambda računu, formalni parametar lambda izraza je bio morao da se pojavljuje barem jednom u telu funkcije, što čini ovu definiciju 0 nemogućom)

Možemo definisati nasleđenu funkciju , koja uzima broj n i vraća n + 1 dodajući drugu aplikaciju f, gde '(mf)x' znači da je funkcija 'f' primenjena 'm' puta na 'x':

SUCC := λn.λf.λx.f (n f x)

Zbog m-tog člana f upoređujući ga sa n-tim članom f daje m+n-ti član f, dodavanja se mogu definisati na sledeći način:

PLUS := λm.λn.λf.λx.m f (n f x)

PLUS se može smatrati kao funkcija koja uzima dva prirodna broja kao argumenta a vraća prirodan broj; može se predstaviti na sledeći način

PLUS 2 3

i

5

su β-ekvivalentni lambda izrazi. Dodavanje m broju n se može postići dodavanjem 1 m puta, ekvivalentna definicija je:

PLUS := λm.λn.m SUCC n 

Slično tome, množenje se definiše kao

MULT := λm.λn.λf.m (n f)

Alternativno

MULT := λm.λn.m (PLUS n) 0

umnožavanje m i n je isto što i ponavljanje dodate n funkcije m puta i pomnoženo 0. Eksponat je češće jedostavan vraćajući Čerčove brojeve, imenovane

POW := λb.λe.e b

Prethodna funkcija definisana PRED n = n − 1 za pozitivni celi broj n i PRED 0 = 0  je znatno više komplikovanija. Formula

PRED := λn.λf.λx.n (λg.λh.h (g f)) (λu.x) (λu.u)

može biti dokazana, pokazujući da ako je T označeno (λg.λh.h (g f)), onda je T⁽ⁿ⁾(λu.x) = (λh.h(f⁽ⁿ⁻¹⁾(x)))za n > 0. Dve postale definicije PRED su date ispod, jedna koristi uslove a druga koristeći parove. Sa prethodnom funkcijom, oduzimanje je jednostavno. Definisanje

SUB := λm.λn.n PRED m,

SUB m n poziva m − n kada je m > n i 0 drugačije.

Logika i iskazi

Konvencijom, sledeće dve definicije (poznata i kao Čerčova istinitosna vrednost) koje se koriste za određivanje istinitosne vrednosti TRUE(tačno) i FALSE(netačno):

TRUE := λx.λy.x

FALSE := λx.λy.y

(Primetiti da  FALSE ekvivalentno Čerčovom broju nula)

Zatim, sa ova dva λ-izraza, možemo definisati neke logičke operacije (ovo su samo moguće formulacije; ostali izrazi su ekvivalentno tačnii):

AND := λp.λq.p q p

OR := λp.λq.p p q

NOT := λp.λa.λb.p b a

IFTHENELSE := λp.λa.λb.p a b

Sada možemo da izralunamo logičke funkcije, npr. :

AND TRUE FALSE

≡ (λp.λq.p q p) TRUE FALSE →_β TRUE FALSE TRUE

≡ (λx.λy.x) FALSE TRUE →_β FALSE

vidimo da je AND(i) TRUE(tačno) FALSE(netačno) ekvivaletno  FALSE(netačnom).

Predikat je funkcija koja vraća istinitosnu vrednost. Najbitniji predikat je ISZERO(je nula), koji vraća TRUE(tačno)ako je argument Čerčov broj 0, a FALSE(netačno)ako je argument bilo koji drugi Čerčov broj:

ISZERO := λn.n (λx.FALSE) TRUE

Sledeći predikat testira da li je prvi argument manji ili jednak drugom:

LEQ := λm.λn.ISZERO (SUB m n),

i dok je m = n, ako LEQ m n i LEQ n m, onda je lako izgraditi predikat numeričke jednakosti.

Dostupnost predikata i definicije TRUE i FALSE čine ga željenim da se napišu "ako-onda-ili" izrazi u lambda računu. Na primer, prethodnik funkcije se može definisati kao:

PRED := λn.n (λg.λk.ISZERO (g 1) k (PLUS (g k) 1)) (λv.0) 0

što se može dokazati pokzujući induktivno da je n (λg.λk.ISZERO (g 1) k (PLUS (g k) 1)) (λv.0) dodata n − 1 funkcija za n > 0.

Parovi

Par (2-zagrade) se može definisati uz pomoć TRUE and FALSE, koristeći Čerčovo dešifrovanje za parove. Na primer, PAIR enkapsulira par (x,y), FIRST vraa prvi element tog para, dok SECOND vraća drugi.

PAIR := λx.λy.λf.f x y

FIRST := λp.p TRUE

SECOND := λp.p FALSE

NIL := λx.TRUE

NULL := λp.p (λx.λy.FALSE)

Linkovane liste se mogu definisati i kao NIL za praznu listu, ili PAIR(par) elementa i male liste. Pterpostavimo da NULL testira za vrednost  NIL(nula). (Alternativno, sa NIL := FALSE, konstrukcija l (λh.λt.λz.deal_with_head_h_and_tail_t) (deal_with_nil) uklanja potrebu za eksplicitnim NULL testom.

Kao primer korišćenja parova, funkcije promena i rasta koje mapiraju (m, n) do (n, n + 1) se može definisati kao

Φ := λx.PAIR (SECOND x) (SUCC (SECOND x))

Koji nam omogućava da dobijemo možda i najtransparentniju verziju prethodne funkcije

PRED := λn.FIRST (n Φ (PAIR 0 0)).

Rekurzija i fiksne tačke

Rekurzija je definica funkcije koja poziva sebe; lambda račun ne dozvoljava ovo (ne možemo odrediti vrednosti koja tek treba da se definiše, unutar lambda izraza definiše se ista vrednost, kao sve anonimne funkcije u lambda računu). Međutim, ovaj utisak vara: u (λx.x x) y  obe x‍ ‍ vrednosti se odnose na isti lambda izraz , y, pa je samim tim moguća za lambda izraz –ovde je y – napravljen tako da poziva sopstvenu vrednost, kroz svoju aplikaciju.

Rekurzivna instanca funkcije faktorijela F(n) je definisana kao

F(n) = 1, if n = 0; else n × F(n − 1).

U lambda izrazu koji je izabran da predstavlja tu funkciju, za parametar (uglavnom prvi) se pretpostavlja da prima svoj lambda izraz, a to se naziva-primati to kao argument- što će biti rekurzija. Ovako se dostiže rekurzija, namerno kao svoj referentni argument,  (koji se ovde naziva r) i mora uvek sebe da poziva u telu funkcije, tj. :

G := λr. λn.(1, if n = 0; else n × (r r (n−1)))

with  r r x = F x = G r x  to hold, so  r = G  and

F := G G = (λx.x x) G

Sopstvena-aplikacija postiže replikaciju ovde, prolazeći funkciju lambda izraza na sledeći poziv kao vrednosni argument, čineći to mogućim za referisanje i poziv.

Ovo rešava to ali podrazumeva ponovno pisanje svakog rekurzivnog poziv kao sopstvena-aplikacija. Voleli bismo da imamo generičko rešenje, bez potrebe ponovnog pisanja:

G := λr. λn.(1, if n = 0; else n × (r (n−1)))

with  r x = F x = G r x  to hold, so  r = G r =: FIX G  and

F := FIX G  where  FIX g := (r where r = g r) = g (FIX g)

so that  FIX G = G (FIX G) = (λn.(1, if n = 0; else n × ((FIX G) (n−1))))

Dati lambda izraz sa prvim argumentom predstavlja rekurzivni poziv ( označeno sa G),  kombinator fiksne tačke FIX će vratiti sopstvenu replikaciju lambda izraza predstavljajući rekurzivnu funkciju (ovde je to F). Funkcija ne mora proći samu sebe po svaku cenu, za sopstvenu replikaciju koja je napravljena u nastavku, kada se kreira, da bude izvršena svaki put kada se pozove. Originalan lambda izraz (FIX G)je ponovo napravljen u samom sebi, postižući sopstvenu referencu

Postoji mnogo različitih definicija za FIX operator, najjednostavniji je:

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

U lambda računu , Y g  je fiksirana tačka g, kao što je pokazano:

Y g

λh.((λx.h (x x)) (λx.h (x x))) g

(λx.g (x x)) (λx.g (x x))

g ((λx.g (x x)) (λx.g (x x)))

g (Y g)

Sada, da bismo izveli naš rekurzivni poziv funkcije faktorijela, jednostavno ćemo pozvati (Y G) n, gde je n broj čiji faktorijel izračunavamo. Dodelimo npr. vrednost  n = 4, što daje:

(Y G) 4

G (Y G) 4

(λr.λn.(1, if n = 0; else n × (r (n−1)))) (Y G) 4

(λn.(1, if n = 0; else n × ((Y G) (n−1)))) 4

1, if 4 = 0; else 4 × ((Y G) (4−1))

4 × (G (Y G) (4−1))

4 × ((λn.(1, if n = 0; else n × ((Y G) (n−1)))) (4−1))

4 × (1, if 3 = 0; else 3 × ((Y G) (3−1)))

4 × (3 × (G (Y G) (3−1)))

4 × (3 × ((λn.(1, if n = 0; else n × ((Y G) (n−1)))) (3−1)))

4 × (3 × (1, if 2 = 0; else 2 × ((Y G) (2−1))))

4 × (3 × (2 × (G (Y G) (2−1))))

4 × (3 × (2 × ((λn.(1, if n = 0; else n × ((Y G) (n−1)))) (2−1))))

4 × (3 × (2 × (1, if 1 = 0; else 1 × ((Y G) (1−1)))))

4 × (3 × (2 × (1 × (G (Y G) (1−1)))))

4 × (3 × (2 × (1 × ((λn.(1, if n = 0; else n × ((Y G) (n−1)))) (1−1)))))

4 × (3 × (2 × (1 × (1, if 0 = 0; else 0 × ((Y G) (0−1))))))

4 × (3 × (2 × (1 × (1))))

24

Svaka rekurzivno definisana funkcija može biti predstavljena kao fiksirana tačka neke odgovarajuće definisane funkcije zatvarajući rekurzivni poziv sa ekstra argumentom Y, svaka rekurzivno definisana funkcija se može izraziti kao lambda izraz. Praktično, mi možemo jasno definisati oduzimanje, množenje i poređenje predikata prirodnih brojeva rekurzivno.

Standardni izrazi

Sledeći izrazi obično prihvataju imena:

I := λx.x

K := λx.λy.x

S := λx.λy.λz.x z (y z)

B := λx.λy.λz.x (y z)

C := λx.λy.λz.x z y

W := λx.λy.x y y

U := λx.λy.y (x x y)

ω := λx.x x

Ω := ω ω

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

Tipski lambda račun

Tipski lambda račun je tipski formalizam koji koristi lambda simbol ($\lambda$) da označi nepoznatu apstrakciju funkcije. U ovom kontekstu, tipovi su obično objekti sintetičke prirode koji su dodeljeni lambda izrazima; egzaktna priroda tipova zavisi od izračunavanja računa (videti vrste u nastavku) . Sa određene tačke gledišta, tipski lambda račun se može predstaviti kao usavršavanje netipskog lambda računa ali sa druge tačke gledišta, oni oni se takođe mogu smatrati više fundamentalnom teorijom i netipski lambda račun je specijalni slučaj sa samo jednim tipom.

Tipski lambda račun je osnivač programskih jezika i on predstavlja bazu funkcionalnih programskih jezika kao što su ML i Haskel i, više indirektni, tipski imperativni programski jezici. Tipski lambda račun ima veoma važnu ulogu u dizajnu tipskih sistema za programske jezike; ovde određivanje tipa obično označava poželjne karakteristike programa, npr. program neće naštetiti pristup memoriji

Tipski lambda račun je usko povezan sa matematičkom logikom i otpornom teorijom sa Kari-Hauradovim izomorfizmom i oni se mogu smatrati kao interni programi sačinjeni od klasa kategorija, npr. jednostavan tipski lambda račun je program Dekartove zatvorene kategorije (Dzk).

Izračunive funkcije i lambda račun

Funkcija F: N → N prirodnih brojeva je izračuniva ako i sako ako postoji lambda izraz  f takav da za svaki par x, y u N, F(x)=y i ako i samo ako je f x =_β y, gde su x i y Čerčovi odgovarajući brojevi za x i y, odnosno i =_β predstavlja ekvivalenciju za beta redukciju. Ovo je jedan od mnogo načina da se definiše izračunjivost; videti Čerč-Tjuringova teza za diskusiju o drugim proračunima i njihovim jednakostima.

Nesigurnost ekvivalencije

Ne postoji algoritam koji uzima kao ulazne podatke dva lambda izraza i vraća TRUE or FALSE u zavisnosti od toga da li su ta dva izraza ekvivalentna ili nisu. Istorijski gledano, ovo je prvi problem čija se nesigurnost mogla dokazati. Kao i kod dokazane nesigurnosti , dokaz pokazuje da ni jedna računiva funkcija ne može da određuje ekvivalenciju. Čerč-Tjuringova teza je uvedena da pokaže da ne postoji algoritam koji ovo radi.

Čerčov dokaz je prvi uprostio problem određivanja gde lambda izraz ima normalnu formu. Normalna forma je ekvivalentna irazu koji se ne može uprostiti ispod pravila koji su uslovljeni pravilom. On sumnja da je ovaj iskaz računiv, i da se mođe predstaviti preko lambda računa. Nadograđujući se na posao koji je odradio Klin, konstruktujući Gedelovo brojanje za lambda izrazem, on je osmislio lambda izraz e koji striktno prati dokaz Gedelove teoreme o nepotpunosti . Ako se e primenjuje na sopstveni Gedelov broj, rezultat je kontradikcija. 

Lambda račun i programski jezici

Kao što je određeno od strane Pitera Landina 1965. korespondencija između Algola 60 i Čerčove Lambda notacije, sekvencijalno proceduralni programi mogu da razumeju izraze lambda računa, koji pružaju osnovne mehanizme za proceduralnu apstrakciju i proceduru (potprogram) aplikacije.

Lambda račun čini "funkcije" povezanijim i čini ih objektima prve klase što utiče na porast kompleksnosti implementacije kada bude izvršena. 

Anonimna funkcija

Na primer, u Lisp-u kvadratna funkcije se može predstaviti kao lambda račun, kao:

(lambda (x) (* x x))

Dati primer je izraz koji pripada prvoj klasi funkcija. Simbol lambda kreira anonimnu funkciju, date liste imena parametra, (x) — samo jedan argument u ovom slučaju, i izraz koji je predstavljen kao telo funkcije , (* x x). Haskelov primer je identičan. Anonimne funkcije se ponekad zovu lambda izrazima

Na primer, Paskal i mnogo ostalih imperativnih programa je dugo podržavalo prelazak preko potprograma, kao argumente za druge potprograme kroz mehanizam izvršilaca funkcije. Međutim, izvršioci programa nisu dovoljan uslov za funkcije da budu tipovi prve klase, zato što je funkcija tip podataka prve klase ako i samo ako nova instanca funkcije može biti kreirana u brzom vremenu. U ovom brzom vremenu kreiranje funkcija je podržano u Smalltalku, Javaskripti, i češće u Skali, Ajfelu ("agenti", C# ("delegacija" i C++11, i mnogi drugi.

Strategija uprošćavanja

Bez obzira na to da li se izraz normalizuje ili ne, i koliko mu treba da se izrši u normalizaciji toga, izraz zavisi u velikoj meri od korišćene strategije uprošćavanja. Razlika između redukcionih strategija zavisi od razlike u funkcionalnom programskom jeziku između poželjne procene i nepoželjne procene.

Potpuna beta redukcija

Bilo kakva redukcija se može redukovati bilo kad. Ovo znači da u suštini odsustvo bilo koje praktične redukcione strategije-koja je usko povezana sa redukcijom , "pada u vodu".

Aplikativni red

Srkoz levo, po dubini se prvo izvršava redukcija. Intuitivno ovo znači da se uvek prvo uprošćavaju argumenti funkcije pre same funkcije. Aplikativni red uvek pokušava da prihvati funkciju u normalnom obliku, čak i kada to nije moguće. Mnogi programski jezici (kao što su Lisp, ML, i imperativni jezici kao što su C i Java)su opisani kao "striktni", misleći da su funkcije primljene od strane ne normalizujućih argumenata, ne normalizujuće. Ovo je urađeno koristeći aplikativni red, a naziva se vrednosno uprošćavanje, ili češće "željena evolucija".

Normalni red

Skroz levo, se prvo redukuje po krajevima. Kad god je moguće, argumenti se zamenjuju u telo abrstrakcije pre nego što su argumenti uprošćeni.

Poziv po imenu

Kao normalni red, ali bez redukcionih performansi unutar apstrakcija. Na primer, λx.(λx.x)x je normalna forma prema ovoj strategiji, iako sadrži redeks  (λx.x)x.

Poziv po vrednosti

Samo krajevi redeksa se uprošćavaj; redeks je uprošćen samo ako je desna strana podložna redukciji (promenljiva ili lambda apstrakcija).

Poziv po potrebi

Kao normalni red, ali aplikacije funkcija će udvostručiti izraze umesto imena argumenata, koji su zatim redukuju samo " kada je to potrebno". Nazvano u praktičnom smislu "lenja procena". U implementacijama ovo "ime" uzima formu izvršioca, sa redeksom predstavljenim uz pomoć uzvika.

Aplikativni izraz nije normalizovano osmišljen. Česti protivprimer je: definisati Ω = ωω gde je ω = λx.xx. Ceo ovaj izraz sadrži samo jedan redeks, koji imenuje celi izraz; redukuje se ponovo Ω. Kako je ovo jedina moguća redukcija, Ω nema normalnu formu (ispod svake procene strategije). Koristeći aplikativni red, izraz KIΩ = (λx.λy.x) (λx.x)Ω je redukovan od strane prve redukcije Ω do normalne forme (dok je redeks skroz desno ), ali dok Ω nema normalnu formu, aplikativni red ne može da nađe normalnu formu za KIΩ.

U suprotnosti, normalni red se tako naziva zato što uvek nađe normalizujuću redukciju. U navedenom primeru, KIΩ se redkuje iz normalnog reda do I, normalne forme. Nedostatak se ogleda u tome što redeksi u argumentima mogu biti koopirani, što dovodi do dupliranog izračunavanja (npr. , (λx.xx) ((λx.x)y) se redukuje dp ((λx.x)y) ((λx.x)y) koristeći ovu strategiju; sada postoje dva redeksa, pa celokupna procena mora da ima još dva koraka, ali ako su argumenti prvo redukovani, tada će neće postojati ništa).

Pozitivni dogovor korišćenja aplikativnog izraza se ogleda u tome što ne izaziva nepotrebno računanj, ako su svi argumenti korišćeni, zbog toha što se nikada ne zamenjuju argumenti koji sadrže redeks i zbog toga ih ne treba nikada kopirati (što može da duplira posao). U gornjem primeru, u aplikacionom izrazu (λx.xx) ((λx.x)y) se redukuje prvo do(λx.xx)y a zatim do normalnog izraza yy, uzimajući dva koraka umesto da uzme tri izraza.

Većina čistih funkcionalnih programskih jezika (posebno Miranda i njegovi prethodnici, uključujući Haskel), i dokazanih programskih jezika teoreme provere, koriste lenju procenu pto je u suštini isto ka i poziv po potrebi. Ove je slično normalnoj redukciji, ali poziv po potrebi uspeva da izbegne duplianje posla inherentno u normalnoj redukciji koristeći deljenje . U gore navedenom primeru, (λx.xx) ((λx.x)y) se redukuje do ((λx.x)y) ((λx.x)y), što sadrži dva redeksa, ali u pozivu po potrebi oni su predstavljeni tako da koriste isti objekat češće nego kopirani, pa kada je jedan redukovan, samim tim je i drugi redukovan.

Napomena o složenosti

Dok je ideja beta redukcije izgledala dovoljno jednostavno, ona ipak nije atomski korak, u smislu da mora da ima komplikovanu strukturu pri proceni računarske složenosti. Precizno, jedna mora nekako da pronađe lokaciju svih ograničenih pojava promenljive V  u izrazu E, što dovodi do trošenja vremena, ili jedna mora da vodi evidenciju lokacija V u izrazu E, što takođe dovodi do trošenja vremena. Naivna pretraga lokacije V u izrazu E je O(n) u dužini n od E. Ovo dovodi do proučavanja sistema koji koriste eksplicitnu zamenu. Sinotov upravljač stringovima  nudi način snimanja lokacija slobodnih varijabli u izrazima.

Paralelizam i slaganje

Čerč-Roserova osobina u lambda računu znači da procena (β-redukcija) može biti izbačena u bilo kom redosledu, čak i u paraleli. Ovo znači da je promenljiva nedeterministička procena strategija bitna. Međutim, lambda račun ne nudi bilo kakvu eksplicitnu konstrukciju za paralelnu obradu. Jedan može dodati konstrukciju kao karakteristiku za lambda račun. Drugi proces računanja je razbi

Semantika

Činjenica, da se izrazi lambda računa ponašaju kao funkcije na ostale lambda izraze, pa čak i na same sebe, dovela je do pitanja o semantici lambda računa . Da li se mogu razumna značenja dodelti izrazima lambda računa? Priroda semantike je je da nađe skupove D izomorfne funkcionalnom prostoru D → D, funkcije na samu sebe. Međutim, komplikovano postojanje D, uz pomoć kardinalnog ograničenja zato što skup svih funkcija iz  D do D ima veću kardinalnost nego D, osim ako je D samostalno.

U 1970-im, Dejna Skot je pokazako da, ako se posmatraju samo neprekidne funkcije, skup ili domen D sa potrebnim osobinama se može naći, praveći tako model lambda računa.

Ovo je stvorilo osnovu za semantiku sistema zakona programskih jezika.

Literatura

• Turbak, Franklyn; Gifford, David (2008). Design concepts in programming languages. MIT press. str. 251. ISBN 978-0-262-20175-9. 
• Bunt, Harry; Muskens, Reinhard (2008). Computing Meaning. Springer Science & Business Media. ISBN 978-1-4020-5957-5. 
• Moortgat, Michael (1988). Categorial Investigations: Logical and Linguistic Aspects of the Lambek Calculus. Walter de Gruyter. ISBN 978-90-6765-387-9. 
• Mitchell, John C. (2003). Concepts in Programming Languages. Cambridge University Press. str. 57. ISBN 978-0-521-78098-8.