Tipizirani lambda račun

Izvor: Wikipedija

Tipizirani lambda račun je tip formalizma koji koristi simbol lambda () 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 s 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 . 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 s ovisnim tipovima su osnova intuicionističke teorije tipa, računa konstrukcija i logičkog okvira (LF - logical framework), čistog lambda računa s 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 podtip od , tada svi termini tipa imaju i tip . Tipizirani lambda računi s podtipiziranjem su jednostavno tipizirani lambda račun s konujnktivnim tipovima i (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 Girardova paradoksa. Ovaj je sustav ujedno i najjednostavniji čisti sustav tipa, formalizam koji poopćuje lambda kocku. Sustavi s 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.