Lambda račun je formalni sistem v matematični logiki za izražanje izračunov, ki temeljijo na abstrakciji, in uporabo funkcij z uporabo vezave in zamenjave spremenljivk. To je univerzalni model, ki ga je mogoče uporabiti za oblikovanje katerega koli Turingovega stroja. Lambda račun je prvi uvedel Church, slavni matematik, v tridesetih letih prejšnjega stoletja.
Sistem je sestavljen iz gradnje lambda članov in izvajanja operacij redukcije na njih.
Pojasnila in aplikacije
Grška črka lambda (λ) se uporablja v lambda izrazih in lambda izrazih za označevanje vezave spremenljivke v funkciji.
Lambda račun je mogoče netipkati ali vtipkati. V prvi varianti se funkcije lahko uporabljajo le, če so sposobne sprejemati podatke te vrste. Vtipkani lambda računi so šibkejši, lahko izražajo manjšo vrednost. Toda po drugi strani vam omogočajo, da dokažete več stvari.
Eden od razlogov, zakaj obstaja toliko različnih vrst, je želja znanstvenikov, da naredijo več, ne da bi se odrekli priložnosti dokazati močne izreke lambda računa.
Sistem se uporablja na številnih različnih področjih matematike, filozofije, jezikoslovja in računalništva. Prvič, lambda račun je račun, ki je imel pomembno vlogo pri razvoju teorije programskih jezikov. Sistemi izvajajo sloge funkcionalnega ustvarjanja. So tudi vroča tema raziskav v teoriji teh kategorij.
Za lutke
Lambda račun je uvedel matematik Alonzo Church v tridesetih letih prejšnjega stoletja kot del svojih raziskav o temeljih znanosti. Prvotni sistem se je izkazal za logično nedoslednega leta 1935, ko sta Stephen Kleen in J. B. Rosser razvila Kleene-Rosserjev paradoks.
Pozneje, leta 1936, je Church izpostavil in objavil le del, ki je pomemben za izračune, kar se danes imenuje netipizirani lambda račun. Leta 1940 je uvedel tudi šibkejšo, a logično konsistentno teorijo, znano kot sistem prvega tipa. V svojem delu razlaga celotno teorijo preprosto, tako da lahko rečemo, da je Church objavil račun lambda za lutke.
Do šestdesetih let prejšnjega stoletja, ko je postal jasen njegov odnos do programskih jezikov, je bil λ le formalizem. Zahvaljujoč aplikacijam Richarda Montaguja in drugih jezikoslovcev v semantiki naravnega jezika je računanje zasedlo ponosno mesto tako v jezikoslovju kot v računalništva.
Izvor simbola
Lambda ne pomeni besede ali kratice, izhaja iz sklicevanja v Russellovi glavni matematiki, ki ji sledita dve tipografski spremembi. Primer zapisa: za funkcijo f s f (y)=2y + 1 je 2ŷ + 1. Tukaj uporabljamo karo (»klobuk«) nad y za označevanje vhodne spremenljivke.
Cerkev je prvotno nameravala uporabljati podobne simbole, vendar pisci niso mogli postaviti simbola "klobuk" nad črke. Namesto tega so ga prvotno natisnili kot "/\y.2y+1". V naslednji epizodi urejanja so tipkarice "/ \" zamenjale z vizualno podobnim znakom.
Uvod v lambda račun
Sistem je sestavljen iz jezika izrazov, ki jih izbere določena formalna sintaksa, in niza transformacijskih pravil, ki omogočajo manipulacijo z njimi. Zadnjo točko lahko obravnavamo kot teorijo enačb ali kot operativno definicijo.
Vse funkcije v lambda računu so anonimne, kar pomeni, da nimajo imen. Prevzamejo samo eno vhodno spremenljivko, curry pa se uporablja za izvajanje grafov z več spremenljivkami.
Lambda izrazi
Sintaksa računanja definira nekatere izraze kot veljavne, druge pa kot neveljavne. Tako kot so različni nizi znakov veljavni programi C in nekateri ne. Dejanski izraz lambda računa se imenuje "lambda izraz".
Naslednja tri pravila zagotavljajo induktivno definicijo, ki je lahkovelja za konstrukcijo vseh sintaktično veljavnih konceptov:
Spremenljivka x je veljaven lambda izraz:
- če je T LT in x ni konstanten, se (lambda xt) imenuje abstrakcija.
- če sta T in s koncepta, se (TS) imenuje aplikacija.
Nič drugega ni lambda izraz. Koncept je torej veljaven, če in samo, če ga je mogoče pridobiti z večkratno uporabo teh treh pravil. Vendar pa so lahko nekateri oklepaji v skladu z drugimi merili izpuščeni.
Definicija
Lambda izrazi so sestavljeni iz:
- spremenljivke v 1, v 2, …, v n, …
- simboli abstrakcije 'λ' in pike '.'
- oklepaji ().
Množico Λ je mogoče definirati induktivno:
- Če je x spremenljivka, potem je x ∈ Λ;
- x ni konstanten in M ∈ Λ, potem (λx. M) ∈ Λ;
- M, N ∈ Λ, nato (MN) ∈ Λ.
Oznaka
Da ostane zapis lambda izrazov nenatrpan, se običajno uporabljajo naslednje konvencije:
- Zunanji oklepaji izpuščeni: MN namesto (MN).
- Za aplikacije se predpostavlja, da ostanejo asociativne: namesto ((MN) P) lahko napišemo MNP.
- Telo abstrakcije se razteza še naprej v desno: λx. MN pomeni λx. (MN), ne (λx. M) N.
- Zaporedje abstrakcij je zmanjšano: λx.λy.λz. N je lahko λxyz. N.
Proste in vezane spremenljivke
Operator λ poveže svojo nekostanto, kjer koli je v telesu abstrakcije. Spremenljivke, ki spadajo v obseg, se imenujejo vezane. V izrazu λ x. M, del λ x pogosto imenujemo vezivo. Kot da bi namigovali, da spremenljivke postanejo skupina z dodatkom X x k M. Vse druge nestabilne se imenujejo proste.
Na primer v izrazu λ y. x x y, y - vezano nestalno in x - prosto. Prav tako je treba omeniti, da je spremenljivka združena po svoji "najbližji" abstrakciji. V naslednjem primeru je rešitev lambda računa predstavljena z enim samim pojavom x, ki je povezan z drugim izrazom:
λ x. y (λ x. z x)
Množica prostih spremenljivk M je označena kot FV (M) in je definirana z rekurzijo po strukturi izrazov, kot sledi:
- FV (x)={x}, kjer je x spremenljivka.
- FV (λx. M)=FV (M) {x}.
- FV (MN)=FV (M) ∪ FV (N).
Formula, ki ne vsebuje prostih spremenljivk, se imenuje zaprta. Zaprti lambda izrazi so znani tudi kot kombinatorji in so enakovredni izrazom v kombinatorični logiki.
Okrajšava
Pomen lambda izrazov je določen s tem, kako jih je mogoče skrajšati.
Obstajajo tri vrste rezov:
- α-transform: spreminjanje vezanih spremenljivk (alfa).
- β-redukcija: uporaba funkcij za njihove argumente (beta).
- η-transform: pokriva pojem ekstenzivnosti.
Tukaj je tudigovorimo o nastalih ekvivalencah: dva izraza sta β-ekvivalentna, če ju je mogoče β-pretvoriti v isto komponento, α / η-ekvivalenca pa je definirana podobno.
Izraz redex, okrajšava za zmanjšan promet, se nanaša na podteme, ki jih je mogoče zmanjšati z enim od pravil. Lambda račun za lutke, primeri:
(λ x. M) N je beta redex v izrazu za zamenjavo N z x v M. Komponenta, na katero se redex reducira, se imenuje njegov redukt. Zmanjšanje (λ x. M) N je M [x:=N].
Če x ni prost v M, λ x. M x tudi em-REDEX z regulatorjem M.
α-transformacija
Alfa preimenovanja vam omogočajo spreminjanje imen vezanih spremenljivk. Na primer, x. x lahko da λ y. y. Izrazi, ki se razlikujejo le v alfa transformaciji, naj bi bili α-ekvivalentni. Pri uporabi lambda računa se α-ekvivalenti pogosto štejejo za vzajemne.
Natančna pravila za alfa pretvorbo niso povsem trivialna. Prvič, s to abstrakcijo se preimenujejo samo tiste spremenljivke, ki so povezane z istim sistemom. Na primer, alfa transformacija λ x.λ x. x lahko vodi do λ y.λ x. x, vendar to morda ne vodi do λy.λx.y. Slednje ima drugačen pomen kot izvirnik. To je analogno konceptu programiranja spremenljivega senčenja.
Drugič, alfa transformacija ni mogoča, če bi povzročila, da bi jo zajela nestalna druga abstrakcija. Na primer, če zamenjate x z y v λ x.λ y. x, potem lahko dobiteλy.λy. u, kar sploh ni isto.
V programskih jezikih s statičnim obsegom se lahko alfa pretvorba uporablja za poenostavitev ločljivosti imen. Hkrati pazite, da koncept spremenljivke ne prikrije oznake v območju, ki vsebuje.
V zapisu indeksa De Bruyne sta katera koli dva alfa-ekvivalentna izraza sintaktično identična.
zamenjava
Spremembe, ki jih zapiše E [V:=R], so postopek zamenjave vseh prostih pojavov spremenljivke V v izrazu E s prometom R. Substitucija v smislu λ je definirana z lambda rekurzije račun o strukturi koncepta, kot sledi (opomba: x in y - samo spremenljivke, in M in N - kateri koli λ-izraz).
x [x:=N] ≡ N
y [x:=N] ≡ y, če je 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]) če je x ≠ y, pod pogojem, da je y ∉ FV (N).
Za zamenjavo v lambda abstrakcijo je včasih potrebno α-transformirati izraz. Na primer, ni res, da (λ x. Y) [y:=x] povzroči (λ x. X), ker bi moral biti substituirani x prost, vendar je bil na koncu vezan. Pravilna zamenjava v tem primeru je (λ z. X) do α-ekvivalence. Upoštevajte, da je zamenjava enolično definirana do lambda.
β-zmanjšanje
Beta zmanjšanje odraža zamisel o uporabi funkcije. Beta-redukcija je opredeljena z izrazizamenjava: ((X V. E) E ') je E [V:=E'].
Na primer, če predpostavimo nekaj kodiranja 2, 7, ×, obstaja naslednja β-redukcija: ((λ n. N × 2) 7) → 7 × 2.
Beta redukcijo lahko razumemo kot isto kot koncept lokalne reducibilnosti po naravnem odbitku preko Curry-Howardovega izomorfizma.
η-transform
Ta pretvorba izraža idejo ekstenzivnosti, ki v tem kontekstu pomeni, da sta dve funkciji enaki, če dajeta enak rezultat za vse argumente. Ta pretvorba se izmenjuje med λ x. (F x) in f, kadar se x ne zdi prost v f.
To dejanje je mogoče obravnavati kot isto kot koncept lokalne popolnosti v naravnem odbitku skozi Curry-Howardov izomorfizem.
Normalne oblike in zlitje
Za netipiziran lambda račun pravilo β-redukcije na splošno ni niti močna niti šibka normalizacija.
Kljub temu je mogoče dokazati, da se β-redukcija združi, ko teče pred α-transformacijo (tj. dve normalni obliki se lahko štejeta za enakovredni, če je možna α-transformacija iz ene v drugo).
Zato imajo tako močno normalizirajoči izrazi kot šibko prilagojeni izrazi eno normalno obliko. Za prve izraze je zagotovljeno, da bo vsaka strategija zmanjšanja povzročila tipično konfiguracijo. Medtem ko pri slabo normalizirajočih se pogojih nekatere strategije zmanjšanja tega morda ne najdejo.
Dodatne metode programiranja
Za lambda račun obstaja veliko kreacijskih idiomov. Mnogi od njih so bili prvotno razviti v kontekstu uporabe sistemov kot osnove za semantiko programskega jezika, pri čemer so jih učinkovito uporabili kot nizkonivojsko konstrukcijo. Ker nekateri slogi vključujejo lambda račun (ali nekaj zelo podobnega) kot delček, te tehnike najdejo uporabo tudi v praktičnem ustvarjanju, vendar jih lahko potem dojemamo kot nejasne ali tuje.
Poimenovane konstante
V lambda računu ima knjižnica obliko nabora predhodno definiranih funkcij, kjer so izrazi le konkretne konstante. Čisti račun nima koncepta imenovanih nespremenljivih, saj so vsi atomski lambda izrazi spremenljivke. Lahko pa jih posnemamo tudi tako, da vzamemo spremenljivo kot ime konstante, uporabimo abstrakcijo lambda za vezavo tega hlapnega elementa v telesu in to abstrakcijo uporabimo za predvideno definicijo. Torej, če uporabite f za predstavljanje M v N, bi lahko rekli
(λ f. N) M.
Avtorji pogosto uvajajo skladenjski koncept, kot je dovoliti, da se stvari zapišejo na bolj intuitiven način.
f=M do N
Z veriženjem takšnih definicij lahko zapišemo "program" lambda računa kot nič ali več definicij funkcij, ki jim sledi en sam lambda član, z uporabo tistih definicij, ki sestavljajo večino programa.
Pomembna omejitev te oznake je, da ime f ni definirano v M,ker je M zunaj zavezujočega obsega lambda abstrakcije f. To pomeni, da atributa rekurzivne funkcije ni mogoče uporabiti kot M z let. Naprednejša sintaksa letrec, ki vam omogoča pisanje definicij rekurzivnih funkcij v tem slogu, dodatno uporablja kombinatorje s fiksno točko.
Tiskani analogi
Ta tip je vtipkani formalizem, ki uporablja simbol za predstavljanje anonimne abstrakcije funkcije. V tem kontekstu so tipi običajno objekti skladenjske narave, ki so dodeljeni lambda izrazom. Natančna narava je odvisna od zadevnega računa. Z določenega vidika lahko tipizirani LI obravnavamo kot izboljšave netipiziranega LI. Po drugi strani pa jih lahko štejemo tudi za bolj temeljno teorijo, netipizirani lambda račun pa je poseben primer samo z eno vrsto.
Typed LI so temelj programskih jezikov in hrbtenica funkcionalnih jezikov, kot sta ML in Haskell. In bolj posredno, imperativni slogi ustvarjanja. Tipizirani lambda izračuni imajo pomembno vlogo pri razvoju tipskih sistemov za programske jezike. Tukaj tipkanje običajno zajame želene lastnosti programa, na primer ne bo povzročilo kršitve dostopa do pomnilnika.
Vtipkani lambda izračuni so tesno povezani z matematično logiko in teorijo dokazov prek Curry-Howardovega izomorfizma in jih je mogoče razumeti kot notranji jezik razredov kategorij, npr.preprosto je slog kartezijanskega zapiranja.
