Lambda aprēķins ir formāla sistēma matemātiskajā loģikā, lai izteiktu uz abstrakciju balstītus aprēķinus un lietotu funkcijas, izmantojot saistošu un mainīgo aizstāšanu. Šis ir universāls modelis, ko var izmantot jebkuras Tjūringa mašīnas dizainā. Lambda aprēķinu pirmo reizi ieviesa slavenais matemātiķis Čērss 1930. gados.
Sistēma sastāv no lambda elementu izveidošanas un samazināšanas darbību veikšanas uz tiem.
Paskaidrojumi un lietojumprogrammas
Grieķu burts lambda (λ) tiek lietots lambda izteiksmēs un lambda terminos, lai apzīmētu mainīgā saistīšanu funkcijā.
Lambda skaitļus var nerakstīt vai ievadīt. Pirmajā variantā funkcijas var izmantot tikai tad, ja tās spēj saņemt šāda veida datus. Ierakstītie lambda kaļķakmens ir vājāki, var izteikt mazāku vērtību. Bet, no otras puses, tie ļauj pierādīt vairāk lietu.
Viens no iemesliem, kāpēc ir tik daudz dažādu veidu, ir zinātnieku vēlme darīt vairāk, neatsakoties no iespējas pierādīt spēcīgas lambda aprēķinu teorēmas.
Sistēmai ir lietojumprogrammas daudzās dažādās matemātikas, filozofijas, valodniecības un datorzinātņu jomās. Pirmkārt, lambda aprēķins ir kalkulators, kam ir bijusi nozīmīga loma programmēšanas valodu teorijas attīstībā. Sistēmas īsteno funkcionālās radīšanas stilus. Tie ir arī aktuāls šo kategoriju teorijas pētījumu temats.
Manekeniem
Lambda aprēķinus ieviesa matemātiķis Alonzo Čērčs 20. gadsimta 30. gados, veicot pētījumus par zinātnes pamatiem. Sākotnējā sistēma tika pierādīta kā loģiski nekonsekventa 1935. gadā, kad Stīvens Kleens un J. B. Rosers izstrādāja Kleēna-Rosera paradoksu.
Vēlāk, 1936. gadā, Čērča izcēla un publicēja tikai to daļu, kas attiecas uz aprēķiniem, ko tagad sauc par untyped lambda calculus. 1940. gadā viņš arī ieviesa vājāku, bet loģiski konsekventu teoriju, kas pazīstama kā primārā tipa sistēma. Savā darbā viņš visu teoriju izskaidro vienkāršā izteiksmē, tāpēc var teikt, ka Čērča publicēja calculus lambda manekeniem.
Līdz 1960. gadiem, kad kļuva skaidra tā saistība ar programmēšanas valodām, λ bija tikai formālisms. Pateicoties Ričarda Montagu un citu valodnieku pielietojumiem dabiskās valodas semantikā, aprēķins ir ieņēmis lepnumu gan valodniecībā, gan datorzinātnēs.
Simbola izcelsme
Lambda neapzīmē vārdu vai akronīmu, tas nāk no atsauces Russell's Principal Mathematics, kam seko divas tipogrāfiskas izmaiņas. Apzīmējuma piemērs: funkcijai f ar f (y)=2y + 1 ir 2ŷ + 1. Un šeit mēs izmantojam caret ("cepure") virs y, lai apzīmētu ievades mainīgo.
Sākotnēji baznīca plānoja izmantot līdzīgus simbolus, taču rakstītāji nespēja virs burtiem novietot simbolu "cepure". Tā vietā viņi to sākotnēji izdrukāja kā "/\y.2y+1". Nākamajā rediģēšanas sērijā mašīnrakstītājas aizstāja "/ \" ar vizuāli līdzīgu rakstzīmi.
Ievads lambda aprēķinos
Sistēma sastāv no terminu valodas, ko izvēlas noteikta formāla sintakse, un transformācijas noteikumu kopas, kas ļauj ar tiem manipulēt. Pēdējo punktu var uzskatīt par vienādojumu teoriju vai kā darbības definīciju.
Visas funkcijas lambda aprēķinos ir anonīmas, tas nozīmē, ka tām nav nosaukumu. Tiem ir nepieciešams tikai viens ievades mainīgais, un kariēšana tiek izmantota, lai ieviestu diagrammas ar vairākiem mainīgajiem.
Lambda noteikumi
Aprēķinu sintakse definē dažas izteiksmes kā derīgas, bet citas kā nederīgas. Tāpat kā dažādas rakstzīmju virknes ir derīgas C programmām, bet dažas nav. Faktisko lambda skaitļa izteiksmi sauc par "lambda terminu".
Šie trīs noteikumi sniedz induktīvu definīciju, kas var būtattiecas uz visu sintaktiski derīgo jēdzienu uzbūvi:
Pats x mainīgais ir derīgs lambda termins:
- ja T ir LT un x ir nekonstants, tad (lambda xt) sauc par abstrakciju.
- ja T un s ir jēdzieni, tad (TS) sauc par lietojumprogrammu.
Nekas cits nav lambda termins. Tādējādi jēdziens ir spēkā tikai tad, ja to var iegūt, atkārtoti piemērojot šos trīs noteikumus. Tomēr dažas iekavas var tikt izlaistas saskaņā ar citiem kritērijiem.
Definīcija
Lambda izteiksmes sastāv no:
- mainīgie v 1, v 2, …, v n, …
- abstrakcijas simboli 'λ' un punkts '.'
- iekavas ().
Kopu Λ var definēt induktīvi:
- Ja x ir mainīgs, tad x ∈ Λ;
- x nav konstants un M ∈ Λ, tad (λx. M) ∈ Λ;
- M, N ∈ Λ, pēc tam (MN) ∈ Λ.
Apzīmējums
Lai lambda izteiksmju apzīmējums būtu nepārblīvēts, parasti tiek izmantotas šādas konvencijas:
- Ārējās iekavas izlaistas: MN (MN) vietā.
- Pieņemts, ka lietojumprogrammas paliek asociatīvas: ((MN) P vietā var rakstīt MNP).
- Abstrakcijas korpuss sniedzas tālāk pa labi: λx. MN nozīmē λx. (MN), nevis (λx. M) N.
- Abstrakciju secība ir samazināta: λx.λy.λz. N var būt λxyz. N.
Brīvi un saistīti mainīgie
Operators λ savieno savu nekonstanti neatkarīgi no tā, kur tā atrodas abstrakcijas ķermenī. Mainīgos, kas ietilpst darbības jomā, sauc par saistītiem. Izteiksmē λ x. M, λ x daļa bieži tiek saukta par saistvielu. It kā dodot mājienu, ka mainīgie kļūst par grupu, pievienojot X x pie M. Visi pārējie nestabilie tiek saukti par brīviem.
Piemēram, izteiksmē λ y. x x y, y - saistīts nepastāvīgs un x - brīvs. Un ir arī vērts atzīmēt, ka mainīgais ir grupēts pēc tā "tuvākās" abstrakcijas. Nākamajā piemērā lambda aprēķinu risinājums ir attēlots ar vienu x gadījumu, kas ir saistīts ar otro terminu:
λ x. y (λ x. z x)
Brīvo mainīgo kopa M tiek apzīmēta kā FV (M) un tiek definēta ar rekursiju pār terminu struktūru šādi:
- FV (x)={x}, kur x ir mainīgais.
- FV (λx. M)=FV (M) {x}.
- FV (MN)=FV (M) ∪ FV (N).
Formulu, kas nesatur brīvus mainīgos, sauc par slēgtu. Slēgtās lambda izteiksmes ir pazīstamas arī kā kombinatores, un tās ir līdzvērtīgas kombinatoriskās loģikas terminiem.
Saīsinājums
Lambda izteiksmju nozīmi nosaka tas, kā tās var saīsināt.
Ir trīs griezumu veidi:
- α-transformācija: saistīto mainīgo maiņa (alfa).
- β-samazināšana: funkciju lietošana to argumentiem (beta).
- η-transformācija: aptver paplašinātuma jēdzienu.
Šeit arī tas irmēs runājam par iegūtajām ekvivalentām: divas izteiksmes ir β-ekvivalentas, ja tās var pārveidot par β vienā un tajā pašā komponentā, un α / η-ekvivalence tiek definēta līdzīgi.
Termins redex, kas ir saīsinājums no samazināmā apgrozījuma, attiecas uz apakštēmām, kuras var samazināt, ievērojot kādu no noteikumiem. Lambda aprēķins manekeniem, piemēri:
(λ x. M) N ir beta redekss izteiksmē N ar x aizstāšanai M. Komponentu, līdz kuram redukcija samazina, sauc par tā reducēšanu. Samazinājums (λ x. M) N ir M [x:=N].
Ja x nav brīvs M, λ x. M x arī em-REDEX ar regulatoru M.
α-transformācija
Alfa pārdēvēšana ļauj mainīt saistīto mainīgo nosaukumus. Piemēram, x. x var dot λ y. y. Tiek uzskatīts, ka termini, kas atšķiras tikai alfa transformācijā, ir α ekvivalenti. Bieži vien, izmantojot lambda aprēķinu, α-ekvivalenti tiek uzskatīti par savstarpēji saistītiem.
Precīzi alfa pārveidošanas noteikumi nav gluži triviāli. Pirmkārt, ar šo abstrakciju tiek pārdēvēti tikai tie mainīgie, kas ir saistīti ar to pašu sistēmu. Piemēram, alfa transformācija λ x.λ x. x var novest pie λ y.λ x. x, taču tas var nenovest pie λy.λx.y Pēdējam ir cita nozīme nekā oriģinālam. Tas ir analoģisks mainīgās ēnošanas programmēšanas jēdzienam.
Otrkārt, alfa transformācija nav iespējama, ja tā tiktu uztverta ar nepastāvīgu citu abstrakciju. Piemēram, ja λ x.λ y aizstājat x ar y. x, tad jūs varat iegūtλy.λy. u, kas nemaz nav tas pats.
Programmēšanas valodās ar statisku darbības jomu alfa konvertēšanu var izmantot, lai vienkāršotu nosaukuma izšķirtspēju. Vienlaikus raugoties, lai mainīgā jēdziens neslēptu apzīmējumu saturošajā apgabalā.
De Bruyne indeksa apzīmējumā jebkuri divi alfa ekvivalenti termini ir sintaktiski identiski.
Aizvietošana
Izmaiņas, ko raksta E [V:=R], ir process, kurā visi mainīgā V brīvie gadījumi izteiksmē E tiek aizstāti ar apgrozījumu R. Aizvietošanu λ izteiksmē nosaka rekursijas lambda. jēdziena struktūras aprēķins (piezīme: x un y - tikai mainīgie, un M un N - jebkura λ izteiksme).
x [x:=N] ≡ N
y [x:=N] ≡ y, ja 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]), ja x ≠ y, ar nosacījumu, ka y ∉ FV (N).
Lai aizstātu ar lambda abstrakciju, dažreiz ir nepieciešams α-pārveidot izteiksmi. Piemēram, nav taisnība, ka (λ x. Y) [y:=x] rezultāts ir (λ x. X), jo aizvietotajam x vajadzēja būt brīvam, taču tas tika piesaistīts. Pareizā aizstāšana šajā gadījumā ir (λ z. X) līdz α-ekvivalencei. Ņemiet vērā, ka aizstāšana ir unikāli definēta līdz lambda.
β-samazinājums
Beta samazināšana atspoguļo ideju par funkcijas lietošanu. Beta-reduktīvs ir definēts terminosaizstāšana: ((X V. E) E ') ir E [V:=E'].
Piemēram, pieņemot, ka kodējums ir 2, 7, ×, ir šāda β-reducēšana: ((λ n. N × 2) 7) → 7 × 2.
Beta samazināšanu var uzskatīt par tādu pašu kā vietējās reducējamības jēdzienu dabiskā dedukcijas rezultātā, izmantojot Karija-Hovarda izomorfismu.
η-pārveidot
Šis pārveidojums pauž paplašināšanas ideju, kas šajā kontekstā ir tāda, ka divas funkcijas ir vienādas, ja tās visiem argumentiem dod vienādu rezultātu. Šī konversija notiek starp λ x. (F x) un f ikreiz, kad x nešķiet brīvs f.
Šo darbību var uzskatīt par tādu pašu kā vietējās pilnības jēdzienu dabiskajā deducijā, izmantojot Karija-Hovarda izomorfismu.
Parastas formas un saplūšana
Netipizētam lambda aprēķinam β-samazināšanas noteikums parasti nav ne spēcīgs, ne vāji normalizējošs.
Tomēr var parādīt, ka β-samazinājums saplūst, veicot pirms α-transformācijas (t.i., divas normālās formas var uzskatīt par vienādām, ja ir iespējama α-transformācija no vienas uz otru).
Tādēļ gan stipri normalizējošiem terminiem, gan vāji koriģējošiem terminiem ir viena normālā forma. Pirmajos termiņos jebkura samazināšanas stratēģija garantē tipisku konfigurāciju. Tā kā vāji normalizējošos apstākļos dažas samazināšanas stratēģijas to nevar atrast.
Papildu programmēšanas metodes
Lambda aprēķinam ir daudz izveides idiomu. Daudzi no tiem sākotnēji tika izstrādāti saistībā ar sistēmu izmantošanu kā programmēšanas valodas semantikas pamatu, efektīvi pielietojot tās kā zema līmeņa konstrukciju. Tā kā dažos stilos kā fragments ir iekļauts lambda aprēķins (vai kaut kas ļoti līdzīgs), šīs metodes tiek izmantotas arī praktiskajā radīšanā, taču pēc tam tās var tikt uztvertas kā neskaidras vai svešas.
Nosauktas konstantes
Lambda aprēķinos bibliotēka izpaužas kā iepriekš definētu funkciju kopa, kur termini ir tikai konkrētas konstantes. Tīrajiem aprēķiniem nav nosaukto nemainīgo jēdziena, jo visi atomu lambda termini ir mainīgie. Bet tos var arī atdarināt, pieņemot mainīgo kā konstantes nosaukumu, izmantojot lambda abstrakciju, lai saistītu šo gaistošo vielu organismā, un piemērojot šo abstrakciju paredzētajai definīcijai. Tātad, ja izmantojat f, lai apzīmētu M N, jūs varētu teikt
(λ f. N) M.
Autori bieži ievieš sintaktisko jēdzienu, piemēram, ļaut, lai lietas varētu rakstīt intuitīvāk.
f=M līdz N
Savienojot šādas definīcijas, var ierakstīt lambda aprēķinu "programmu" kā nulle vai vairākas funkciju definīcijas, kam seko viens lambda elements, izmantojot tās definīcijas, kas veido programmas lielāko daļu.
Ievērojams ierobežojums ir tas, ka vārds f nav definēts M,jo M ir ārpus lambda abstrakcijas f saistošās jomas. Tas nozīmē, ka rekursīvās funkcijas atribūtu nevar izmantot kā M ar let. Uzlabotā Letrec sintakse, kas ļauj rakstīt rekursīvas funkciju definīcijas šajā stilā, papildus izmanto fiksēto punktu kombinatorus.
Iedrukātie analogi
Šis veids ir drukāts formālisms, kas izmanto simbolu, lai attēlotu anonīmu funkcijas abstrakciju. Šajā kontekstā tipi parasti ir sintaktiskas dabas objekti, kas tiek piešķirti lambda terminiem. Precīzs raksturs ir atkarīgs no attiecīgā aprēķina. No noteikta viedokļa tipizētu LI var uzskatīt par netipizēta LI precizējumiem. Bet, no otras puses, tos var uzskatīt arī par fundamentālāku teoriju, un netipizētais lambda aprēķins ir īpašs gadījums tikai ar vienu tipu.
Typed LI ir programmēšanas valodu pamats un funkcionālo valodu, piemēram, ML un Haskell, mugurkauls. Un, vēl netiešāk, obligātie radīšanas stili. Tipveida lambda skaitļiem ir liela nozīme programmēšanas valodu tipu sistēmu izstrādē. Šeit tipējamība parasti uztver vēlamās programmas īpašības, piemēram, tas neizraisīs atmiņas piekļuves pārkāpumu.
Ierakstītie lambda aprēķini ir cieši saistīti ar matemātisko loģiku un pierādījumu teoriju, izmantojot Karija–Hovarda izomorfismu, un tos var uzskatīt par, piemēram, kategoriju klašu iekšējo valodu, kasvienkārši ir dekarta aizdares stils.
