WikiSysop: Bot: Automatski unos stranica

2021-08-23T03:38:32Z

Bot: Automatski unos stranica

Nova stranica

'''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 sa [[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 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 sa [[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 sa 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 sa podtipiziranjem su jednostavno tipizirani lambda račun sa konujnktivnim tipovima i <math>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 [[Girardov paradoks|Girardova paradoksa]]. Ovaj je sustav ujedno i najjednostavniji [[čisti sustav tipa]], formalizam koji poopćuje [[lambda kocka|lambda kocku]]. Sustavi sa eksplicitnim kombinatorima 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]]

Tipizirani lambda račun - Povijest promjena

WikiSysop: Bot: Automatski unos stranica