Lambda-kalkyl är ett formellt system inom matematisk logik för att uttrycka abstraktionsbaserade beräkningar och tillämpa funktioner med bindning och variabelsubstitution. Detta är en universell modell som kan appliceras på designen av vilken Turing-maskin som helst. Lambdakalkylen introducerades först av Church, en berömd matematiker, på 1930-talet.
Systemet består av att bygga lambdaelement och utföra reduktionsoperationer på dem.
Förklaringar och tillämpningar
Den grekiska bokstaven lambda (λ) används i lambda-uttryck och lambda-termer för att beteckna bindningen av en variabel i en funktion.
Lambda-kalkyl kan vara oskriven eller maskinskriven. I den första varianten kan funktioner endast användas om de kan ta emot data av denna typ. Typade lambdakalkyler är svagare, kan uttrycka ett mindre värde. Men å andra sidan låter de dig bevisa fler saker.
En anledning till att det finns så många olika typer är forskarnas önskan att göra mer utan att ge upp möjligheten att bevisa starka lambdakalkylsatser.
Systemet har applikationer inom många olika områden inom matematik, filosofi, lingvistik och datavetenskap. För det första är lambdakalkylen en kalkyl som har spelat en viktig roll i utvecklingen av teorin om programmeringsspråk. Det är stilarna för funktionellt skapande som systemen implementerar. De är också ett hett ämne för forskning inom teorin för dessa kategorier.
För dummies
Lambdakalkylen introducerades av matematikern Alonzo Church på 1930-talet som en del av hans forskning om vetenskapens grunder. Det ursprungliga systemet visade sig vara logiskt inkonsekvent 1935 när Stephen Kleen och J. B. Rosser utvecklade Kleene-Rosser-paradoxen.
Senare, 1936, pekade Church ut och publicerade endast den del som är relevant för beräkningar, det som nu kallas den otypade lambdakalkylen. 1940 introducerade han också en svagare men logiskt konsekvent teori som kallas prime type system. I sitt arbete förklarar han hela teorin i enkla termer, så man kan säga att kyrkan publicerade kalkylen lambda för dummies.
Fram till 1960-talet, när dess relation till programmeringsspråk blev tydlig, var λ bara en formalism. Tack vare Richard Montagu och andra lingvisters tillämpningar inom det naturliga språkets semantik har kalkyl tagit en stor plats inom både lingvistik och datavetenskap.
Ursprunget till symbolen
Lambda står inte för ett ord eller en akronym, det kommer från en referens i Russells Principal Mathematics följt av två typografiska ändringar. Notationsexempel: för en funktion f med f (y)=2y + 1 är 2ŷ + 1. Och här använder vi en karet ("hatt") över y för att märka indatavariabeln.
Kyrkan hade ursprungligen tänkt att använda liknande symboler, men sättare kunde inte placera "hatt"-symbolen ovanför bokstäverna. Så istället skrev de det ursprungligen som "/\y.2y+1". I nästa avsnitt av redigering ersatte maskinskrivare "/ \" med en visuellt liknande karaktär.
Introduktion till lambdakalkyl
Systemet består av ett språk av termer, som väljs av en viss formell syntax, och en uppsättning transformationsregler som gör att de kan manipuleras. Den sista punkten kan betraktas som en ekvationsteori eller som en operationell definition.
Alla funktioner i lambdakalkylen är anonyma, vilket betyder att de inte har namn. De tar bara en indatavariabel och currying används för att implementera plotter med flera variabler.
Lambda-villkor
Kalkylsyntaxen definierar vissa uttryck som giltiga och andra som ogiltiga. Precis som olika teckensträngar är giltiga C-program och vissa inte. Det faktiska uttrycket för lambdakalkylen kallas "lambdatermen".
Följande tre regler ger en induktiv definition som kan varatillämpas på konstruktionen av alla syntaktiskt giltiga begrepp:
X-variabeln i sig är en giltig lambdaterm:
- om T är LT och x är icke-konstant, kallas (lambda xt) en abstraktion.
- om T såväl som s är begrepp, kallas (TS) en applikation.
Inget annat är en lambdaterm. Ett begrepp är alltså giltigt om och endast om det kan erhållas genom upprepad tillämpning av dessa tre regler. Vissa parenteser kan dock utelämnas enligt andra kriterier.
Definition
Lambda-uttryck består av:
- variabler v 1, v 2, …, v n, …
- symboler för abstraktion 'λ' och punkt '.'
- parentes ().
Mängden Λ kan definieras induktivt:
- Om x är en variabel, då x ∈ Λ;
- x är inte konstant och M ∈ Λ, då (λx. M) ∈ Λ;
- M, N ∈ Λ, sedan (MN) ∈ Λ.
Beteckning
Följande konventioner används vanligtvis för att hålla notationen av lambda-uttryck ren:
- Ytterparenteser utelämnade: MN istället för (MN).
- Applikationer antas förbli associativa: man kan skriva MNP istället för ((MN) P).
- Abstraktionskroppen sträcker sig längre till höger: λx. MN betyder λx. (MN), inte (λx. M) N.
- Sekvensen av abstraktioner reduceras: λx.λy.λz. N kan vara λxyz. N.
Fri och bundna variabler
Operatorn λ ansluter sin icke-konstant var den än befinner sig i abstraktionskroppen. Variabler som faller inom räckvidden kallas bundna. I uttrycket λ x. M, λ x-delen kallas ofta för ett bindemedel. Som om att antyda att variablerna blir en grupp med tillägg av X x till M. Alla andra instabila kallas fria.
Till exempel i uttrycket λ y. x x y, y - bundet icke-permanent och x - fri. Och det är också värt att notera att variabeln är grupperad efter sin "närmaste" abstraktion. I följande exempel representeras lambdakalkyllösningen av en enda förekomst av x, som är relaterad till den andra termen:
λ x. y (λ x. z x)
Mängden fria variabler M betecknas som FV (M) och definieras av rekursion över termernas struktur enligt följande:
- FV (x)={x}, där x är en variabel.
- FV (λx. M)=FV (M) {x}.
- FV (MN)=FV (M) ∪ FV (N).
En formel som inte innehåller fria variabler kallas sluten. Slutna lambda-uttryck är också kända som kombinatorer och är ekvivalenta med termer i kombinatorisk logik.
Förkortning
Betydelsen av lambda-uttryck bestäms av hur de kan förkortas.
Det finns tre typer av snitt:
- α-transform: ändra bundna variabler (alfa).
- β-reduktion: tillämpa funktioner på deras argument (beta).
- η-transform: täcker begreppet extensionalitet.
Här är den ocksåvi talar om de resulterande ekvivalenserna: två uttryck är β-ekvivalenta om de kan β-transformeras till samma komponent, och α / η-ekvivalens definieras på liknande sätt.
Termen redex, kort för reducerbar omsättning, syftar på underämnen som kan reduceras med någon av reglerna. Lambdakalkyl för dummies, exempel:
(λ x. M) N är en beta-redex i uttrycket för att ersätta N med x i M. Komponenten som en redex reducerar till kallas dess redukt. Reduktionen (λ x. M) N är M [x:=N].
Om x inte är ledig i M, λ x. M x även em-REDEX med regulator M.
α-transformation
Alpha renames låter dig ändra namnen på bundna variabler. Till exempel, x. x kan ge λ y. y. Termer som skiljer sig endast i alfatransformation sägs vara α-ekvivalenta. Ofta, när man använder lambdakalkylen, anses α-ekvivalenter vara ömsesidiga.
De exakta reglerna för alfakonvertering är inte helt triviala. För det första, med denna abstraktion, byts bara de variabler som är associerade med samma system om. Till exempel alfatransformen λ x.λ x. x kan leda till λ y.λ x. x, men detta kanske inte leder till λy.λx.y Det senare har en annan betydelse än originalet. Detta är analogt med konceptet med variabel skuggningsprogrammering.
För det andra är en alfatransform inte möjlig om den skulle resultera i att den fångas upp av en icke-permanent annan abstraktion. Till exempel, om du ersätter x med y i λ x.λ y. x, då kan du fåλy.λy. u, vilket inte alls är detsamma.
I programmeringsspråk med statisk omfattning kan alfakonvertering användas för att förenkla namnupplösning. Se samtidigt till att begreppet variabel inte maskerar beteckningen i det innehållande området.
I De Bruyne-indexnotation är två valfria alfa-ekvivalenta termer syntaktiskt identiska.
Ersättning
Ändringarna som skrivs av E [V:=R] är processen att ersätta alla fria förekomster av variabeln V i uttrycket E med omsättningen R. Substitution i termer av λ definieras av lambda för rekursionen beräkning av begreppsstrukturen enligt följande (obs: x och y - endast variabler, och M och N - valfritt λ-uttryck).
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]) om x ≠ y, förutsatt att y ∉ FV (N).
För substitution till en lambdaabstraktion är det ibland nödvändigt att α-transformera ett uttryck. Till exempel är det inte sant att (λ x. Y) [y:=x] resulterar i (λ x. X) eftersom det substituerade x borde ha varit fritt, men slutade med att vara bundet. Den korrekta ersättningen i detta fall är (λ z. X) upp till α-ekvivalens. Observera att substitution är unikt definierad upp till lambda.
β-reduction
Beta-reduktion återspeglar idén med att använda en funktion. Beta-reduktiv definieras i termersubstitution: ((X V. E) E ') är E [V:=E'].
Om man till exempel antar någon kodning 2, 7, ×, finns det följande β-reduktion: ((λ n. N × 2) 7) → 7 × 2.
Beta-reduktion kan ses som samma som konceptet med lokal reducerbarhet under naturligt deduktion via Curry-Howard-isomorfismen.
η-transform
Denna omvandling uttrycker idén om extensionalitet, som i detta sammanhang är att två funktioner är lika när de ger samma resultat för alla argument. Denna omvandling växlar mellan λ x. (F x) och f när x inte verkar fritt i f.
Denna åtgärd kan betraktas som samma som konceptet med lokal fullständighet i naturlig deduktion genom Curry-Howard-isomorfismen.
Normala former och fusion
För en otypad lambdakalkyl är β-reduktionsregeln i allmänhet varken stark eller svag normaliserande.
Ändå kan det visas att β-reduktionen smälter samman när den körs före α-transformationen (dvs två normalformer kan anses lika om en α-transformation från den ena till den andra är möjlig).
Därför har både starkt normaliserande termer och svagt justerande termer en enda normalform. För de första termerna kommer varje reduktionsstrategi garanterat att resultera i en typisk konfiguration. Medan för svagt normaliserande förhållanden kanske vissa reduktionsstrategier inte hittar det.
Ytterligare programmeringsmetoder
Det finns många skapande idiom för lambdakalkylen. Många av dem utvecklades ursprungligen i sammanhanget med att använda system som grund för semantiken i ett programmeringsspråk, och effektivt tillämpa dem som en lågnivåkonstruktion. Eftersom vissa stilar inkluderar en lambda-kalkyl (eller något liknande) som ett utdrag, kan dessa tekniker även användas i praktiskt skapande, men kan då uppfattas som oklara eller främmande.
Namnställda konstanter
I lambdakalkyl tar ett bibliotek formen av en uppsättning tidigare definierade funktioner, där termerna bara är konkreta konstanter. Ren kalkyl har inget koncept för namngivna oföränderliga eftersom alla atomära lambda-termer är variabler. Men de kan också efterliknas genom att ta det föränderliga som namnet på konstanten, använda en lambdaabstraktion för att binda det flyktiga i kroppen och tillämpa den abstraktionen på den avsedda definitionen. Så om du använder f för att representera M i N kan du säga
(λ f. N) M.
Författare introducerar ofta ett syntaktisk koncept som att låta saker skrivas på ett mer intuitivt sätt.
f=M till N
Genom att kedja sådana definitioner kan man skriva en lambdakalkyl "program" som noll eller fler funktionsdefinitioner följt av en enda lambdamedlem, med hjälp av de definitioner som utgör huvuddelen av programmet.
En anmärkningsvärd begränsning av denna låt är att namnet f inte är definierat i M,eftersom M ligger utanför det bindande omfånget för lambdaabstraktionen f. Detta innebär att ett rekursivt funktionsattribut inte kan användas som M med let. Den mer avancerade letrec-syntaxen, som låter dig skriva rekursiva funktionsdefinitioner i denna stil, använder dessutom fixpunktskombinatorer istället.
Tryckta analoger
Den här typen är en maskinskriven formalism som använder en symbol för att representera en anonym funktionsabstraktion. Typer är i detta sammanhang vanligtvis objekt av syntaktisk karaktär som tilldelas lambda-termer. Den exakta naturen beror på kalkylen i fråga. Ur en viss synvinkel kan typad LI betraktas som förfining av otypad LI. Men å andra sidan kan de också betraktas som en mer fundamental teori, och den otypade lambdakalkylen är ett specialfall med bara en typ.
Typade LI är grunden för programmeringsspråk och ryggraden i funktionella språk som ML och Haskell. Och, mer indirekt, imperativa skapelsestilar. Maskinskrivna lambdakalkyler spelar en viktig roll i utvecklingen av typsystem för programmeringsspråk. Här fångar typbarhet vanligtvis de önskade egenskaperna hos programmet, till exempel kommer det inte att orsaka minnesåtkomstbrott.
Typade lambda-kalkyler är nära besläktade med matematisk logik och bevisteori genom Curry–Howard-isomorfismen, och kan ses som ett internt språk för kategoriklasser, som till exempelhelt enkelt är stilen med kartesiska stängningar.
