Njehsimi Lambda është një sistem formal në logjikën matematikore për shprehjen e llogaritjeve të bazuara në abstraksion dhe aplikimin e funksioneve duke përdorur lidhjen dhe zëvendësimin e ndryshoreve. Ky është një model universal që mund të aplikohet në dizajnin e çdo makinerie Turing. Llogaritja lambda u prezantua për herë të parë nga Church, një matematikan i famshëm, në vitet 1930.
Sistemi përbëhet nga ndërtimi i anëtarëve lambda dhe kryerja e operacioneve të reduktimit mbi to.
Shpjegime dhe Zbatime
Shkronja greke lambda (λ) përdoret në shprehjet lambda dhe termat lambda për të treguar lidhjen e një ndryshoreje në një funksion.
Llogaritja Lambda mund të jetë e pashtypshme ose e shtypur. Në variantin e parë, funksionet mund të përdoren vetëm nëse janë në gjendje të marrin të dhëna të këtij lloji. Llogaritë e shtypura lambda janë më të dobëta, mund të shprehin një vlerë më të vogël. Por, nga ana tjetër, ato ju lejojnë të provoni më shumë gjëra.
Një arsye që ka kaq shumë lloje të ndryshme është dëshira e shkencëtarëve për të bërë më shumë pa hequr dorë nga mundësia për të provuar teorema të forta të llogaritjes lambda.
Sistemi ka aplikime në shumë fusha të ndryshme të matematikës, filozofisë, gjuhësisë dhe shkencave kompjuterike. Para së gjithash, llogaritja lambda është një llogaritje që ka luajtur një rol të rëndësishëm në zhvillimin e teorisë së gjuhëve të programimit. Janë stilet e krijimit funksional që sistemet zbatojnë. Ato janë gjithashtu një temë e nxehtë e kërkimit në teorinë e këtyre kategorive.
Për bedelet
Llogaritja lambda u prezantua nga matematikani Alonzo Church në vitet 1930 si pjesë e kërkimit të tij në themelet e shkencës. Sistemi origjinal u tregua se ishte logjikisht jokonsistent në vitin 1935 kur Stephen Kleen dhe J. B. Rosser zhvilluan paradoksin Kleene-Rosser.
Më vonë, në vitin 1936, Church veçoi dhe publikoi vetëm pjesën që lidhet me llogaritjet, atë që tani quhet llogaritja e pashtypshme lambda. Në vitin 1940 ai prezantoi gjithashtu një teori më të dobët, por logjikisht të qëndrueshme të njohur si sistemi i tipit kryesor. Në veprën e tij, ai shpjegon të gjithë teorinë në terma të thjeshtë, kështu që mund të thuhet se Kisha botoi llogaritjen lambda për dummies.
Deri në vitet 1960, kur lidhja e saj me gjuhët e programimit u bë e qartë, λ ishte thjesht një formalizëm. Falë aplikimeve të Richard Montagu dhe gjuhëtarëve të tjerë në semantikën e gjuhës natyrore, llogaritja ka zënë vend krenarinë si në gjuhësi ashtu edhe në shkencën kompjuterike.
Origjina e simbolit
Lambda nuk do të thotë një fjalë ose akronim, ajo vjen nga një referencë në Matematika kryesore e Russell e ndjekur nga dy ndryshime tipografike. Shembull shënimi: për një funksion f me f (y)=2y + 1 është 2ŷ + 1. Dhe këtu përdorim një kapelë (“kapelë”) mbi y për të etiketuar variablin e hyrjes.
Kisha fillimisht kishte për qëllim të përdorte simbole të ngjashme, por daktilografët nuk ishin në gjendje të vendosnin simbolin "kapelë" mbi shkronjat. Pra, në vend të kësaj ata e printuan atë fillimisht si "/\y.2y+1". Në episodin tjetër të redaktimit, daktilografistët zëvendësuan "/ \" me një karakter vizualisht të ngjashëm.
Hyrje në llogaritjen lambda
Sistemi përbëhet nga një gjuhë termash, të cilat zgjidhen nga një sintaksë e caktuar formale, dhe një grup rregullash transformimi që lejojnë manipulimin e tyre. Pika e fundit mund të konsiderohet si një teori ekuacionale ose si një përkufizim operacional.
Të gjitha funksionet në llogaritjen lambda janë anonime, që do të thotë se nuk kanë emra. Ata marrin vetëm një ndryshore hyrëse dhe currying përdoret për të zbatuar grafikët me shumë variabla.
Termat Lambda
Sintaksa e llogaritjes përcakton disa shprehje si të vlefshme dhe të tjera si të pavlefshme. Ashtu si vargjet e ndryshme të karaktereve janë programe të vlefshme C dhe disa jo. Shprehja aktuale e llogaritjes lambda quhet "termi lambda".
Tre rregullat e mëposhtme ofrojnë një përkufizim induktiv që mund të jetëzbatohet për ndërtimin e të gjitha koncepteve të vlefshme sintaksore:
Vetë ndryshorja x është një term i vlefshëm lambda:
- nëse T është LT dhe x është jokonstante, atëherë (lambda xt) quhet abstraksion.
- nëse T si dhe s janë koncepte, atëherë (TS) quhet aplikacion.
Asgjë tjetër nuk është një term lambda. Kështu, një koncept është i vlefshëm nëse dhe vetëm nëse ai mund të merret me zbatimin e përsëritur të këtyre tre rregullave. Megjithatë, disa kllapa mund të hiqen sipas kritereve të tjera.
Përkufizim
Shprehjet Lambda përbëhen nga:
- variabla v 1, v 2, …, v n, …
- simbolet e abstraksionit 'λ' dhe pikës '.'
- kllapa ().
Setia Λ mund të përcaktohet në mënyrë induktive:
- Nëse x është një ndryshore, atëherë x ∈ Λ;
- x nuk është konstante dhe M ∈ Λ, atëherë (λx. M) ∈ Λ;
- M, N ∈ Λ, pastaj (MN) ∈ Λ.
Përcaktimi
Për të mbajtur shënimin e shprehjeve lambda të pa ngatërruar, zakonisht përdoren konventat e mëposhtme:
- Kllapat e jashtme u hoqën: MN në vend të (MN).
- Aplikimet supozohet të mbeten shoqëruese: mund të shkruhet MNP në vend të ((MN) P).
- Trupi i abstraksionit shtrihet më tej djathtas: λx. MN do të thotë λx. (MN), jo (λx. M) N.
- Sekuenca e abstraksioneve zvogëlohet: λx.λy.λz. N mund të jetë λxyz. N.
Ndryshoret e lira dhe të kufizuara
Operatori λ lidh jokonstanten e tij kudo që është në trupin e abstraksionit. Variablat që hyjnë në fushëveprim quhen të lidhura. Në shprehjen λ x. M, pjesa λ x shpesh referohet si lidhës. Sikur të lë të kuptohet se variablat bëhen një grup me shtimin e X x në M. Të gjitha ato të tjera të paqëndrueshme quhen të lira.
Për shembull, në shprehjen λ y. x x y, y - i lidhur jo i përhershëm dhe x - i lirë. Dhe vlen gjithashtu të theksohet se ndryshorja është grupuar sipas abstraksionit të saj "më të afërt". Në shembullin e mëposhtëm, zgjidhja e llogaritjes lambda përfaqësohet nga një dukuri e vetme e x, e cila lidhet me termin e dytë:
λ x. y (λ x. z x)
Bashkimi i ndryshoreve të lira M shënohet si FV (M) dhe përcaktohet me rekursion mbi strukturën e termave si më poshtë:
- FV (x)={x}, ku x është një ndryshore.
- FV (λx. M)=FV (M) {x}.
- FV (MN)=FV (M) ∪ FV (N).
Një formulë që nuk përmban variabla të lira quhet e mbyllur. Shprehjet e mbyllura lambda njihen gjithashtu si kombinatorë dhe janë ekuivalente me termat në logjikën kombinatorike.
Shkurtesa
Kuptimi i shprehjeve lambda përcaktohet nga mënyra se si ato mund të shkurtohen.
Ka tre lloje prerjesh:
- α-transformim: ndryshimi i variablave të kufizuar (alfa).
- β-reduksion: aplikimi i funksioneve në argumentet e tyre (beta).
- η-transform: mbulon nocionin e shtrirjes.
Ja ku është gjithashtupo flasim për ekuivalencat që rezultojnë: dy shprehje janë β-ekuivalente nëse ato mund të shndërrohen β-në të njëjtin komponent, dhe ekuivalenca α/η përcaktohet në mënyrë të ngjashme.
Termi redex, shkurt për qarkullim të reduktueshëm, i referohet nënçështjeve që mund të reduktohen me një nga rregullat. Llogaritja e Lambda për dummies, shembuj:
(λ x. M) N është një beta redex në shprehjen për zëvendësimin e N me x në M. Komponenti në të cilin reduktohet një redeks quhet reduktim i tij. Reduktimi (λ x. M) N është M [x:=N].
Nëse x nuk është i lirë në M, λ x. M x gjithashtu em-REDEX me rregullator M.
a-transformim
Riemërimet alfa ju lejojnë të ndryshoni emrat e variablave të lidhur. Për shembull, x. x mund të japë λ y. y. Termat që ndryshojnë vetëm në transformimin alfa thuhet se janë α-ekuivalente. Shpesh, kur përdoret llogaritja lambda, α-ekuivalentët konsiderohen reciproke.
Rregullat e sakta për konvertimin alfa nuk janë krejtësisht të parëndësishme. Së pari, me këtë abstraksion riemërohen vetëm ato variabla që janë të lidhur me të njëjtin sistem. Për shembull, transformimi alfa λ x.λ x. x mund të çojë në λ y.λ x. x, por kjo mund të mos çojë në λy.λx.y Kjo e fundit ka një kuptim të ndryshëm nga origjinali. Kjo është analoge me konceptin e programimit të hijeve të ndryshueshme.
Së dyti, një transformim alfa nuk është i mundur nëse do të rezultonte në kapjen nga një abstraksion tjetër jo i përhershëm. Për shembull, nëse zëvendësoni x me y në λ x.λ y. x, atëherë mund të merrniλy.λy. u, e cila nuk është aspak e njëjtë.
Në gjuhët e programimit me shtrirje statike, konvertimi alfa mund të përdoret për të thjeshtuar rezolucionin e emrit. Në të njëjtën kohë, duke u kujdesur që koncepti i një ndryshore të mos maskojë emërtimin në zonën që përmban.
Në shënimin e indeksit De Bruyne, çdo dy terma ekuivalent alfa janë sintaksisht identikë.
Zëvendësim
Ndryshimet e shkruara nga E [V:=R] janë procesi i zëvendësimit të të gjitha dukurive të lira të ndryshores V në shprehjen E me qarkullimin R. Zëvendësimi në terma λ përcaktohet nga lambda e rekursionit llogaritja në strukturën e konceptit si më poshtë (shënim: x dhe y - vetëm variablat, dhe M dhe N - çdo shprehje λ).
x [x:=N] ≡ N
y [x:=N] ≡ y nëse 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]) nëse x ≠ y, me kusht që y ∉ FV (N).
Për zëvendësimin në një abstraksion lambda, ndonjëherë është e nevojshme të transformohet α-një shprehje. Për shembull, nuk është e vërtetë që (λ x. Y) [y:=x] rezulton në (λ x. X) sepse x i zëvendësuar duhet të ishte i lirë, por përfundoi i lidhur. Zëvendësimi i saktë në këtë rast është (λ z. X) deri në α-ekuivalencë. Vini re se zëvendësimi është përcaktuar në mënyrë unike deri në lambda.
b-reduktim
Reduktimi beta pasqyron idenë e aplikimit të një funksioni. Beta-reduktivi përcaktohet në termazëvendësimi: ((X V. E) E ') është E [V:=E'].
Për shembull, duke supozuar një kodim 2, 7, ×, ekziston reduktimi i mëposhtëm β: ((λ n. N × 2) 7) → 7 × 2.
Reduktimi beta mund të shihet si i njëjtë me konceptin e reduktueshmërisë lokale nën deduksion natyror nëpërmjet izomorfizmit Curry-Howard.
η-transform
Ky konvertim shpreh idenë e shtrirjes, që në këtë kontekst është se dy funksione janë të barabarta kur japin të njëjtin rezultat për të gjitha argumentet. Ky konvertim shkëmbehet ndërmjet λ x. (F x) dhe f sa herë që x nuk duket i lirë në f.
Ky veprim mund të konsiderohet i njëjtë me konceptin e plotësisë lokale në deduksionin natyror nëpërmjet izomorfizmit Curry-Howard.
Format normale dhe shkrirja
Për një llogaritje lambda të pa tipizuar, rregulli i reduktimit β në përgjithësi nuk është normalizues as i fortë as i dobët.
Megjithatë, mund të tregohet se reduktimi β bashkohet kur shkon përpara transformimit α (d.m.th., dy forma normale mund të konsiderohen të barabarta nëse është i mundur një transformim α nga njëra në tjetrën).
Prandaj, si termat normalizues të fortë ashtu edhe termat me rregullim të dobët kanë një formë të vetme normale. Për kushtet e para, çdo strategji reduktimi është e garantuar të rezultojë në një konfigurim tipik. Ndërsa për kushtet normalizuese të dobëta, disa strategji reduktimi mund të mos e gjejnë atë.
Metoda programimi shtesë
Ka shumë idioma të krijimit për llogaritjen lambda. Shumë prej tyre fillimisht u zhvilluan në kontekstin e përdorimit të sistemeve si bazë për semantikën e një gjuhe programimi, duke i zbatuar ato në mënyrë efektive si një konstrukt i nivelit të ulët. Meqenëse disa stile përfshijnë një llogaritje lambda (ose diçka shumë të ngjashme) si një fragment, këto teknika gjejnë përdorim edhe në krijimin praktik, por më pas mund të perceptohen si të paqarta ose të huaja.
Konstanta të emërtuara
Në llogaritjen lambda, një bibliotekë merr formën e një grupi funksionesh të përcaktuara më parë, ku termat janë thjesht konstante konkrete. Llogaritja e pastër nuk ka koncept të pandryshueshmeve të emërtuara pasi të gjithë termat lambda atomike janë variabla. Por ato gjithashtu mund të imitohen duke marrë të ndryshueshmen si emër të konstantës, duke përdorur një abstraksion lambda për të lidhur atë të paqëndrueshme në trup dhe duke zbatuar atë abstraksion në përkufizimin e synuar. Pra, nëse përdorni f për të përfaqësuar M në N, mund të thoni
(λ f. N) M.
Autorët shpesh prezantojnë një koncept sintaksor të tillë si le të lejojë që gjërat të shkruhen në një mënyrë më intuitive.
f=M në N
Duke lidhur me zinxhirë përkufizime të tilla, mund të shkruhet një "program" i llogaritjes lambda si zero ose më shumë përkufizime funksioni të ndjekura nga një anëtar i vetëm lambda, duke përdorur ato përkufizime që përbëjnë pjesën më të madhe të programit.
Një kufizim i dukshëm i kësaj le të jetë se emri f nuk është përcaktuar në M,meqenëse M është jashtë fushëveprimit lidhor të abstraksionit lambda f. Kjo do të thotë që një atribut funksioni rekurziv nuk mund të përdoret si M me let. Sintaksa më e avancuar letrec, e cila ju lejon të shkruani përkufizime të funksioneve rekursive në këtë stil, përdor në vend të kësaj, kombinues me pikë fikse.
Analoge të shtypura
Ky lloj është një formalizëm i shtypur që përdor një simbol për të përfaqësuar një abstraksion funksioni anonim. Në këtë kontekst, tipet janë zakonisht objekte të një natyre sintaksore që u caktohen termave lambda. Natyra e saktë varet nga llogaritja në fjalë. Nga një këndvështrim i caktuar, LI i shtypur mund të konsiderohet si përsosje e LI-së së pashtypshme. Por nga ana tjetër, ato mund të konsiderohen gjithashtu një teori më themelore, dhe llogaritja e pashtypshme lambda është një rast i veçantë me vetëm një lloj.
Typed LI janë themeli i gjuhëve të programimit dhe shtylla kurrizore e gjuhëve funksionale si ML dhe Haskell. Dhe, më indirekt, stilet imperative të krijimit. Llogaritjet e shtypura lambda luajnë një rol të rëndësishëm në zhvillimin e sistemeve të tipit për gjuhët e programimit. Këtu, tipizimi zakonisht kap vetitë e dëshiruara të programit, për shembull, nuk do të shkaktojë shkelje të aksesit në kujtesë.
Llogaritjet e tipuara lambda janë të lidhura ngushtë me logjikën matematikore dhe teorinë e provës përmes izomorfizmit Curry–Howard dhe mund të mendohen si një gjuhë e brendshme e klasave të kategorisë, për shembull, e cilathjesht është stili i mbylljeve karteziane.
