Vidi kôd stranice Tipizirani lambda račun

'''Tipizirani lambda račun''' je tip formalizma koji koristi simbol lambda (<math>\lambda</math>) za označavanje apstrakcije anonimne funkcije. Tipizirani lambda računi su [[programski jezik|programski jezici]] i pružaju osnovu za tipizirane [[funkcijski programski jezik|funkcijske programske jezike]] kao što su [[ML (programski jezik)|ML]] i [[Haskell (programski jezik)|Haskell]] te i, neizravno, tipizirane [[imperativno programiranje|imperativne programske jezike]]. Usko su povezani s [[intuicionistička logika|intuicionističkom logikom]] preko [[Curry-Howard izomorfizam|Curry-Howard izomorfizma]] i mogu se smatrati internim jezikom klasa [[teorija kategorija|kategorija]], npr. jednostavno tipizirani lambda račun je jezik [[kartezijanski zatvorena kategorija|kartezijanski zatvorenih kategorija]] (CCC-ova).

Tradicionalno, tipizirani lambda računi su shvaćeni kao rafiniranja [[netipizirani lambda račun|netipiziranog lambda računa]]. Suvremenije gledište smatra tipizirane lambda račune fundamentalnijom teorijom, i [[netipizirani lambda račun]] posebnim slučajem sa samo jednim tipom.

Razni tipizirani lambda računi su proučavani: tipovi [[jednostavno tipizirani lambda račun|jednostavno tipiziranog lambda računa]] su samo bazni tipovi (ili varijable tipa) i funkcijski tipovi <math>\sigma\to\tau</math>. [[Sustav T]] proširuje jednostavno tipiziran lambda račun tipom [[Prirodni broj|prirodnih brojeva]] i primitivnom rekurzijom višeg reda - u ovom su sustavu sve funkcije dokažljivo rekurzivne u [[Peanova aritmetika|Peanovoj aritmetici]] definabilne. [[Sustav F]] dozvoljava polimorfizam koristeći univerzalnu kvantifikaciju nad svim tipovima - iz logičke perspektive može opisati sve funkcije koje su dokažljivo totalne u [[logika drugog reda|logici drugog reda]]. Lambda računi s [[ovisni tip|ovisnim tipovima]] su osnova [[intucionistička teorija tipa|intuicionističke teorije tipa]], [[račun konstrukcija|računa konstrukcija]] i [[LO (logički okvir)|logičkog okvira]] (LF - ''logical framework''), čistog lambda računa s ovisnim tipovima. Na osnovu rada Berardija, [[Barendregt]] je predložio [[lambda kocka|lambda kocku]] za sistematiziranje relacija čistog tipiziranog lambda računa (uključujući jednostavno tipiziran lambda račun, Sustav F, LF i račun konstrukcija).

Neki jednostavno tipizirani lambda račun uvode pojam ''[[podtip]]iziranja'', tj. ako je <math>A</math> podtip od <math>B</math>, tada svi termini tipa <math>A</math> imaju i tip <math>B</math>. Tipizirani lambda računi s podtipiziranjem su jednostavno tipizirani lambda račun s konujnktivnim tipovima i <math>F^\leq</math> (''F-sub'').

Svi sustavi dosad spomenuti, s iznimkom netipiziranog lambda računa, su ''strogo normalizirajući'': sva računanja terminiraju. Kao posljedica toga su konzistentni kao logika, tj. postoje nenaseljeni tipovi. Postoje, međutim, tipizirani lambda računi koji nisu strogo normalizirajući. Primjerice ovisno tipizirani lambda račun s tipom svih tipova (Tip : Tip) nije normalizirajući zbog [[Girardov paradoks|Girardova paradoksa]]. Ovaj je sustav ujedno i najjednostavniji [[čisti sustav tipa]], formalizam koji poopćuje [[lambda kocka|lambda kocku]]. Sustavi s eksplicitnim kombinatorima [[Rekurzija|rekurzije]], kao što je [[Gordon Plotkin|Plotkinov]] PCF, nisu normalizirajući, ali nisu ni namijenjeni da budu interpretirani kao logika. Uistinu, PCF (stoji za engl. ''Partially Computable Functions'' - parcijalno izračunljive funkcije) je prototipni tipizirani funkcijski programski jezik, pri čemu se tipovi koriste kako bi se osiguralo dobro ponašanje programa, no ne nužno i terminacija.

Tipizirani lambda računi igraju važnu ulogu u dizajnu novih sustava tipa za programske jezike - tu tipiziranost obično služi za obuhvaćanje poželjnih svojstava programa, npr. da program neće uzrokovati nedozvoljen pristup memoriji.

U [[programiranje|programiranju]], rutine (funkcije, procedure, metode) [[strogo tipiziran programski jezik|strogo tipiziranih programskih jezika]] usko odgovaraju tipiziranim lambda izrazima. [[Eiffel (programski jezik)|Eiffel]] posjeduje pojam "inline agenta" koji omogućava izravno definiranje i manipuliranje lambda izrazima, kroz izraze kao što je '''agent''' (O: OSOBA): STRING '''do Rezultat''' := o.supruznik.ime '''end''', označujući objekt koji predstavlja funkciju koja vraća ime osobinog supružnika.
[[Kategorija:Lambda račun]]
[[Kategorija:Teorija računanja]]