Kalkulasi ya Lambda ni mfumo rasmi katika mantiki ya hisabati kwa ajili ya kueleza hesabu zenye msingi wa uchukuaji na kutumia vitendakazi kwa kutumia uwekaji wa kuunganisha na kutofautisha. Huu ni mfano wa ulimwengu wote ambao unaweza kutumika kwa muundo wa mashine yoyote ya Turing. Kalkulasi ya lambda ilianzishwa kwa mara ya kwanza na Kanisa, mwanahisabati maarufu, katika miaka ya 1930.
Mfumo huu unajumuisha kujenga wanachama wa lambda na kufanya shughuli za kupunguza juu yao.
Maelezo na Maombi
Herufi ya Kigiriki lambda (λ) inatumika katika misemo ya lambda na istilahi za lambda ili kuashiria ufungaji wa kigezo katika chaguo la kukokotoa.
Kalkulasi ya Lambda inaweza kubatilishwa au kuandikwa. Katika toleo la kwanza, chaguo za kukokotoa zinaweza kutumika tu ikiwa zina uwezo wa kupokea data ya aina hii. Chapa lambda calculi ni dhaifu, inaweza kueleza thamani ndogo. Lakini, kwa upande mwingine, wanakuruhusu kuthibitisha mambo zaidi.
Sababu moja ya kuwepo kwa aina nyingi tofauti ni hamu ya wanasayansi kufanya zaidi bila kuacha nafasi ya kuthibitisha nadharia kali za calculus za lambda.
Mfumo una matumizi katika maeneo mengi tofauti ya hisabati, falsafa, isimu na sayansi ya kompyuta. Kwanza kabisa, calculus lambda ni calculus ambayo imekuwa na jukumu muhimu katika maendeleo ya nadharia ya lugha za programu. Ni mitindo ya uundaji wa kazi ambayo mifumo inatekelezwa. Pia ni mada motomoto ya utafiti katika nadharia ya kategoria hizi.
Kwa ajili ya dummies
Kalkulasi ya lambda ilianzishwa na mwanahisabati Alonzo Church katika miaka ya 1930 kama sehemu ya utafiti wake katika misingi ya sayansi. Mfumo asilia ulionyeshwa kuwa hauendani kimantiki mwaka wa 1935 wakati Stephen Kleen na J. B. Rosser walipoanzisha kitendawili cha Kleene-Rosser.
Baadaye, mnamo 1936, Kanisa lilitenga na kuchapisha tu sehemu ambayo ni muhimu kwa hesabu, kile ambacho sasa kinaitwa calculus ya lambda isiyochapishwa. Mnamo 1940 pia alianzisha nadharia dhaifu lakini thabiti inayojulikana kama mfumo wa aina kuu. Katika kazi yake, anaeleza nadharia nzima kwa maneno rahisi, hivyo inaweza kusemwa kwamba Kanisa lilichapisha calculus lambda kwa ajili ya dummies.
Hadi miaka ya 1960, wakati uhusiano wake na lugha za utayarishaji ulipodhihirika, λ ilikuwa urasmi tu. Shukrani kwa matumizi ya Richard Montagu na wanaisimu wengine katika semantiki ya lugha asilia, calculus imejivunia nafasi katika isimu na sayansi ya kompyuta.
Asili ya ishara
Lambda haimaanishi neno au kifupi, inatoka kwa marejeleo katika Hisabati Mkuu ya Russell ikifuatiwa na mabadiliko mawili ya uchapaji. Mfano wa nukuu: kwa chaguo za kukokotoa f yenye f (y)=2y + 1 ni 2ŷ + 1. Na hapa tunatumia caret ("kofia") juu ya y kuweka lebo ya kibadilishaji cha ingizo.
Hapo awali kanisa lilinuia kutumia alama sawa, lakini watayarishaji wa kupanga hawakuweza kuweka alama ya "kofia" juu ya herufi. Kwa hivyo badala yake waliichapisha awali kama "/\y.2y+1". Katika kipindi kilichofuata cha kuhariri, wachapaji walibadilisha "/ \" na herufi inayofanana.
Utangulizi wa calculus lambda
Mfumo unajumuisha lugha ya istilahi, ambayo huchaguliwa kwa sintaksia fulani rasmi, na seti ya sheria za mabadiliko zinazoruhusu kubadilishwa. Hoja ya mwisho inaweza kuzingatiwa kama nadharia ya usawa au ufafanuzi wa kiutendaji.
Vitendaji vyote katika kalkulasi ya lambda hazijulikani majina, kumaanisha kwamba hazina majina. Zinachukua kigezo kimoja tu, na uchakataji hutumika kutekeleza njama zilizo na anuwai nyingi.
Masharti ya Lambda
Sintaksia ya calculus inafafanua baadhi ya vielezi kuwa halali na vingine kuwa batili. Kama vile safu tofauti za herufi ni programu halali za C na zingine sio. Usemi halisi wa calculus lambda unaitwa "neno lambda".
Sheria tatu zifuatazo hutoa ufafanuzi wa kufata neno ambao unaweza kuwainatumika kwa ujenzi wa dhana zote halali za kisintaksia:
Kigeuzi cha x chenyewe ni neno halali lambda:
- ikiwa T ni LT na x haitumiki mara kwa mara, basi (lambda xt) inaitwa uondoaji.
- ikiwa T pamoja na s ni dhana, basi (TS) inaitwa matumizi.
Hakuna kingine ni neno lambda. Kwa hivyo, dhana ni halali ikiwa tu inaweza kupatikana kwa matumizi ya mara kwa mara ya sheria hizi tatu. Hata hivyo, baadhi ya mabano yanaweza kuachwa kulingana na vigezo vingine.
Ufafanuzi
Semi za Lambda zinajumuisha:
- vigezo v 1, v 2, …, v n, …
- ishara za uondoaji 'λ' na nukta '.'
- mabano ().
Seti Λ inaweza kuelezwa kwa kufata neno:
- Kama x ni kigezo, basi x ∈ Λ;
- x haibadiliki na M ∈ Λ, kisha (λx. M) ∈ Λ;
- M, N ∈ Λ, kisha (MN) ∈ Λ.
Maudhui
Ili kuweka nukuu ya misemo ya lambda bila kuchanganywa, kanuni zifuatazo hutumiwa kwa kawaida:
- Mabano ya nje yameachwa: MN badala ya (MN).
- Maombi yanachukuliwa kuwa ya ushirika: mtu anaweza kuandika MNP badala ya ((MN) P).
- Sehemu ya uondoaji inaenea zaidi hadi kulia: λx. MN ina maana λx. (MN), si (λx. M) N.
- Msururu wa uondoaji umepunguzwa: λx.λy.λz. N inaweza kuwa λxyz. N.
Vigezo visivyolipishwa na vilivyofungwa
Opereta λ inaunganisha isiyo ya kudumu popote ilipo katika sehemu ya uondoaji. Vigezo vinavyoanguka katika upeo huitwa kufungwa. Katika usemi λ x. M, sehemu ya λ x mara nyingi hurejelewa kama kiunganishi. Kana kwamba inadokeza kwamba viambajengo vinakuwa kikundi kwa kuongezwa kwa X x hadi M. Zingine zote zisizo imara huitwa bure.
Kwa mfano, katika usemi λ y. x x y, y - imefungwa isiyo ya kudumu, na x - bila malipo. Na pia inafaa kuzingatia kuwa kutofautisha kumewekwa kwa uondoaji wake wa "karibu". Katika mfano ufuatao, suluhisho la calculus lambda linawakilishwa na tukio moja la x, ambalo linahusiana na neno la pili:
λ x. y (λ x. z x)
Seti ya vigeu visivyolipishwa M hufafanuliwa kama FV (M) na hufafanuliwa kwa kujirudia kwa muundo wa maneno kama ifuatavyo:
- FV (x)={x}, ambapo x ni kigezo.
- FV (λx. M)=FV (M) {x}.
- FV (MN)=FV (M) ∪ FV (N).
Mchanganyiko ambao hauna vigeu visivyolipishwa huitwa kufungwa. Semi funge za lambda pia hujulikana kama viunganishi na ni sawa na istilahi katika mantiki ya mchanganyiko.
Ufupisho
Maana ya misemo ya lambda hubainishwa na jinsi yanavyoweza kufupishwa.
Kuna aina tatu za mikato:
- α-badilisha: kubadilisha vigeu vilivyofungamana (alpha).
- β-kupunguza: kutumia vitendakazi kwenye hoja zao (beta).
- η-transform: inashughulikia dhana ya upanuzi.
Hii hapa piatunazungumza kuhusu usawa unaotokana: misemo miwili ni β-sawa ikiwa inaweza kubadilishwa β hadi sehemu moja, na α / η-usawa hufafanuliwa vile vile.
Neno redex, fupi kwa mauzo inayoweza kupunguzwa, hurejelea mada ndogo zinazoweza kupunguzwa kwa mojawapo ya sheria. Mahesabu ya Lambda ya dummies, mifano:
(λ x. M) N ni redex ya beta katika usemi wa kubadilisha N na x katika M. Kijenzi ambacho redex hupunguza huitwa upunguzaji wake. Kupunguzwa (λ x. M) N ni M [x:=N].
Kama x si bure katika M, λ x. M x pia em-REDEX yenye kidhibiti M.
α-mabadiliko
Majina ya alfa hukuruhusu kubadilisha majina ya vigeu vilivyounganishwa. Kwa mfano, x. x anaweza kutoa λ y. y. Masharti ambayo yanatofautiana katika ubadilishaji wa alpha pekee yanasemekana kuwa α-sawa. Mara nyingi, unapotumia calculus ya lambda, α-sawa huchukuliwa kuwa sawa.
Sheria kamili za ubadilishaji wa alpha sio ndogo kabisa. Kwanza, kwa uondoaji huu, ni vigezo tu vinavyohusishwa na mfumo huo huo vinaitwa jina. Kwa mfano, alfa kubadilisha λ x.λ x. x inaweza kusababisha λ y.λ x. x, lakini hii inaweza isielekeze kwa λy.λx.y Mwisho una maana tofauti na asilia. Hii ni sawa na dhana ya upangaji vivuli tofauti.
Pili, ubadilishaji wa alpha hauwezekani ikiwa ungesababisha kunaswa na muhtasari mwingine usio wa kudumu. Kwa mfano, ukibadilisha x na y katika λ x.λ y. x, basi unaweza kupataλy.λy. u, ambayo si sawa hata kidogo.
Katika lugha za kupanga zenye upeo tuli, ubadilishaji wa alpha unaweza kutumika kurahisisha utatuzi wa jina. Wakati huo huo, kuwa mwangalifu kwamba dhana ya kigezo haifichi uainisho katika eneo lililo na maudhui.
Katika nukuu ya faharasa ya De Bruyne, istilahi zozote mbili zinazolingana na alfa zinafanana kisintaksia.
Badiliko
Mabadiliko yaliyoandikwa na E [V:=R] ni mchakato wa kubadilisha matukio yote yasiyolipishwa ya tofauti V katika usemi E na mauzo R. Ubadilishaji katika masharti ya λ hufafanuliwa na lambda ya kujirudia. calculus kwenye muundo wa dhana kama ifuatavyo (kumbuka: x na y - viambajengo pekee, na M na N - usemi wowote wa λ).
x [x:=N] ≡ N
y [x:=N] ≡ y ikiwa x ≠ y
(M 1 M 2) [x:=N] ≡ (M 1 [x:=N]) (M 2 [x:=N])
(λ x. M) [x:=N] ≡ λ x. M
(λ y. M) [x:=N] y λ y. (M [x:=N]) ikiwa x ≠ y, mradi y ∉ FV (N).
Ili badala ya ufupisho wa lambda, wakati mwingine ni muhimu α-kubadilisha usemi. Kwa mfano, si kweli kwamba (λ x. Y) [y:=x] husababisha (λ x. X) kwa sababu x iliyobadilishwa ilipaswa kuwa huru, lakini ikaishia kufungwa. Uingizwaji sahihi katika kesi hii ni (λ z. X) hadi α-sawa. Kumbuka kuwa uingizwaji umefafanuliwa kipekee hadi lambda.
β-kupunguza
Kupunguza kwa Beta kunaonyesha wazo la kutumia chaguo la kukokotoa. Beta-reductive inafafanuliwa katika mashartibadala: ((X V. E) E ') ni E [V:=E'].
Kwa mfano, tukichukulia baadhi ya usimbaji 2, 7, ×, kuna upunguzaji wa β ufuatao: ((λ n. N × 2) 7) → 7 × 2.
Kupunguza Beta kunaweza kuonekana kuwa sawa na dhana ya upunguzaji wa ndani chini ya ukato wa asili kupitia isomorphism ya Curry-Howard.
η-mabadiliko
Uongofu huu unaonyesha wazo la upanuzi, ambalo katika muktadha huu ni kwamba kazi mbili ni sawa zinapotoa matokeo sawa kwa hoja zote. Ubadilishaji huu wa ubadilishaji kati ya λ x. (F x) na f wakati wowote x haionekani kuwa huru katika f.
Kitendo hiki kinaweza kuchukuliwa kuwa sawa na dhana ya ukamilifu wa ndani katika ukato wa asili kupitia isomorphism ya Curry-Howard.
Aina za kawaida na muunganisho
Kwa calculus ya lambda ambayo haijachapishwa, sheria ya kupunguza β kwa ujumla si nguvu wala urekebishaji dhaifu.
Hata hivyo, inaweza kuonyeshwa kuwa upunguzaji wa β huunganishwa wakati wa kufanya mageuzi ya α (yaani, aina mbili za kawaida zinaweza kuchukuliwa kuwa sawa ikiwa ubadilishaji wa α kutoka moja hadi nyingine unawezekana).
Kwa hivyo, istilahi za kuhalalisha sana na za urekebishaji dhaifu zina muundo mmoja wa kawaida. Kwa masharti ya kwanza, mkakati wowote wa kupunguza umehakikishiwa kusababisha usanidi wa kawaida. Ingawa kwa hali duni ya kuhalalisha, baadhi ya mikakati ya kupunguza inaweza isiipate.
Njia za ziada za kupanga
Kuna nahau nyingi za ubunifu za calculus ya lambda. Nyingi kati yao zilitengenezwa hapo awali katika muktadha wa kutumia mifumo kama msingi wa semantiki ya lugha ya programu, na kuitumia ipasavyo kama muundo wa kiwango cha chini. Kwa kuwa baadhi ya mitindo ni pamoja na calculus lambda (au kitu kinachofanana sana) kama kijisehemu, mbinu hizi pia hutumika katika uundaji wa vitendo, lakini zinaweza kuonekana kuwa zisizoeleweka au ngeni.
Vifungu vilivyotajwa
Katika calculus lambda, maktaba huchukua muundo wa seti ya vitendakazi vilivyobainishwa hapo awali, ambapo maneno ni viunga thabiti tu. Calculus safi haina dhana ya vibadilifu vilivyopewa jina kwani maneno yote ya lambda ya atomiki ni vigeuzo. Lakini pia zinaweza kuigwa kwa kuchukua kigeugeu kama jina la kisichobadilika, kwa kutumia kifupisho cha lambda kufunga tete hilo katika mwili, na kutumia uondoaji huo kwa ufafanuzi uliokusudiwa. Kwa hivyo ikiwa unatumia f kuwakilisha M katika N, unaweza kusema
(λ f. N) M.
Waandishi mara nyingi huanzisha dhana ya kisintaksia kama vile kuruhusu kuruhusu mambo kuandikwa kwa njia angavu zaidi.
f=M hadi N
Kwa kuweka fasili kama hizi, mtu anaweza kuandika "mpango" wa calculus ya lambda kama fasili sifuri au zaidi za utendakazi zinazofuatwa na mwanachama mmoja wa lambda, kwa kutumia fasili hizo zinazounda sehemu kubwa ya programu.
Kizuizi muhimu cha hii ni kwamba jina f halijafafanuliwa katika M,kwa kuwa M iko nje ya mawanda ya kisheria ya uondoaji wa lambda f. Hii inamaanisha kuwa sifa ya utendakazi inayojirudia haiwezi kutumika kama M with let. Sintaksia ya hali ya juu zaidi ya letrec, inayokuruhusu kuandika ufafanuzi wa utendakazi unaojirudia katika mtindo huu, hutumia viunganishi vya uhakika badala yake.
Analogi zilizochapishwa
Aina hii ni urasmi uliochapwa ambao hutumia ishara kuwakilisha kifupisho cha fomula kisichojulikana. Katika muktadha huu, aina kawaida ni vitu vya asili ya kisintaksia ambavyo hupewa istilahi za lambda. Asili halisi inategemea calculus inayohusika. Kwa mtazamo fulani, LI iliyochapishwa inaweza kuzingatiwa kama uboreshaji wa LI isiyochapishwa. Lakini kwa upande mwingine, zinaweza pia kuchukuliwa kuwa nadharia ya msingi zaidi, na calculus ya lambda isiyochapishwa ni kesi maalum yenye aina moja tu.
LI iliyochapishwa ndio msingi wa lugha za upangaji na uti wa mgongo wa lugha za utendaji kama vile ML na Haskell. Na, kwa njia isiyo ya moja kwa moja, mitindo ya lazima ya uumbaji. Chapa lambda calculi ina jukumu muhimu katika maendeleo ya mifumo ya aina kwa lugha za programu. Hapa, uchapaji kwa kawaida hunasa sifa zinazohitajika za programu, kwa mfano, haitasababisha ukiukaji wa ufikiaji wa kumbukumbu.
Kalikuli za lambda zilizoainishwa zinahusiana kwa karibu na mantiki ya hisabati na nadharia ya uthibitisho kupitia isomorphism ya Curry–Howard, na inaweza kufikiriwa kuwa lugha ya ndani ya kategoria, kwa mfano, ambayokwa urahisi ni mtindo wa kufungwa kwa Cartesian.
