Lambda-kalkulus er et formelt system i matematisk logikk for å uttrykke abstraksjonsbaserte beregninger og bruke funksjoner ved bruk av binding og variabelsubstitusjon. Dette er en universell modell som kan brukes på utformingen av enhver Turing-maskin. Lambdaregningen ble først introdusert av Church, en kjent matematiker, på 1930-tallet.
Systemet består av å bygge lambda-medlemmer og utføre reduksjonsoperasjoner på dem.
Forklaringer og applikasjoner
Den greske bokstaven lambda (λ) brukes i lambda-uttrykk og lambda-uttrykk for å betegne bindingen av en variabel i en funksjon.
Lambda-kalkulus kan være uskrevet eller skrevet. I den første varianten kan funksjoner bare brukes hvis de er i stand til å motta data av denne typen. Skrevne lambdaregninger er svakere, kan uttrykke en mindre verdi. Men på den annen side lar de deg bevise flere ting.
En grunn til at det er så mange forskjellige typer, er forskeres ønske om å gjøre mer uten å gi opp muligheten til å bevise sterke lambda-regningsteoremer.
Systemet har applikasjoner innen mange forskjellige områder innen matematikk, filosofi, lingvistikk og informatikk. For det første er lambda-regningen en kalkulus som har spilt en viktig rolle i utviklingen av teorien om programmeringsspråk. Det er stilene for funksjonell skapelse som systemene implementerer. De er også et hett tema for forskning i teorien om disse kategoriene.
For dummies
Lambda-regningen ble introdusert av matematikeren Alonzo Church på 1930-tallet som en del av hans forskning på vitenskapens grunnlag. Det originale systemet ble vist å være logisk inkonsekvent i 1935 da Stephen Kleen og J. B. Rosser utviklet Kleene-Rosser-paradokset.
Senere, i 1936, pekte Church ut og publiserte kun den delen som er relevant for beregninger, det som nå kalles den utskrevne lambdaregningen. I 1940 introduserte han også en svakere, men logisk konsistent teori kjent som prime type system. I sitt arbeid forklarer han hele teorien på en enkel måte, så det kan sies at Church publiserte lambda-kalkylen for dummies.
Fram til 1960-tallet, da forholdet til programmeringsspråk ble tydelig, var λ bare en formalisme. Takket være bruken av Richard Montagu og andre lingvister i semantikken til naturlig språk, har kalkulus tatt en stor plass i både lingvistikk og informatikk.
Opprinnelsen til symbolet
Lambda står ikke for et ord eller akronym, det kommer fra en referanse i Russells Principal Mathematics etterfulgt av to typografiske endringer. Notasjonseksempel: for en funksjon f med f (y)=2y + 1 er 2ŷ + 1. Og her bruker vi en indikator ("hat") over y for å merke inngangsvariabelen.
Kirken hadde opprinnelig til hensikt å bruke lignende symboler, men setterne klarte ikke å plassere "hatte"-symbolet over bokstavene. Så i stedet skrev de den opprinnelig ut som "/\y.2y+1". I neste episode av redigering erstattet maskinskrivere "/ \" med en visuelt lik karakter.
Introduksjon til lambdaregning
Systemet består av et språk med termer, som er valgt av en viss formell syntaks, og et sett med transformasjonsregler som gjør at de kan manipuleres. Det siste punktet kan betraktes som en likningsteori eller som en operasjonell definisjon.
Alle funksjoner i lambda-kalkulen er anonyme, noe som betyr at de ikke har navn. De tar bare én inngangsvariabel, og currying brukes til å implementere plott med flere variabler.
Lambda-vilkår
Kalkylesyntaksen definerer noen uttrykk som gyldige og andre som ugyldige. Akkurat som forskjellige tegnstrenger er gyldige C-programmer og noen ikke. Selve uttrykket for lambda-kalkulen kalles "lambda-begrepet".
De følgende tre reglene gir en induktiv definisjon som kan væregjelder for konstruksjonen av alle syntaktisk gyldige konsepter:
X-variabelen i seg selv er en gyldig lambda-term:
- hvis T er LT og x er ikke-konstant, kalles (lambda xt) en abstraksjon.
- hvis T så vel som s er begreper, kalles (TS) en applikasjon.
Ingenting annet er et lambdabegrep. Dermed er et konsept gyldig hvis og bare hvis det kan oppnås ved gjentatt anvendelse av disse tre reglene. Noen parenteser kan imidlertid utelates i henhold til andre kriterier.
Definition
Lambda-uttrykk består av:
- variabler v 1, v 2, …, v n, …
- symboler for abstraksjon 'λ' og prikk '.'
- parentes ().
Sammen Λ kan defineres induktivt:
- Hvis x er en variabel, så x ∈ Λ;
- x er ikke konstant og M ∈ Λ, da (λx. M) ∈ Λ;
- M, N ∈ Λ, deretter (MN) ∈ Λ.
Betegnelse
For å holde notasjonen til lambda-uttrykk ryddig, er følgende konvensjoner ofte brukt:
- Ytre parentes utelatt: MN i stedet for (MN).
- Applikasjoner antas å forbli assosiative: man kan skrive MNP i stedet for ((MN) P).
- Astraksjonskroppen strekker seg lenger til høyre: λx. MN betyr λx. (MN), ikke (λx. M) N.
- Rekkefølgen av abstraksjoner er redusert: λx.λy.λz. N kan være λxyz. N.
Fri og bundne variabler
Operatøren λ kobler sammen sin ikke-konstant uansett hvor den er i abstraksjonskroppen. Variabler som faller inn under omfanget kalles bundet. I uttrykket λ x. M, λ x-delen blir ofte referert til som et bindemiddel. Som om å antyde at variablene blir en gruppe med tillegg av X x til M. Alle andre ustabile kalles gratis.
For eksempel i uttrykket λ y. x x y, y - bundet ikke-permanent, og x - fri. Og det er også verdt å merke seg at variabelen er gruppert etter sin "nærmeste" abstraksjon. I det følgende eksempelet er lambdakalkulusløsningen representert av en enkelt forekomst av x, som er relatert til det andre leddet:
λ x. y (λ x. z x)
Settet med frie variabler M er betegnet som FV (M) og er definert av rekursjon over strukturen av ledd som følger:
- FV (x)={x}, der x er en variabel.
- FV (λx. M)=FV (M) {x}.
- FV (MN)=FV (M) ∪ FV (N).
En formel som ikke inneholder frie variabler kalles lukket. Lukkede lambda-uttrykk er også kjent som kombinatorer og tilsvarer termer i kombinatorisk logikk.
Forkortelse
Betydningen av lambda-uttrykk bestemmes av hvordan de kan forkortes.
Det finnes tre typer kutt:
- α-transform: endre bundne variabler (alfa).
- β-reduksjon: å bruke funksjoner på argumentene deres (beta).
- η-transform: dekker begrepet ekstensjonalitet.
Her er den ogsåvi snakker om de resulterende ekvivalensene: to uttrykk er β-ekvivalente hvis de kan β-transformeres til samme komponent, og α / η-ekvivalens er definert på samme måte.
Begrepet redex, forkortelse for redusible turnover, refererer til underemner som kan reduseres med en av reglene. Lambdaregning for dummies, eksempler:
(λ x. M) N er en beta-redeks i uttrykket for å erstatte N med x i M. Komponenten som en redeks reduserer til kalles dens redukt. Reduksjonen (λ x. M) N er M [x:=N].
Hvis x ikke er ledig i M, λ x. M x også em-REDEX med regulator M.
α-transformation
Alpha renames lar deg endre navnene på bundne variabler. For eksempel, x. x kan gi λ y. y. Termer som bare er forskjellige i alfa-transformasjon sies å være α-ekvivalente. Ofte, når du bruker lambda-regningen, anses α-ekvivalenter som gjensidige.
De nøyaktige reglene for alfakonvertering er ikke helt trivielle. For det første, med denne abstraksjonen, får bare de variablene som er assosiert med det samme systemet nytt navn. For eksempel alfatransformasjonen λ x.λ x. x kan føre til λ y.λ x. x, men dette fører kanskje ikke til λy.λx.y Sistnevnte har en annen betydning enn originalen. Dette er analogt med konseptet med variabel skyggeprogrammering.
For det andre er en alfatransformasjon ikke mulig hvis den ville resultere i å bli fanget opp av en ikke-permanent annen abstraksjon. For eksempel, hvis du erstatter x med y i λ x.λ y. x, så kan du fåλy.λy. u, som ikke er det samme i det hele tatt.
I programmeringsspråk med statisk omfang kan alfakonvertering brukes til å forenkle navneoppløsning. Pass samtidig på at konseptet med en variabel ikke maskerer betegnelsen i det inneholdende området.
I De Bruyne-indeksnotasjonen er to alfa-ekvivalente termer syntaktisk identiske.
Replacement
Endringene skrevet av E [V:=R] er prosessen med å erstatte alle frie forekomster av variabelen V i uttrykket E med omsetningen R. Substitusjon i form av λ er definert av lambdaen til rekursjonen kalkuler på konseptstrukturen som følger (merk: x og y - kun variabler, og M og N - ethvert λ-uttrykk).
x [x:=N] ≡ N
y [x:=N] ≡ y if 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]) hvis x ≠ y, forutsatt at y ∉ FV (N).
For substitusjon til en lambdaabstraksjon er det noen ganger nødvendig å α-transformere et uttrykk. For eksempel er det ikke sant at (λ x. Y) [y:=x] resulterer i (λ x. X) fordi den substituerte x burde vært fri, men endte opp med å bli bundet. Riktig erstatning i dette tilfellet er (λ z. X) opp til α-ekvivalens. Merk at substitusjon er unikt definert opp til lambda.
β-reduksjon
Beta-reduksjon gjenspeiler ideen om å bruke en funksjon. Beta-reduktiv er definert i termererstatning: ((X V. E) E ') er E [V:=E'].
For eksempel, hvis du antar en eller annen koding 2, 7, ×, er det følgende β-reduksjon: ((λ n. N × 2) 7) → 7 × 2.
Beta-reduksjon kan sees på som det samme som konseptet med lokal reduserbarhet under naturlig deduksjon via Curry-Howard-isomorfismen.
η-transform
Denne konverteringen uttrykker ideen om ekstensjonalitet, som i denne sammenheng er at to funksjoner er like når de gir samme resultat for alle argumenter. Denne konverteringen veksler mellom λ x. (F x) og f når x ikke virker ledig i f.
Denne handlingen kan betraktes som det samme som konseptet med lokal fullstendighet i naturlig deduksjon gjennom Curry-Howard-isomorfismen.
Vanlige former og fusjon
For en utype lambda-regning er β-reduksjonsregelen generelt verken sterk eller svak normaliserende.
Likevel kan det vises at β-reduksjonen smelter sammen når den kjøres før α-transformasjonen (dvs. to normalformer kan anses like hvis en α-transformasjon fra den ene til den andre er mulig).
Derfor har både sterkt normaliserende termer og svakt justerende termer én normalform. For de første vilkårene vil enhver reduksjonsstrategi garantert resultere i en typisk konfigurasjon. Mens for svakt normaliserende forhold kan det hende at enkelte reduksjonsstrategier ikke finner det.
Ytterligere programmeringsmetoder
Det er mange skapelsesspråk for lambda-regningen. Mange av dem ble opprinnelig utviklet i sammenheng med å bruke systemer som grunnlag for semantikken til et programmeringsspråk, og effektivt anvende dem som en lavnivåkonstruksjon. Siden noen stiler inkluderer en lambda-kalkulus (eller noe lignende) som et utdrag, finner disse teknikkene også bruk i praktisk skapelse, men kan da oppfattes som uklare eller fremmede.
Navngivne konstanter
I lambda-regning har et bibliotek form av et sett med tidligere definerte funksjoner, der begrepene bare er konkrete konstanter. Ren kalkulus har ikke noe begrep om navngitte uforanderlige siden alle atomære lambda-termer er variabler. Men de kan også etterlignes ved å ta det foranderlige som navnet på konstanten, bruke en lambdaabstraksjon for å binde det flyktige i kroppen, og bruke den abstraksjonen til den tiltenkte definisjonen. Så hvis du bruker f for å representere M i N, kan du si
(λ f. N) M.
Forfattere introduserer ofte et syntaktisk konsept som å la ting skrives på en mer intuitiv måte.
f=M til N
Ved å kjede sammen slike definisjoner kan man skrive en lambdakalkulus "program" som null eller flere funksjonsdefinisjoner etterfulgt av et enkelt lambdamedlem, ved å bruke de definisjonene som utgjør hoveddelen av programmet.
En bemerkelsesverdig begrensning av denne låten er at navnet f ikke er definert i M,siden M er utenfor det bindende omfanget av lambda-abstraksjonen f. Dette betyr at et rekursivt funksjonsattributt ikke kan brukes som M med let. Den mer avanserte letrec-syntaksen, som lar deg skrive rekursive funksjonsdefinisjoner i denne stilen, bruker i tillegg fastpunktskombinatorer i stedet.
Trykte analoger
Denne typen er en maskinskrevet formalisme som bruker et symbol for å representere en anonym funksjonsabstraksjon. Typer er i denne sammenheng vanligvis objekter av syntaktisk karakter som er tilordnet lambda-termer. Den nøyaktige arten avhenger av den aktuelle kalkulen. Fra et visst synspunkt kan typet LI betraktes som forbedringer av utypet LI. Men på den annen side kan de også betraktes som en mer fundamental teori, og den utypede lambda-regningen er et spesi altilfelle med bare én type.
Typet LI er grunnlaget for programmeringsspråk og ryggraden i funksjonelle språk som ML og Haskell. Og, mer indirekte, imperative skapelsesstiler. Maskinskrevne lambdaregninger spiller en viktig rolle i utviklingen av typesystemer for programmeringsspråk. Her fanger skrivbarhet vanligvis de ønskede egenskapene til programmet, for eksempel vil det ikke forårsake brudd på minnetilgangen.
Typede lambda-beregninger er nært beslektet med matematisk logikk og bevisteori gjennom Curry–Howard-isomorfismen, og kan betraktes som et internt språk i kategoriklasser, som f.eks.er ganske enkelt stilen til kartesiske nedleggelser.
