Lambda-calculus is een formeel systeem in wiskundige logica voor het uitdrukken van op abstractie gebaseerde berekeningen en het toepassen van functies met behulp van binding en variabele substitutie. Dit is een universeel model dat kan worden toegepast op het ontwerp van elke Turing-machine. De lambda-calculus werd voor het eerst geïntroduceerd door Church, een beroemde wiskundige, in de jaren 1930.
Het systeem bestaat uit het bouwen van lambda-leden en het uitvoeren van reductiebewerkingen op hen.
Uitleg en toepassingen
De Griekse letter lambda (λ) wordt gebruikt in lambda-uitdrukkingen en lambda-termen om de binding van een variabele in een functie aan te duiden.
Lambda-calculus kan ongetypt of getypt zijn. In de eerste variant kunnen functies alleen worden gebruikt als ze dit soort gegevens kunnen ontvangen. Getypte lambda calculi zijn zwakker, kunnen een kleinere waarde uitdrukken. Maar aan de andere kant stellen ze je in staat om meer dingen te bewijzen.
Een reden waarom er zoveel verschillende soorten zijn, is de wens van wetenschappers om meer te doen zonder de kans op te geven om sterke lambda-rekeningstellingen te bewijzen.
Het systeem heeft toepassingen op veel verschillende gebieden van wiskunde, filosofie, taalkunde en informatica. Allereerst is de lambda-calculus een calculus die een belangrijke rol heeft gespeeld bij de ontwikkeling van de theorie van programmeertalen. Het zijn de stijlen van functionele creatie die systemen implementeren. Ze zijn ook een hot topic van onderzoek in de theorie van deze categorieën.
Voor dummies
De lambda-calculus werd in de jaren dertig geïntroduceerd door de wiskundige Alonzo Church als onderdeel van zijn onderzoek naar de fundamenten van de wetenschap. Het oorspronkelijke systeem bleek in 1935 logisch inconsistent te zijn toen Stephen Kleen en J. B. Rosser de Kleene-Rosser-paradox ontwikkelden.
Later, in 1936, selecteerde en publiceerde Church alleen het deel dat relevant is voor berekeningen, wat nu de ongetypeerde lambda-calculus wordt genoemd. In 1940 introduceerde hij ook een zwakkere maar logisch consistente theorie die bekend staat als het prime-type systeem. In zijn werk legt hij de hele theorie in eenvoudige bewoordingen uit, zodat men kan zeggen dat Church de calculus lambda voor dummies heeft gepubliceerd.
Tot de jaren zestig, toen de relatie met programmeertalen duidelijk werd, was λ slechts een formalisme. Dankzij de toepassingen van Richard Montagu en andere taalkundigen in de semantiek van natuurlijke taal, heeft calculus een prominente plaats ingenomen in zowel de taalkunde als de informatica.
Oorsprong van het symbool
Lambda staat niet voor een woord of acroniem, het komt van een verwijzing in Russell's Principal Mathematics gevolgd door twee typografische veranderingen. Notatievoorbeeld: voor een functie f met f (y)=2y + 1 is 2ŷ + 1. En hier gebruiken we een caret (“hat”) over y om de invoervariabele te labelen.
De kerk was oorspronkelijk van plan soortgelijke symbolen te gebruiken, maar zetters konden het "hoed"-symbool niet boven de letters plaatsen. Dus in plaats daarvan drukten ze het oorspronkelijk af als "/\y.2y+1". In de volgende montage-aflevering vervingen typisten "/ \" door een visueel vergelijkbaar teken.
Inleiding tot lambda-calculus
Het systeem bestaat uit een taal van termen, die worden gekozen door een bepaalde formele syntaxis, en een reeks transformatieregels waarmee ze kunnen worden gemanipuleerd. Het laatste punt kan worden beschouwd als een vergelijkingstheorie of als een operationele definitie.
Alle functies in de lambda-calculus zijn anoniem, wat betekent dat ze geen naam hebben. Ze nemen slechts één invoervariabele en currying wordt gebruikt om plots met meerdere variabelen te implementeren.
Lambda-termen
De calculus-syntaxis definieert sommige uitdrukkingen als geldig en andere als ongeldig. Net zoals verschillende tekenreeksen geldige C-programma's zijn en sommige niet. De eigenlijke uitdrukking van de lambda-calculus wordt de "lambda-term" genoemd.
De volgende drie regels bieden een inductieve definitie die kan zijn:gelden voor de constructie van alle syntactisch geldige concepten:
De x-variabele zelf is een geldige lambda-term:
- als T LT is en x niet-constant is, dan wordt (lambda xt) een abstractie genoemd.
- als T zowel als s concepten zijn, dan wordt (TS) een applicatie genoemd.
Niets anders is een lambda-term. Een concept is dus geldig als en alleen als het kan worden verkregen door herhaalde toepassing van deze drie regels. Sommige haakjes kunnen echter worden weggelaten op basis van andere criteria.
Definitie
Lambda-uitdrukkingen bestaan uit:
- variabelen v 1, v 2, …, v n, …
- symbolen van abstractie 'λ' en punt '.'
- haakjes ().
De verzameling Λ kan inductief worden gedefinieerd:
- Als x een variabele is, dan is x ∈ Λ;
- x is niet constant en M ∈ Λ, dan (λx. M) ∈ Λ;
- M, N ∈ Λ, dan (MN) ∈ Λ.
Aanduiding
Om de notatie van lambda-expressies overzichtelijk te houden, worden de volgende conventies vaak gebruikt:
- Buitenste haakjes weggelaten: MN in plaats van (MN).
- Applicaties worden verondersteld associatief te blijven: men kan MNP schrijven in plaats van ((MN) P).
- De abstractie strekt zich verder naar rechts uit: λx. MN betekent λx. (MN), niet (λx. M) N.
- De volgorde van abstracties wordt gereduceerd: λx.λy.λz. N kan λxyz. N. zijn
Vrije en gebonden variabelen
De operator λ verbindt zijn niet-constante waar deze zich ook bevindt in het lichaam van abstractie. Variabelen die binnen het bereik vallen, worden gebonden genoemd. In de uitdrukking λ x. M, wordt het λ x-deel vaak een bindmiddel genoemd. Alsof het erop wijst dat de variabelen een groep worden met de toevoeging van X x tot M. Alle andere onstabiele worden vrij genoemd.
Bijvoorbeeld in de uitdrukking λ y. x x y, y - gebonden niet-permanent en x - vrij. En het is ook vermeldenswaard dat de variabele is gegroepeerd op zijn "dichtstbijzijnde" abstractie. In het volgende voorbeeld wordt de lambda-calculus-oplossing weergegeven door een enkel exemplaar van x, dat gerelateerd is aan de tweede term:
λ x. y (λ x. z x)
De verzameling vrije variabelen M wordt aangeduid als FV (M) en wordt als volgt gedefinieerd door recursie over de structuur van termen:
- FV (x)={x}, waarbij x een variabele is.
- FV (λx. M)=FV (M) {x}.
- FV (MN)=FV (M) ∪ FV (N).
Een formule die geen vrije variabelen bevat, wordt gesloten genoemd. Gesloten lambda-expressies zijn ook bekend als combinators en zijn equivalent aan termen in combinatorische logica.
Afkorting
De betekenis van lambda-uitdrukkingen wordt bepaald door hoe ze kunnen worden ingekort.
Er zijn drie soorten sneden:
- α-transform: gebonden variabelen wijzigen (alfa).
- β-reductie: functies toepassen op hun argumenten (bèta).
- η-transform: omvat het begrip extensionaliteit.
Hier is het ookwe hebben het over de resulterende equivalenties: twee uitdrukkingen zijn β-equivalent als ze β-getransformeerd kunnen worden in dezelfde component, en α / η-equivalentie wordt op dezelfde manier gedefinieerd.
De term redex, een afkorting voor reduceerbare omzet, verwijst naar subonderwerpen die kunnen worden gereduceerd door een van de regels. Lambda-calculus voor dummies, voorbeelden:
(λ x. M) N is een bèta-redex in de uitdrukking voor het vervangen van N door x in M. De component waartoe een redex reduceert, wordt zijn reduct genoemd. De reductie (λ x. M) N is M [x:=N].
Als x niet vrij is in M, λ x. M x ook em-REDEX met regelaar M.
α-transformatie
Alpha-hernoemingen stellen u in staat de namen van gebonden variabelen te wijzigen. Bijvoorbeeld x. x kan λ y geven. j. Termen die alleen in alfa-transformatie verschillen, worden α-equivalent genoemd. Bij gebruik van de lambda-calculus worden α-equivalenten vaak als wederkerig beschouwd.
De exacte regels voor alfaconversie zijn niet helemaal triviaal. Ten eerste worden met deze abstractie alleen die variabelen hernoemd die bij hetzelfde systeem horen. Bijvoorbeeld de alfa-transformatie λ x.λ x. x kan leiden tot λ y.λ x. x, maar dit mag niet leiden tot λy.λx.y Dit laatste heeft een andere betekenis dan het origineel. Dit is analoog aan het concept van variabele schaduwprogrammering.
Ten tweede is een alfa-transformatie niet mogelijk als deze zou worden vastgelegd door een niet-permanente andere abstractie. Als u bijvoorbeeld x vervangt door y in λ x.λ y. x, dan kun jey.λy. u, wat helemaal niet hetzelfde is.
In programmeertalen met statische reikwijdte kan alfaconversie worden gebruikt om naamresolutie te vereenvoudigen. Zorg er tegelijkertijd voor dat het concept van een variabele de aanduiding in het bevattende gebied niet maskeert.
In De Bruyne-indexnotatie zijn twee alfa-equivalente termen syntactisch identiek.
Vervanging
De veranderingen geschreven door E [V:=R] zijn het proces waarbij alle vrije voorkomens van de variabele V in de uitdrukking E worden vervangen door de omzet R. Substitutie in termen van λ wordt gedefinieerd door de lambda van de recursie berekening van de conceptstructuur als volgt (let op: x en y - alleen variabelen, en M en N - elke λ-expressie).
x [x:=N] ≡ N
y [x:=N] ≡ y als 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]) als x ≠ y, op voorwaarde dat y ∉ FV (N).
Voor vervanging in een lambda-abstractie is het soms nodig om een uitdrukking te -transformeren. Het is bijvoorbeeld niet waar dat (λ x. Y) [y:=x] resulteert in (λ x. X) omdat de gesubstitueerde x vrij had moeten zijn, maar uiteindelijk gebonden was. De juiste vervanging is in dit geval (λ z. X) tot α-equivalentie. Merk op dat vervanging uniek is gedefinieerd tot aan lambda.
β-reductie
Beta-reductie weerspiegelt het idee van het toepassen van een functie. Beta-reductief wordt gedefinieerd in termen:substitutie: ((X V. E) E ') is E [V:=E'].
Bijvoorbeeld, uitgaande van enige codering 2, 7, ×, is er de volgende β-reductie: ((λ n. N × 2) 7) → 7 × 2.
Beta-reductie kan worden gezien als hetzelfde als het concept van lokale reduceerbaarheid onder natuurlijke deductie via het Curry-Howard-isomorfisme.
η-transform
Deze conversie drukt het idee van extensie uit, wat in deze context is dat twee functies gelijk zijn als ze hetzelfde resultaat geven voor alle argumenten. Deze conversie wisselt tussen λ x. (F x) en f wanneer x niet vrij lijkt in f.
Deze actie kan worden beschouwd als hetzelfde als het concept van lokale volledigheid in natuurlijke deductie door middel van het Curry-Howard-isomorfisme.
Normale vormen en fusie
Voor een ongetypeerde lambda-calculus is de β-reductieregel over het algemeen noch sterk noch zwak normaliserend.
Desalniettemin kan worden aangetoond dat de β-reductie samenvloeit wanneer deze vóór de α-transformatie loopt (d.w.z. twee normaalvormen kunnen als gelijk worden beschouwd als een α-transformatie van de ene naar de andere mogelijk is).
Daarom hebben zowel sterk normaliserende termen als zwak aanpassende termen één enkele normaalvorm. Voor de eerste termen resulteert elke reductiestrategie gegarandeerd in een typische configuratie. Terwijl voor zwak normaliserende omstandigheden, sommige reductiestrategieën het misschien niet vinden.
Extra programmeermethoden
Er zijn veel creatie-idiomen voor de lambda-calculus. Veel van hen zijn oorspronkelijk ontwikkeld in de context van het gebruik van systemen als basis voor de semantiek van een programmeertaal, waarbij ze effectief werden toegepast als een constructie op laag niveau. Aangezien sommige stijlen een lambda-calculus (of iets vergelijkbaars) als fragment bevatten, worden deze technieken ook gebruikt in praktische creatie, maar kunnen ze dan als obscuur of vreemd worden ervaren.
Benoemde constanten
In lambda-calculus neemt een bibliotheek de vorm aan van een reeks eerder gedefinieerde functies, waarbij de termen slechts concrete constanten zijn. Pure calculus heeft geen concept van benoemde onveranderlijkheden, aangezien alle atomaire lambda-termen variabelen zijn. Maar ze kunnen ook worden nagebootst door het veranderlijke als de naam van de constante te nemen, een lambda-abstractie te gebruiken om dat vluchtige in het lichaam te binden, en die abstractie toe te passen op de bedoelde definitie. Dus als je f gebruikt om M in N weer te geven, zou jekunnen zeggen
(λ f. N) M.
Auteurs introduceren vaak een syntactisch concept zoals let om dingen op een meer intuïtieve manier te laten schrijven.
f=M tot N
Door dergelijke definities aan elkaar te koppelen, kan men een lambda-calculus "programma" schrijven als nul of meer functiedefinities gevolgd door een enkel lambdalid, waarbij de definities worden gebruikt die het grootste deel van het programma uitmaken.
Een opmerkelijke beperking van deze let is dat de naam f niet gedefinieerd is in M,aangezien M buiten de bindende reikwijdte van de lambda-abstractie f v alt. Dit betekent dat een recursief functieattribuut niet kan worden gebruikt als M met let. De meer geavanceerde letrec-syntaxis, waarmee u recursieve functiedefinities in deze stijl kunt schrijven, gebruikt in plaats daarvan ook vaste-komma-combinators.
Gedrukte analogen
Dit type is een getypt formalisme dat een symbool gebruikt om een anonieme functie-abstractie weer te geven. In deze context zijn typen meestal objecten van syntactische aard die worden toegewezen aan lambda-termen. De exacte aard hangt af van de calculus in kwestie. Vanuit een bepaald gezichtspunt kan getypte LI worden beschouwd als verfijningen van ongetypte LI. Maar aan de andere kant kunnen ze ook als een meer fundamentele theorie worden beschouwd, en de ongetypeerde lambda-calculus is een speciaal geval met slechts één type.
Getypte LI vormen de basis van programmeertalen en vormen de ruggengraat van functionele talen zoals ML en Haskell. En, meer indirect, dwingende scheppingsstijlen. Getypte lambda-calculi spelen een belangrijke rol bij de ontwikkeling van typesystemen voor programmeertalen. Hier legt typbaarheid meestal de gewenste eigenschappen van het programma vast, het zal bijvoorbeeld geen schending van de geheugentoegang veroorzaken.
Getypte lambda-calculi zijn nauw verwant aan wiskundige logica en bewijstheorie via het Curry-Howard-isomorfisme, en kunnen worden gezien als een interne taal van bijvoorbeeld categorieklassen, dieis gewoon de stijl van cartesiaanse sluitingen.
