Lambda-regning er et formelt system i matematisk logik til at udtrykke abstraktionsbaserede beregninger og anvende funktioner ved hjælp af binding og variabel substitution. Dette er en universel model, der kan anvendes til designet af enhver Turing-maskine. Lambdaregningen blev først introduceret af Church, en berømt matematiker, i 1930'erne.
Systemet består af at bygge lambda-elementer og udføre reduktionsoperationer på dem.
Forklaringer og applikationer
Det græske bogstav lambda (λ) bruges i lambda-udtryk og lambda-udtryk for at angive bindingen af en variabel i en funktion.
Lambda-kalkulus kan være utype eller indtastet. I den første variant kan funktioner kun bruges, hvis de er i stand til at modtage data af denne type. Indskrevne lambdaregninger er svagere, kan udtrykke en mindre værdi. Men på den anden side giver de dig mulighed for at bevise flere ting.
En grund til, at der er så mange forskellige typer, er videnskabsmænds ønske om at gøre mere uden at give afkald på muligheden for at bevise stærke lambda-regningssætninger.
Systemet har applikationer inden for mange forskellige områder inden for matematik, filosofi, lingvistik og datalogi. Først og fremmest er lambda-regningen en beregning, der har spillet en vigtig rolle i udviklingen af teorien om programmeringssprog. Det er stilene til funktionel skabelse, som systemerne implementerer. De er også et varmt emne for forskning i teorien om disse kategorier.
For dummies
Lambda-regningen blev introduceret af matematikeren Alonzo Church i 1930'erne som en del af hans forskning i videnskabens grundlag. Det originale system viste sig at være logisk inkonsekvent i 1935, da Stephen Kleen og J. B. Rosser udviklede Kleene-Rosser-paradokset.
Senere, i 1936, udpegede og offentliggjorde Church kun den del, der er relevant for beregninger, det, der nu kaldes den utyperede lambdaregning. I 1940 introducerede han også en svagere, men logisk konsistent teori kendt som prime type system. I sit arbejde forklarer han hele teorien i enkle vendinger, så det kan siges, at Church udgav lambda-calculus for dummies.
Indtil 1960'erne, hvor dets forhold til programmeringssprog blev tydeligt, var λ blot en formalisme. Takket være Richard Montagu og andre lingvisters anvendelser inden for det naturlige sprogs semantik har calculus taget en ære i både lingvistik og datalogi.
Oprindelse af symbolet
Lambda står ikke for et ord eller akronym, det kommer fra en reference i Russells Principal Mathematics efterfulgt af to typografiske ændringer. Notationseksempel: for en funktion f med f (y)=2y + 1 er 2ŷ + 1. Og her bruger vi en streg ("hat") over y til at mærke inputvariablen.
Kirken havde oprindeligt til hensigt at bruge lignende symboler, men sætterne var ikke i stand til at placere "hat"-symbolet over bogstaverne. Så i stedet udskrev de det oprindeligt som "/\y.2y+1". I næste afsnit af redigering erstattede maskinskrivere "/ \" med en visuelt lignende karakter.
Introduktion til lambdaregning
Systemet består af et sprog af termer, som er valgt af en bestemt formel syntaks, og et sæt transformationsregler, der tillader dem at blive manipuleret. Det sidste punkt kan betragtes som en ligningsteori eller som en operationel definition.
Alle funktioner i lambda-regningen er anonyme, hvilket betyder, at de ikke har navne. De tager kun én inputvariabel, og currying bruges til at implementere plots med flere variabler.
Lambda-vilkår
Kalkylesyntaksen definerer nogle udtryk som gyldige og andre som ugyldige. Ligesom forskellige strenge af tegn er gyldige C-programmer, og nogle er ikke. Det egentlige udtryk for lambdaregningen kaldes "lambda-udtrykket".
De følgende tre regler giver en induktiv definition, der kan væregælder for konstruktionen af alle syntaktisk gyldige begreber:
Selve x-variablen er en gyldig lambda-term:
- hvis T er LT og x er ikke-konstant, så kaldes (lambda xt) en abstraktion.
- hvis T såvel som s er begreber, så kaldes (TS) en applikation.
Intet andet er et lambdaudtryk. Et begreb er således gyldigt, hvis og kun hvis det kan opnås ved gentagen anvendelse af disse tre regler. Nogle parenteser kan dog udelades i henhold til andre kriterier.
Definition
Lambda-udtryk består af:
- variabler v 1, v 2, …, v n, …
- symboler for abstraktion 'λ' og prik '.'
- parentes ().
Sættet Λ kan defineres induktivt:
- Hvis x er en variabel, så x ∈ Λ;
- x er ikke konstant og M ∈ Λ, så (λx. M) ∈ Λ;
- M, N ∈ Λ, derefter (MN) ∈ Λ.
Betegnelse
For at holde notationen af lambda-udtryk overskuelig, bruges følgende konventioner almindeligvis:
- Ydre parenteser udeladt: MN i stedet for (MN).
- Applikationer antages at forblive associative: man kan skrive MNP i stedet for ((MN) P).
- Abstraktionens krop strækker sig længere til højre: λx. MN betyder λx. (MN), ikke (λx. M) N.
- Rækkefølgen af abstraktioner er reduceret: λx.λy.λz. N kan være λxyz. N.
Fri og bundne variable
Operatoren λ forbinder sin ikke-konstant, uanset hvor den er i abstraktionskroppen. Variabler, der falder ind under anvendelsesområdet, kaldes bundne. I udtrykket λ x. M, λ x-delen omtales ofte som et bindemiddel. Som om at antyde, at variablerne bliver en gruppe med tilføjelse af X x til M. Alle andre ustabile kaldes frie.
For eksempel i udtrykket λ y. x x y, y - bundet ikke-permanent og x - fri. Og det er også værd at bemærke, at variablen er grupperet efter sin "nærmeste" abstraktion. I det følgende eksempel er lambdaregningsløsningen repræsenteret af en enkelt forekomst af x, som er relateret til det andet led:
λ x. y (λ x. z x)
Sættet af frie variabler M er betegnet som FV (M) og er defineret ved rekursion over strukturen af led som følger:
- FV (x)={x}, hvor x er en variabel.
- FV (λx. M)=FV (M) {x}.
- FV (MN)=FV (M) ∪ FV (N).
En formel, der ikke indeholder frie variabler, kaldes lukket. Lukkede lambda-udtryk er også kendt som kombinatorer og svarer til termer i kombinatorisk logik.
Forkortelse
Betydningen af lambda-udtryk bestemmes af, hvordan de kan forkortes.
Der er tre typer snit:
- α-transform: ændring af bundne variabler (alfa).
- β-reduktion: anvendelse af funktioner på deres argumenter (beta).
- η-transform: dækker begrebet ekstensionalitet.
Her er den ogsåvi taler om de resulterende ækvivalenser: to udtryk er β-ækvivalente, hvis de kan β-transformeres til den samme komponent, og α / η-ækvivalens er defineret på samme måde.
Udtrykket redex, en forkortelse for reducerbar omsætning, henviser til underemner, der kan reduceres med en af reglerne. Lambdaregning for dummies, eksempler:
(λ x. M) N er en beta redex i udtrykket for at erstatte N med x i M. Komponenten, som en redex reducerer til, kaldes dens redukt. Reduktionen (λ x. M) N er M [x:=N].
Hvis x ikke er fri i M, λ x. M x også em-REDEX med regulator M.
α-transformation
Alpha-omdøbninger giver dig mulighed for at ændre navnene på bundne variabler. For eksempel, x. x kan give λ y. y. Udtryk, der kun adskiller sig i alfa-transformation, siges at være α-ækvivalente. Ofte, når man bruger lambda-regningen, betragtes α-ækvivalenter som gensidige.
De nøjagtige regler for alfakonvertering er ikke helt trivielle. For det første, med denne abstraktion, omdøbes kun de variabler, der er forbundet med det samme system. For eksempel alfa-transformationen λ x.λ x. x kan føre til λ y.λ x. x, men det fører måske ikke til λy.λx.y Sidstnævnte har en anden betydning end originalen. Dette er analogt med konceptet med variabel skyggeprogrammering.
For det andet er en alfatransformation ikke mulig, hvis den ville resultere i at blive fanget af en ikke-permanent anden abstraktion. For eksempel, hvis du erstatter x med y i λ x.λ y. x, så kan du fåλy.λy. u, hvilket slet ikke er det samme.
I programmeringssprog med statisk omfang kan alfakonvertering bruges til at forenkle navneopløsning. Samtidig skal man passe på, at begrebet variabel ikke maskerer betegnelsen i det indeholdende område.
I De Bruyne-indeksnotation er to alfa-ækvivalente udtryk syntaktisk identiske.
Erstatning
Ændringerne skrevet af E [V:=R] er processen med at erstatte alle frie forekomster af variablen V i udtrykket E med omsætningen R. Substitution i form af λ er defineret af lambdaen for rekursionen beregning af begrebsstrukturen som følger (bemærk: x og y - kun variable, og M og N - ethvert λ-udtryk).
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, forudsat at y ∉ FV (N).
For substitution til en lambda-abstraktion er det nogle gange nødvendigt at α-transformere et udtryk. For eksempel er det ikke rigtigt, at (λ x. Y) [y:=x] resulterer i (λ x. X), fordi den substituerede x skulle have været fri, men endte med at blive bundet. Den korrekte erstatning i dette tilfælde er (λ z. X) op til α-ækvivalens. Bemærk, at substitution er unikt defineret op til lambda.
β-reduktion
Beta-reduktion afspejler ideen om at anvende en funktion. Beta-reduktiv er defineret i termersubstitution: ((X V. E) E ') er E [V:=E'].
For eksempel, hvis man antager en kodning 2, 7, ×, er der følgende β-reduktion: ((λ n. N × 2) 7) → 7 × 2.
Beta-reduktion kan ses som det samme som begrebet lokal reduktion under naturlig deduktion via Curry-Howard-isomorfismen.
η-transform
Denne konvertering udtrykker ideen om ekstensionalitet, som i denne sammenhæng er, at to funktioner er ens, når de giver det samme resultat for alle argumenter. Denne konvertering udveksler mellem λ x. (F x) og f, når x ikke synes fri i f.
Denne handling kan betragtes som det samme som konceptet om lokal fuldstændighed i naturlig deduktion gennem Curry-Howard-isomorfi.
Normale former og fusion
For en utypebestemt lambdaregning er β-reduktionsreglen generelt hverken stærk eller svag normaliserende.
Alligevel kan det påvises, at β-reduktionen smelter sammen, når den kører før α-transformationen (dvs. to normalformer kan betragtes som ens, hvis en α-transformation fra den ene til den anden er mulig).
Derfor har både stærkt normaliserende termer og svagt justerende led en enkelt normalform. For de første termer er enhver reduktionsstrategi garanteret at resultere i en typisk konfiguration. Mens nogle reduktionsstrategier muligvis ikke finder det for svagt normaliserende forhold.
Yderligere programmeringsmetoder
Der er mange skabelsessprog til lambda-regningen. Mange af dem blev oprindeligt udviklet i sammenhæng med at bruge systemer som grundlag for semantikken i et programmeringssprog, og effektivt anvende dem som en konstruktion på lavt niveau. Da nogle stilarter inkluderer en lambdaregning (eller noget meget lignende) som et uddrag, finder disse teknikker også anvendelse i praktisk skabelse, men kan så opfattes som uklare eller fremmede.
Navngivne konstanter
I lambda-regning har et bibliotek form af et sæt af tidligere definerede funktioner, hvor termerne blot er konkrete konstanter. Ren calculus har intet begreb om navngivne uforanderlige, da alle atomare lambda-udtryk er variable. Men de kan også efterlignes ved at tage det foranderlige som navnet på konstanten, bruge en lambdaabstraktion til at binde det flygtige i kroppen og anvende denne abstraktion til den tilsigtede definition. Så hvis du bruger f til at repræsentere M i N, kan du sige
(λ f. N) M.
Forfattere introducerer ofte et syntaktisk koncept, såsom lad for at tillade ting at blive skrevet på en mere intuitiv måde.
f=M til N
Ved at sammenkæde sådanne definitioner kan man skrive et lambda-kalkulus-"program" som nul eller flere funktionsdefinitioner efterfulgt af et enkelt lambda-medlem ved at bruge de definitioner, der udgør hovedparten af programmet.
En bemærkelsesværdig begrænsning ved dette let er, at navnet f ikke er defineret i M,da M er uden for lambdaabstraktionens bindingsområde f. Det betyder, at en rekursiv funktionsattribut ikke kan bruges som M med let. Den mere avancerede letrec-syntaks, som giver dig mulighed for at skrive rekursive funktionsdefinitioner i denne stil, bruger i stedet fikspunktskombinatorer.
Trykte analoger
Denne type er en maskinskrevet formalisme, der bruger et symbol til at repræsentere en anonym funktionsabstraktion. Typer er i denne sammenhæng norm alt objekter af syntaktisk karakter, der tildeles lambda-termer. Den nøjagtige karakter afhænger af den pågældende regning. Fra et bestemt synspunkt kan typebestemt LI betragtes som justeringer af utypebestemt LI. Men på den anden side kan de også betragtes som en mere fundamental teori, og den utyperede lambdaregning er et speci altilfælde med kun én type.
Typede LI er grundlaget for programmeringssprog og rygraden i funktionelle sprog som ML og Haskell. Og mere indirekte imperative skabelsesstile. Indskrevne lambdaregninger spiller en vigtig rolle i udviklingen af typesystemer til programmeringssprog. Her fanger typabilitet norm alt de ønskede egenskaber for programmet, for eksempel vil det ikke forårsage en hukommelsesadgangskrænkelse.
Typede lambdaregning er tæt beslægtet med matematisk logik og bevisteori gennem Curry-Howard isomorfismen og kan opfattes som et internt sprog i kategoriklasser, som f.eks.er simpelthen stilen med kartesiske lukninger.
