Lambdaarvutus on formaalne matemaatilise loogika süsteem abstraktsioonipõhiste arvutuste väljendamiseks ja funktsioonide rakendamiseks sidumise ja muutuja asendamise abil. See on universaalne mudel, mida saab rakendada mis tahes Turingi masina disainis. Lambda-arvutuse võttis esmakordselt kasutusele kuulus matemaatik Church 1930. aastatel.
Süsteem koosneb lambda-elementide ehitamisest ja nendega redutseerimistoimingute tegemisest.
Selgitused ja rakendused
Kreeka tähte lambda (λ) kasutatakse lambda-avaldistes ja lambda-terminites, et tähistada muutuja sidumist funktsioonis.
Lambdaarvutit saab tüpistada või trükkida. Esimeses variandis saab funktsioone kasutada ainult siis, kui need on võimelised seda tüüpi andmeid vastu võtma. Tüüpilised lambdakivid on nõrgemad, võivad väljendada väiksemat väärtust. Kuid teisest küljest võimaldavad need tõestada rohkem asju.
Üks põhjus, miks on nii palju erinevaid tüüpe, on teadlaste soov teha rohkem, loobumata võimalusest tõestada tugevaid lambda-arvutuse teoreeme.
Süsteemil on rakendusi paljudes erinevates matemaatika, filosoofia, lingvistika ja arvutiteaduse valdkondades. Esiteks on lambda-arvutus programmeerimiskeelte teooria arengus olulist rolli mänginud arvutus. Süsteemid rakendavad funktsionaalse loomise stiile. Need on ka nende kategooriate teooria uurimise kuum teema.
Mannekeenidele
Matemaatik Alonzo Church võttis lambdaarvutuse kasutusele 1930. aastatel osana oma teaduse aluste uurimisest. Algne süsteem näis olevat loogiliselt vastuoluline 1935. aastal, kui Stephen Kleen ja J. B. Rosser töötasid välja Kleene-Rosseri paradoksi.
Hiljem, 1936. aastal, tõi Church välja ja avaldas ainult arvutuste jaoks olulise osa, mida praegu nimetatakse tüpiseerimata lambdaarvutuseks. 1940. aastal tutvustas ta ka nõrgemat, kuid loogiliselt järjekindlat teooriat, mida tuntakse algtüübisüsteemina. Oma töös selgitab ta kogu teooriat lihtsate sõnadega, seega võib öelda, et Church avaldas mannekeenide jaoks lambda-arvutuse.
Kuni 1960. aastateni, mil selle seos programmeerimiskeeltega sai selgeks, oli λ lihts alt formalism. Tänu Richard Montagu ja teiste keeleteadlaste rakendustele loomuliku keele semantikas on arvutus võtnud aukoha nii lingvistikas kui arvutiteaduses.
Sümboli päritolu
Lambda ei tähista sõna ega akronüümi, see pärineb viitest Russelli põhimatemaatikas, millele järgneb kaks tüpograafilist muudatust. Tähistusnäide: funktsiooni f puhul, mille f (y)=2y + 1, on 2ŷ + 1. Ja siin kasutame sisendmuutuja märgistamiseks y kohal olevat tähist ("kübar").
Kirik kavatses algselt kasutada sarnaseid sümboleid, kuid trükiladujad ei suutnud tähtede kohale asetada sümbolit "mütsi". Selle asemel printisid nad selle algselt kujul "/\y.2y+1". Redigeerimise järgmises osas asendasid masinakirjutajad "/ \" visuaalselt sarnase tähemärgiga.
Sissejuhatus lambdaarvutusse
Süsteem koosneb terminite keelest, mis on valitud kindla formaalse süntaksi järgi, ja teisendusreeglite komplektist, mis võimaldab nendega manipuleerida. Viimast punkti võib pidada võrranditeooriaks või operatiivdefinitsiooniks.
Kõik lambda-arvutuse funktsioonid on anonüümsed, mis tähendab, et neil pole nimesid. Neil on ainult üks sisendmuutuja ja karrimist kasutatakse mitme muutujaga graafikute rakendamiseks.
Lambda tingimused
Arvutuse süntaks määratleb mõned avaldised kehtivatena ja teised kehtetutena. Nii nagu erinevad märgistringid on kehtivad C-programmid ja mõned mitte. Lambda-arvutuse tegelikku väljendit nimetatakse "lambda-terminiks".
Järgmised kolm reeglit annavad induktiivse määratluse, mis võib ollarakendatakse kõigi süntaktiliselt kehtivate mõistete koostamisel:
Muutuja x ise on kehtiv lambda-termin:
- kui T on LT ja x on mittekonstantne, siis (lambda xt) nimetatakse abstraktsiooniks.
- kui T ja s on mõisted, siis (TS) nimetatakse rakenduseks.
Miski muu pole lambda-termin. Seega kehtib mõiste siis ja ainult siis, kui seda on võimalik saada nende kolme reegli korduval rakendamisel. Kuid mõned sulud võidakse teiste kriteeriumide kohaselt välja jätta.
Definitsioon
Lambda avaldised koosnevad:
- muutujad v 1, v 2, …, v n, …
- abstraktsiooni sümbolid 'λ' ja punkt '.'
- sulud ().
Komplekti Λ saab defineerida induktiivselt:
- Kui x on muutuja, siis x ∈ Λ;
- x ei ole konstantne ja M ∈ Λ, siis (λx. M) ∈ Λ;
- M, N ∈ Λ, siis (MN) ∈ Λ.
Nimetus
Selleks, et lambda-avaldiste tähistus oleks segaduses, kasutatakse tavaliselt järgmisi kokkuleppeid:
- Välised sulud välja jäetud: MN asemel (MN).
- Eeldatakse, et rakendused jäävad assotsiatiivseks: ((MN) P asemel võib kirjutada MNP).
- Abstraktsiooni keha ulatub veelgi paremale: λx. MN tähendab λx. (MN), mitte (λx. M) N.
- Abstraktsioonide järjestust vähendatakse: λx.λy.λz. N võib olla λxyz. N.
Vabad ja seotud muutujad
Tehetaja λ ühendab oma mittekonstandi kõikjal, kus see abstraktsiooni kehas asub. Muutujaid, mis kuuluvad ulatusse, nimetatakse seotuks. Avaldises λ x. M, λ x osa nimetatakse sageli sideaineks. Justkui vihjates, et muutujatest saab rühm, millele M-le lisandub X x. Kõiki teisi ebastabiilseid nimetatakse vabadeks.
Näiteks avaldises λ y. x x y, y - seotud mittepüsiv ja x - vaba. Samuti väärib märkimist, et muutuja on rühmitatud selle "lähima" abstraktsiooni järgi. Järgmises näites on lambda-arvutuse lahendus esitatud x ühekordse esinemisega, mis on seotud teise liikmega:
λ x. y (λ x. z x)
Vabade muutujate hulk M on tähistatud kui FV (M) ja on määratletud terminite struktuuri rekursiooniga järgmiselt:
- FV (x)={x}, kus x on muutuja.
- FV (λx. M)=FV (M) {x}.
- FV (MN)=FV (M) ∪ FV (N).
Valemit, mis ei sisalda vabu muutujaid, nimetatakse suletud. Suletud lambda-avaldisi tuntakse ka kombinaatoritena ja need on samaväärsed kombinatoorse loogika terminitega.
Lühend
Lambda-avaldiste tähenduse määrab see, kuidas neid saab lühendada.
On kolme tüüpi lõikeid:
- α-teisendus: seotud muutujate muutmine (alfa).
- β-reduktsioon: funktsioonide rakendamine nende argumentidele (beeta).
- η-teisendus: hõlmab laiendamise mõistet.
Siin see ka onme räägime saadud ekvivalentsustest: kaks avaldist on β-ekvivalentsed, kui neid saab β-transformeerida samaks komponendiks ja α / η-ekvivalentsus on defineeritud sarnaselt.
Mõte redex, lühend sõnadest vähendatav käive, viitab alateemadele, mida saab ühe reegliga vähendada. Lambda arvutus mannekeenide jaoks, näited:
(λ x. M) N on beeta-redex avaldises N-ga x-ga asendamiseks M-s. Komponenti, millele redex taandab, nimetatakse selle redutseerimiseks. Vähendus (λ x. M) N on M [x:=N].
Kui x ei ole M-s vaba, siis λ x. M x ka em-REDEX koos regulaatoriga M.
α-transformatsioon
Alfa ümbernimetamine võimaldab muuta seotud muutujate nimesid. Näiteks x. x võib anda λ y. y. Terminid, mis erinevad ainult alfa-teisenduses, on väidetav alt α-ekvivalendid. Sageli loetakse lambda-arvutuse kasutamisel α-ekvivalente vastastikusteks.
Alfa teisendamise täpsed reeglid ei ole täiesti triviaalsed. Esiteks, selle abstraktsiooniga nimetatakse ümber ainult need muutujad, mis on seotud sama süsteemiga. Näiteks alfateisendus λ x.λ x. x võib viia λ y.λ x-ni. x, kuid see ei pruugi kaasa tuua λy.λx.y Viimasel on originaalist erinev tähendus. See on analoogne muutuva varjundiga programmeerimise kontseptsiooniga.
Teiseks ei ole alfateisendus võimalik, kui selle tulemuseks oleks mittepüsiva muu abstraktsiooni hõivamine. Näiteks kui asendate x y-ga λ x.λ y-s. x, siis saadλy.λy. u, mis pole üldse sama.
Staatilise ulatusega programmeerimiskeeltes saab alfakonverteerimist kasutada nimede eraldusvõime lihtsustamiseks. Samal ajal tuleb hoolitseda selle eest, et muutuja mõiste ei varjaks tähistust sisaldavas piirkonnas.
De Bruyne'i indeksi tähistuses on mis tahes kaks alfa-ekvivalentset terminit süntaktiliselt identsed.
Asendamine
E [V:=R] poolt kirjutatud muudatused on protsess, mille käigus asendatakse kõik muutuja V vabad esinemised avaldises E käibega R. Asendamine λ-ga määratakse rekursiooni lambda abil. mõiste struktuuri arvutamine järgmiselt (märkus: x ja y - ainult muutujad ning M ja N - mis tahes λ-avaldis).
x [x:=N] ≡ N
y [x:=N] ≡ y, kui 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]), kui x ≠ y, eeldusel, et y ∉ FV (N).
Lambda-abstraktsiooniga asendamiseks on mõnikord vaja avaldist α-teisndada. Näiteks ei vasta tõele, et (λ x. Y) [y:=x] annab tulemuseks (λ x. X), sest asendatud x oleks pidanud olema vaba, kuid sai lõpuks seotud. Õige asendus on sel juhul (λ z. X) kuni α-ekvivalendini. Pange tähele, et asendus on üheselt määratletud kuni lambda-ni.
β-vähendamine
Beetavähendamine peegeldab funktsiooni rakendamise ideed. Beeta-redutseeriv on määratletud terminitesasendus: ((X V. E) E ') on E [V:=E'].
Kui eeldada näiteks mingit kodeeringut 2, 7, ×, on järgmine β-reduktsioon: ((λ n. N × 2) 7) → 7 × 2.
Beeta-vähendust võib vaadelda samana, mis kohaliku taandatavuse kontseptsiooni loomuliku deduktsiooni korral Curry-Howardi isomorfismi kaudu.
η-teisendus
See teisendus väljendab laienduse ideed, mis selles kontekstis seisneb selles, et kaks funktsiooni on võrdsed, kui need annavad kõigi argumentide jaoks sama tulemuse. See teisendus vahetab λ x vahel. (F x) ja f alati, kui x ei tundu f-s vaba.
Seda toimingut võib pidada samaks kui kohaliku täielikkuse kontseptsiooni loomulikus deduktsioonis Curry-Howardi isomorfismi kaudu.
Tavalised vormid ja sulandumine
Tüpimata lambda-arvutuse puhul ei ole β-taandamise reegel üldiselt ei tugev ega nõrk normaliseerimine.
Siiski saab näidata, et β-reduktsioon ühineb enne α-teisendust käivitades (st kahte normaalvormi võib lugeda võrdseks, kui α-teisendus ühest teiseks on võimalik).
Seetõttu on nii tugev alt normaliseerivatel kui ka nõrg alt kohandavatel terminitel üks normaalvorm. Esimestel tähtaegadel tagatakse iga vähendamise strateegia tulemuseks tüüpiline konfiguratsioon. Kui nõrg alt normaliseerivate tingimuste korral ei pruugi mõned vähendamise strateegiad seda leida.
Täiendavad programmeerimismeetodid
Lambda-arvutuse jaoks on palju loomise idioome. Paljud neist töötati algselt välja süsteemide kasutamise kontekstis programmeerimiskeele semantika alusena, rakendades neid tõhus alt madala taseme konstruktsioonina. Kuna mõned stiilid sisaldavad lambda-arvutit (või midagi väga sarnast) katkendina, leiavad need tehnikad kasutust ka praktilises loomingus, kuid neid võidakse siis tajuda ebaselgete või võõrastena.
Nimega konstandid
Lambda-arvutuses on teek eelnev alt määratletud funktsioonide komplekti kujul, kus terminid on vaid konkreetsed konstandid. Puhtal arvutusel pole nimega muutumatute mõistet, kuna kõik aatomi lambda terminid on muutujad. Kuid neid saab ka jäljendada, võttes konstandi nimeks muutuv, kasutades selle lenduva aine sidumiseks kehas lambda-abstraktsiooni ja rakendades seda abstraktsiooni kavandatud määratlusele. Nii et kui kasutate f-i M-i tähistamiseks N-s, võite öelda
(λ f. N) M.
Autorid tutvustavad sageli süntaktilist kontseptsiooni, näiteks luba, et võimaldada asjade kirjutamist intuitiivsemal viisil.
f=M kuni N
Selliste definitsioonide aheldamisel saab lambda-arvutuse "programmi" kirjutada null- või enama funktsioonimääratlustena, millele järgneb üks lambda-liige, kasutades definitsioone, mis moodustavad suurema osa programmist.
Selle olemuse märkimisväärne piirang on see, et nimi f ei ole M-s määratletud,kuna M on väljaspool lambda abstraktsiooni f siduvat ulatust. See tähendab, et rekursiivse funktsiooni atribuuti ei saa kasutada kui M koos letiga. Täpsem letreci süntaks, mis võimaldab kirjutada selles stiilis rekursiivseid funktsioonide määratlusi, kasutab lisaks selle asemel fikseeritud punktiga kombineerijaid.
Trükitud analoogid
See tüüp on tüüpformalism, mis kasutab anonüümse funktsiooni abstraktsiooni tähistamiseks sümbolit. Selles kontekstis on tüübid tavaliselt süntaktilist laadi objektid, mis on määratud lambda-terminitele. Täpne olemus sõltub kõnealusest arvutusest. Teatud vaatenurgast võib tüpiseeritud LI-d pidada tüpiseerimata LI täiustusteks. Kuid teisest küljest võib neid pidada ka fundamentaalsemaks teooriaks ja tüpiseerimata lambdaarvutus on erijuhtum ainult ühe tüübi puhul.
Typed LI on programmeerimiskeelte alus ja funktsionaalsete keelte, nagu ML ja Haskell, selgroog. Ja veel kaudsem alt imperatiivsed loomingustiilid. Tüüpilised lambda-arvutid mängivad olulist rolli programmeerimiskeelte tüübisüsteemide väljatöötamisel. Siin fikseerib tüüpilisus tavaliselt programmi soovitud omadused, näiteks ei põhjusta see mälu juurdepääsu rikkumist.
Tüpitud lambdaarvutused on Curry-Howardi isomorfismi kaudu tihed alt seotud matemaatilise loogika ja tõestusteooriaga ning neid võib pidada näiteks kategooriaklasside sisemiseks keeleks, mison lihts alt Descartes'i sulgede stiil.
