Tipizirani lambda račun

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

Tradicionalno, tipizirani lambda računi su shvaćeni kao rafiniranja 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 tipiziranog lambda računa su samo bazni tipovi (ili varijable tipa) i funkcijski tipovi [math]\displaystyle{ \sigma\to\tau }[/math]. Sustav T proširuje jednostavno tipiziran lambda račun tipom prirodnih brojeva i primitivnom rekurzijom višeg reda - u ovom su sustavu sve funkcije dokažljivo rekurzivne u 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 logici drugog reda. Lambda računi sa ovisnim tipovima su osnova intuicionističke teorije tipa, računa konstrukcija i logičkog okvira (LF - logical framework), čistog lambda računa sa ovisnim tipovima. Na osnovu rada Berardija, Barendregt je predložio 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 podtipiziranja, tj. ako je [math]\displaystyle{ A }[/math] podtip od [math]\displaystyle{ B }[/math], tada svi termini tipa [math]\displaystyle{ A }[/math] imaju i tip [math]\displaystyle{ B }[/math]. Tipizirani lambda računi sa podtipiziranjem su jednostavno tipizirani lambda račun sa konujnktivnim tipovima i [math]\displaystyle{ F^\leq }[/math] (F-sub).

Svi sustavi dosad spomenuti, sa 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 sa tipom svih tipova (Tip : Tip) nije normalizirajući zbog Girardova paradoksa. Ovaj je sustav ujedno i najjednostavniji čisti sustav tipa, formalizam koji poopćuje lambda kocku. Sustavi sa eksplicitnim kombinatorima rekurzije, kao što je 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 programiranju, rutine (funkcije, procedure, metode) strogo tipiziranih programskih jezika usko odgovaraju tipiziranim lambda izrazima. 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.