Lambda kalkyl

Lambdakalkyl ( λ-calculus ) är ett formellt system utvecklat av den amerikanske matematikern Alonzo Church för att formalisera och analysera begreppet beräkningsbarhet .

Ren λ-kalkyl

Ren λ-kalkyl , vars termer , även kallade objekt ("båda"), eller λ -termer, byggs uteslutande från variabler med användning av tillämpning och abstraktion. Inledningsvis antas inte närvaron av några konstanter.

Tillämpning och abstraktion

λ -kalkylen är baserad på två grundläggande operationer:

Application ( lat. applicatio - attachment, attachment) betyder tillämpning eller anrop av en funktion i förhållande till ett givet värde. Det betecknas vanligtvis , där är en funktion och är ett argument. Detta motsvarar den notation som är allmänt accepterad inom matematik , som också ibland används, men det som är viktigt för λ-kalkylen är att den tolkas som en algoritm som beräknar resultatet från ett givet ingångsvärde. I denna mening kan ansökan till betraktas på två sätt: som ett resultat av att ansöka till eller som en beräkningsprocess . Den sista tolkningen av ansökan är relaterad till begreppet β-reduktion . $fa$ $f$ $a$ $fa)$ $f$ $f$ $a$ $f$ $a$ $fa$

Abstraktion eller λ-abstraktion ( lat. abstractio - distraktion, separation) bygger i sin tur funktioner efter givna uttryck. Nämligen, om är ett uttryck som fritt innehåller , så betyder notationen : λ är en funktion av argumentet , som har formen , betecknar en funktion . Med hjälp av abstraktion kan du alltså konstruera nya funktioner. Kravet att det fritt inträder är inte särskilt viktigt - det räcker att anta att om det inte är det. $t\equiv t[x]$ $x$ $\ \lambda xt[x]$ $x$ $t[x]$ $x\mapsto t[x]$ $x$ $t$ $\lambda xt\equiv t$

α-ekvivalens

Den grundläggande formen av ekvivalens definierad i lambda-termer är alfa-ekvivalens. Till exempel och : är alfaekvivalenta lambda-termer och båda representerar samma funktion (identitetsfunktion). Termer och är inte alfaekvivalenta eftersom de inte är i en lambdaabstraktion. $\lambda xx$ $\lambda åå$ $x$ $y$

β-reduktion

Eftersom uttrycket betecknar en funktion som tilldelar ett värde till varje , då för att utvärdera uttrycket $\lambda x.2\cdot x+1$ $x$ $2\cdot x+1$

(\lambda x.2\cdot x+1)\ 3,

som inkluderar både tillämpning och abstraktion , är det nödvändigt att utföra substitution av siffran 3 i termen istället för variabeln . Resultatet är . Denna idé kan skrivas i allmän form som $2\cdot x+1$ $x$ $2\cdot 3+1=7$

(\lambda xt)\ a=t[x:=a]

och kallas β-reduktion . Ett uttryck för formen , det vill säga tillämpningen av en abstraktion på en viss term, kallas en redex . Även om β-reduktionen i huvudsak är det enda "väsentliga" axiomet för λ-kalkylen, leder det till en mycket rik och komplex teori. Tillsammans med den har λ-kalkylen egenskapen Turing-fullständighet och är därför det enklaste programmeringsspråket . $(\lambda xt)\ a$

η-transform

$\eta$ -konvertering uttrycker idén att två funktioner är identiska om och endast om de, när de tillämpas på något argument, ger samma resultat. -transformation översätter formler och till varandra (endast om den inte har några fria förekomster i : annars kommer den fria variabeln efter transformationen att bli en bunden extern abstraktion, eller vice versa). $\eta$ $\lambda xf\ x$ $f$ $x$ $f$ $x$

Currying (currying)

En funktion av två variabler och kan betraktas som en funktion av en variabel , returnerar en funktion av en variabel , det vill säga som ett uttryck . Den här tekniken fungerar exakt likadant för funktioner av vilken art som helst . Detta visar att funktioner för många variabler kan uttryckas i λ-kalkyl och är " syntaktisk socker ". Den beskrivna processen att omvandla funktioner för många variabler till en funktion av en variabel kallas currying (även: currying ), efter den amerikanske matematikern Haskell Curry , även om den först föreslogs av Moses Sheinfinkel ( 1924 ). $x$ $y$ $f(x,y)=x+y$ $x$ $y$ $\ \lambda x.\lambda y.x+y$

Semantik för den otypade λ-kalkylen

Det faktum att termerna för λ-kalkylen fungerar som funktioner som tillämpas på termerna för λ-kalkylen (det vill säga kanske till dem själva) leder till svårigheter att konstruera en adekvat semantik av λ-kalkylen. För att ge λ-kalkylen någon mening är det nödvändigt att erhålla en mängd där dess funktionsutrymme skulle vara inbäddat . I det allmänna fallet existerar detta inte på grund av begränsningar av kardinaliteterna för dessa två uppsättningar, och fungerar från till : den andra har en större kardinalitet än den första. $D$ $D\to D$ $D$ $D$ $D$ $D$

Dana Scott övervann denna svårighet i början av 1970-talet genom att konstruera begreppet en region (till en början på kompletta gitter [1] , senare generalisera den till en komplett delvis ordnad uppsättning med en speciell topologi ) och skära ner den till funktioner som är kontinuerliga i denna topologi [ 2] . På basis av dessa konstruktioner skapades programmeringsspråkens denotationssemantik , i synnerhet på grund av det faktum att det med hjälp av dem är möjligt att ge en exakt mening till två viktiga programmeringsspråkskonstruktioner, som t.ex. som rekursion och datatyper . $D$ $D\to D$

Relation till rekursiva funktioner

Rekursion är att definiera en funktion i termer av sig själv; vid första anblicken tillåter inte lambdakalkylen detta, men detta intryck är missvisande. Tänk till exempel på en rekursiv funktion som beräknar faktorn :

f(n) = 1, om n = 0; annars n × f(n - 1).

I lambdakalkylen kan en funktion inte direkt referera till sig själv. En funktion kan dock skickas med en parameter som är associerad med den. Som regel kommer detta argument först. Förknippar den med en funktion får vi en ny, redan rekursiv funktion. För att göra detta måste ett argument som refererar till sig självt (här betecknat som ) skickas till funktionskroppen. $r$

g := λr. λn.(1, om n = 0; annars n × (rr (n-1))) f := gg

Detta löser det specifika problemet med att beräkna faktorialen, men en generell lösning är också möjlig. Givet en lambda-term som representerar kroppen av en rekursiv funktion eller slinga, som ger sig själv som det första argumentet, kommer fixpunktskombinatorn att returnera den önskade rekursiva funktionen eller slingan. Funktioner behöver inte explicit passera sig själva varje gång.

Det finns flera definitioner av fixpunktskombinatorer. Den enklaste av dem:

Y = λg.(λx.g (xx)) (λx.g (xx))

I lambdakalkyl är en fixpunkt ; låt oss visa det: $\operatörsnamn {Y\ g}$ $\operatörsnamn {g}$

Y g (λh.(λx.h (xx)) (λx.h (xx))) g (λx.g (xx)) (λx.g (xx)) g((λx.g(xx))(λx.g(xx))) g (Yg)

Nu, för att definiera faktorial som en rekursiv funktion, kan vi helt enkelt skriva , där är talet för vilket faktorialet beräknas. Låt , vi får: $\operatörsnamn {g\ (Y\ g)} n$ $n$ $n=4$

g (Y g) 4 (λfn.(1, om n = 0; och n (f(n-1)), om n>0)) (Y g) 4 (λn.(1, om n = 0; och n ((Yg) (n-1)), om n>0)) 4 1, om 4 = 0; och 4 (g(Yg) (4-1)), om 4>0 4 (g(Y g) 3) 4 (λn.(1, om n = 0; och n ((Yg) (n-1)), om n>0) 3) 4 (1, om 3 = 0; och 3 (g(Y g) (3-1)), om 3>0) 4 (3 (g(Y g) 2)) 4 (3 (λn.(1, om n = 0; och n ((Yg) (n-1)), om n>0) 2)) 4 (3 (1, om 2 = 0; och 2 (g(Y g) (2-1)), om 2>0)) 4 (3 (2 (g(Y g) 1))) 4 (3 (2 (λn.(1, om n = 0; och n ((Yg) (n-1)), om n>0) 1))) 4 (3 (2 (1, om 1 = 0; och 1 ((Y g) (1-1)), om 1>0))) 4 (3 (2 (1) ((Y g) 0)))) 4 (3 (2 (1) ((λn.(1, om n = 0; och n ((Y g) (n-1)), om n>0) 0)))) 4 (3 (2 (1 (1), om 0 = 0; och 0 ((Y g) (0-1)), om 0>0)))) 4 (3 (2 (1 (1)))) 24

Varje rekursiv funktionsdefinition kan representeras som en fixpunkt för motsvarande funktion, och därför kan varje rekursiv definition uttryckas som ett lambda-uttryck. I synnerhet kan vi definiera subtraktion, multiplikation, jämförelse av naturliga tal rekursivt. $\operatörsnamn {Y}$

I programmeringsspråk

I programmeringsspråk förstås "λ-kalkyl" ofta som mekanismen för " anonyma funktioner " - återuppringningsfunktioner som kan definieras direkt på den plats där de används och som har tillgång till de lokala variablerna för den aktuella funktionen ( stängning ).

Se även

Anteckningar

↑ Scott DS The lattice of flow diagrams.-- Lecture Notes in Mathematics, 188, Symposium on Semantics of Algorithmic Languages.-- Berlin, Heidelberg, New York: Springer-Verlag, 1971, pp. 311-372.
↑ Scott DS Lattice-teoretiska modeller för olika typfria kalkyler. — I: Proc. 4:e Int. Congress for Logic, Methodology and the Philosophy of Science, Bukarest, 1972.

Litteratur

Barendregt X. Lambdakalkyl. Dess syntax och semantik: Per. från engelska. — M.: Mir, 1985. — 606 sid.