Lambda-rekening is 'n formele stelsel in wiskundige logika vir die uitdrukking van abstraksie-gebaseerde berekeninge en die toepassing van funksies deur gebruik te maak van binding en veranderlike substitusie. Dit is 'n universele model wat toegepas kan word op die ontwerp van enige Turing-masjien. Die lambda-rekening is die eerste keer in die 1930's deur Church, 'n bekende wiskundige, bekendgestel.
Die stelsel bestaan uit die bou van lambda-lede en die uitvoering van reduksiebewerkings daarop.
Verduidelikings en toepassings
Die Griekse letter lambda (λ) word in lambda-uitdrukkings en lambda-terme gebruik om die binding van 'n veranderlike in 'n funksie aan te dui.
Lambda-rekening kan ongetik of getik word. In die eerste variant kan funksies slegs gebruik word as hulle in staat is om data van hierdie tipe te ontvang. Getikte lambda-rekeninge is swakker, kan 'n kleiner waarde uitdruk. Maar aan die ander kant laat hulle jou toe om meer dinge te bewys.
Een rede waarom daar soveel verskillende tipes is, is die begeerte van wetenskaplikes om meer te doen sonder om die geleentheid prys te gee om sterk lambda-rekeningstellings te bewys.
Die stelsel het toepassings in baie verskillende areas van wiskunde, filosofie, linguistiek en rekenaarwetenskap. Eerstens is die lambda-rekening 'n calculus wat 'n belangrike rol gespeel het in die ontwikkeling van die teorie van programmeertale. Dit is die style van funksionele skepping wat stelsels implementeer. Hulle is ook 'n warm onderwerp van navorsing in die teorie van hierdie kategorieë.
Vir dummies
Die lambda-rekening is in die 1930's deur die wiskundige Alonzo Church bekendgestel as deel van sy navorsing oor die grondslae van wetenskap. Daar is in 1935 getoon dat die oorspronklike stelsel logies inkonsekwent was toe Stephen Kleen en J. B. Rosser die Kleene-Rosser-paradoks ontwikkel het.
Later, in 1936, het Church net die deel uitgesonder en gepubliseer wat vir berekeninge relevant is, wat nou die ongetikte lambda-rekening genoem word. In 1940 het hy ook 'n swakker, maar logies konsekwente teorie bekendgestel, bekend as die prima tipe stelsel. In sy werk verduidelik hy die hele teorie in eenvoudige terme, so daar kan gesê word dat Church die calculus lambda for dummies gepubliseer het.
Tot die 1960's, toe die verband daarvan met programmeertale duidelik geword het, was λ net 'n formalisme. Danksy die toepassings van Richard Montagu en ander linguiste in die semantiek van natuurlike taal, het calculus 'n trotse plek ingeneem in beide linguistiek en rekenaarwetenskap.
Oorsprong van die simbool
Lambda staan nie vir 'n woord of akroniem nie, dit kom van 'n verwysing in Russell se Principal Mathematics gevolg deur twee tipografiese veranderinge. Notasievoorbeeld: vir 'n funksie f met f (y)=2y + 1 is 2ŷ + 1. En hier gebruik ons 'n karet (“hoed”) oor y om die invoerveranderlike te benoem.
Die kerk was oorspronklik van plan om soortgelyke simbole te gebruik, maar lettersetters kon nie die "hoed"-simbool bo die letters plaas nie. Hulle het dit dus oorspronklik as "/\y.2y+1" gedruk. In die volgende episode van redigering het tiksters "/ \" vervang met 'n visueel soortgelyke karakter.
Inleiding tot lambda-rekening
Die stelsel bestaan uit 'n taal van terme, wat deur 'n sekere formele sintaksis gekies word, en 'n stel transformasiereëls wat dit toelaat om te manipuleer. Die laaste punt kan as 'n vergelykingsteorie of as 'n operasionele definisie beskou word.
Alle funksies in die lambda-rekening is anoniem, wat beteken dat hulle nie name het nie. Hulle neem net een insetveranderlike, en kerrie word gebruik om plotte met veelvuldige veranderlikes te implementeer.
Lambda-bepalings
Die calculus-sintaksis definieer sommige uitdrukkings as geldig en ander as ongeldig. Net soos verskillende stringe karakters geldige C-programme is en sommige nie. Die werklike uitdrukking van die lambda-rekening word die "lambda-term" genoem.
Die volgende drie reëls verskaf 'n induktiewe definisie wat kan weesvan toepassing op die konstruksie van alle sintakties geldige konsepte:
Die x-veranderlike self is 'n geldige lambda-term:
- as T LT is en x is nie-konstant, dan word (lambda xt) 'n abstraksie genoem.
- as T sowel as s konsepte is, dan word (TS) 'n toepassing genoem.
Niks anders is 'n lambda-term nie. Dus is 'n konsep geldig indien en slegs as dit verkry kan word deur herhaalde toepassing van hierdie drie reëls. Sommige hakies kan egter volgens ander kriteria weggelaat word.
Definisie
Lambda-uitdrukkings bestaan uit:
- veranderlikes v 1, v 2, …, v n, …
- simbole van abstraksie 'λ' en punt '.'
- hakies ().
Die versameling Λ kan induktief gedefinieer word:
- As x 'n veranderlike is, dan is x ∈ Λ;
- x is nie konstant nie en M ∈ Λ, dan (λx. M) ∈ Λ;
- M, N ∈ Λ, dan (MN) ∈ Λ.
Benaming
Om die notasie van lambda-uitdrukkings ondeursigtig te hou, word die volgende konvensies algemeen gebruik:
- Buitenste hakies weggelaat: MN in plaas van (MN).
- Aansoeke word aanvaar om assosiatief te bly: mens kan MNP skryf in plaas van ((MN) P).
- Die liggaam van abstraksie strek verder na regs: λx. MN beteken λx. (MN), nie (λx. M) N.
- Die volgorde van abstraksies word verminder: λx.λy.λz. N kan λxyz. N. wees
Vrye en gebonde veranderlikes
Die operateur λ verbind sy nie-konstante waar dit ook al in die liggaam van abstraksie is. Veranderlikes wat binne die bestek val, word gebonde genoem. In die uitdrukking λ x. M, die λ x deel word dikwels na verwys as 'n bindmiddel. Asof te kenne gee dat die veranderlikes 'n groep word met die toevoeging van X x tot M. Alle ander onstabiele word vry genoem.
Byvoorbeeld, in die uitdrukking λ y. x x y, y - gebind nie-permanent, en x - vry. En dit is ook opmerklik dat die veranderlike gegroepeer word volgens sy "naaste" abstraksie. In die volgende voorbeeld word die lambda-rekeningoplossing voorgestel deur 'n enkele voorkoms van x, wat verband hou met die tweede term:
λ x. y (λ x. z x)
Die stel vrye veranderlikes M word aangedui as FV (M) en word gedefinieer deur rekursie oor die struktuur van terme soos volg:
- FV (x)={x}, waar x 'n veranderlike is.
- FV (λx. M)=FV (M) {x}.
- FV (MN)=FV (M) ∪ FV (N).
'n Formule wat nie vrye veranderlikes bevat nie, word geslote genoem. Geslote lambda-uitdrukkings staan ook bekend as kombineerders en is gelykstaande aan terme in kombinatoriese logika.
Afkorting
Die betekenis van lambda-uitdrukkings word bepaal deur hoe hulle verkort kan word.
Daar is drie tipes snitte:
- α-transformeer: verander gebonde veranderlikes (alfa).
- β-reduksie: die toepassing van funksies op hul argumente (beta).
- η-transformeer: dek die idee van ekstensionaliteit.
Hier is dit ookons praat van die resulterende ekwivalensies: twee uitdrukkings is β-ekwivalent as hulle β-getransformeer kan word in dieselfde komponent, en α / η-ekwivalensie word soortgelyk gedefinieer.
Die term redex, kort vir verminderbare omset, verwys na subonderwerpe wat deur een van die reëls verminder kan word. Lambda-rekening vir dummies, voorbeelde:
(λ x. M) N is 'n beta-redeks in die uitdrukking vir die vervanging van N met x in M. Die komponent waartoe 'n redeks reduseer word sy reduksie genoem. Die reduksie (λ x. M) N is M [x:=N].
As x nie vry is in M nie, λ x. M x em-REDEX ook met reguleerder M.
α-transformasie
Alfa-hername laat jou toe om die name van gebonde veranderlikes te verander. Byvoorbeeld, x. x kan λ y gee. y. Daar word gesê dat terme wat slegs in alfa-transformasie verskil, α-ekwivalent is. Dikwels, wanneer die lambda-rekening gebruik word, word α-ekwivalente as wederkerig beskou.
Die presiese reëls vir alfa-omskakeling is nie heeltemal triviaal nie. Eerstens, met hierdie abstraksie, word slegs daardie veranderlikes wat met dieselfde stelsel geassosieer word hernoem. Byvoorbeeld, die alfa-transformasie λ x.λ x. x kan lei tot λ y.λ x. x, maar dit mag nie lei tot λy.λx.y Laasgenoemde het 'n ander betekenis as die oorspronklike. Dit is analoog aan die konsep van veranderlike skadu-programmering.
Tweedens, 'n alfa-transformasie is nie moontlik as dit sou lei dat dit vasgevang word deur 'n nie-permanente ander abstraksie. Byvoorbeeld, as jy x vervang met y in λ x.λ y. x, dan kan jy kryλy.λy. u, wat glad nie dieselfde is nie.
In programmeertale met statiese omvang, kan alfa-omskakeling gebruik word om naamresolusie te vereenvoudig. Sorg terselfdertyd dat die konsep van 'n veranderlike nie die benaming in die inhoudende area verberg nie.
In De Bruyne-indeksnotasie is enige twee alfa-ekwivalente terme sintakties identies.
Vervanging
Die veranderinge geskryf deur E [V:=R] is die proses om alle vrye voorkomste van die veranderlike V in die uitdrukking E te vervang met die omset R. Vervanging in terme van λ word gedefinieer deur die lambda van die rekursie berekening oor die konsepstruktuur soos volg (let wel: x en y - slegs veranderlikes, en M en N - enige λ-uitdrukking).
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]) as x ≠ y, met dien verstande dat y ∉ FV (N).
Vir vervanging in 'n lambda-abstraksie, is dit soms nodig om 'n uitdrukking te α-transformeer. Dit is byvoorbeeld nie waar dat (λ x. Y) [y:=x] lei tot (λ x. X) omdat die gesubstitueerde x vry moes gewees het, maar uiteindelik gebind was. Die korrekte vervanging in hierdie geval is (λ z. X) tot α-ekwivalensie. Let daarop dat vervanging uniek gedefinieer word tot lambda.
β-vermindering
Beta-vermindering weerspieël die idee om 'n funksie toe te pas. Beta-reduktief word in terme gedefinieervervanging: ((X V. E) E ') is E [V:=E'].
Byvoorbeeld, met die aanname van een of ander enkodering 2, 7, ×, is daar die volgende β-reduksie: ((λ n. N × 2) 7) → 7 × 2.
Beta-vermindering kan gesien word as dieselfde as die konsep van plaaslike reduseerbaarheid onder natuurlike aftrekking via die Curry-Howard isomorfisme.
η-transform
Hierdie omskakeling druk die idee van ekstensionaliteit uit, wat in hierdie konteks is dat twee funksies gelyk is wanneer hulle dieselfde resultaat vir alle argumente gee. Hierdie omskakeling ruil tussen λ x. (F x) en f wanneer x nie vry lyk in f nie.
Hierdie aksie kan beskou word as dieselfde as die konsep van plaaslike volledigheid in natuurlike deduksie deur die Curry-Howard isomorfisme.
Normale vorms en samesmelting
Vir 'n ongetipe lambda-rekening is die β-reduksiereël oor die algemeen nie sterk of swak normaliserend nie.
Daar kan nietemin aangetoon word dat die β-reduksie saamsmelt wanneer dit voor die α-transformasie loop (d.w.s. twee normale vorme kan as gelyk beskou word as 'n α-transformasie van die een na die ander moontlik is).
Daarom het beide sterk normaliserende terme en swak aangepaste terme 'n enkele normale vorm. Vir die eerste terme is enige verminderingstrategie gewaarborg om 'n tipiese konfigurasie tot gevolg te hê. Terwyl sommige verminderingstrategieë dit dalk nie sal vind vir swak normaliserende toestande nie.
Bykomende programmeringsmetodes
Daar is baie skeppings-idiome vir die lambda-rekening. Baie van hulle is oorspronklik ontwikkel in die konteks van die gebruik van stelsels as die basis vir die semantiek van 'n programmeertaal, wat hulle effektief as 'n laevlak-konstruk toepas. Aangesien sommige style 'n lambda-rekening (of iets soortgelyks) as 'n brokkie insluit, vind hierdie tegnieke ook gebruik in praktiese skepping, maar kan dan as onduidelik of vreemd beskou word.
Benoemde konstantes
In lambda-rekening neem 'n biblioteek die vorm aan van 'n stel voorheen gedefinieerde funksies, waar die terme net konkrete konstantes is. Suiwer calculus het geen konsep van genoemde onveranderlikes nie, aangesien alle atoom-lambda-terme veranderlikes is. Maar hulle kan ook nageboots word deur die veranderlike as die naam van die konstante te neem, 'n lambda-abstraksie te gebruik om daardie vlugtige in die liggaam te bind, en daardie abstraksie op die beoogde definisie toe te pas. So as jy f gebruik om M in N voor te stel, kan jy sê
(λ f. N) M.
Skrywers stel dikwels 'n sintaktiese konsep voor soos laat om toe te laat dat dinge op 'n meer intuïtiewe manier geskryf word.
f=M tot N
Deur sulke definisies te ketting, kan 'n mens 'n lambda-rekening "program" skryf as nul of meer funksie-definisies gevolg deur 'n enkele lambda-lid, deur daardie definisies te gebruik wat die grootste deel van die program uitmaak.
'n Opvallende beperking van hierdie let is dat die naam f nie in M gedefinieer word nie,aangesien M buite die bindende bestek van die lambda-abstraksie is f. Dit beteken dat 'n rekursiewe funksie-kenmerk nie as M met laat gebruik kan word nie. Die meer gevorderde letrec-sintaksis, wat jou toelaat om rekursiewe funksiedefinisies in hierdie styl te skryf, gebruik eerder vastepuntkombineerders.
Gedrukte analoë
Hierdie tipe is 'n getikte formalisme wat 'n simbool gebruik om 'n anonieme funksie-abstraksie voor te stel. In hierdie konteks is tipes gewoonlik objekte van 'n sintaktiese aard wat aan lambda-terme toegeken word. Die presiese aard hang af van die betrokke calculus. Uit 'n sekere oogpunt kan getikte LI as verfynings van ongetikte LI beskou word. Maar aan die ander kant kan hulle ook as 'n meer fundamentele teorie beskou word, en die ongetikte lambda-rekening is 'n spesiale geval met net een tipe.
Getikte LI is die grondslag van programmeertale en die ruggraat van funksionele tale soos ML en Haskell. En, meer indirek, noodsaaklike skeppingstyle. Getikte lambda-rekeninge speel 'n belangrike rol in die ontwikkeling van tipestelsels vir programmeertale. Hier vang tikbaarheid gewoonlik die verlangde eienskappe van die program vas, dit sal byvoorbeeld nie 'n geheuetoegangsoortreding veroorsaak nie.
Getikte lambda-rekeninge is nou verwant aan wiskundige logika en bewysteorie deur die Curry–Howard-isomorfisme, en kan beskou word as 'n interne taal van kategorieklasse, wat byvoorbeeldis eenvoudig die styl van Cartesiese sluitings.
