Lambdaregning

Lambdaregning ( λ-calculus ) er et formelt system udviklet af den amerikanske matematiker Alonzo Church til at formalisere og analysere begrebet beregnelighed .

Ren λ-regning

Ren λ-kalkulus , hvis termer , også kaldet objekter ("begge"), eller λ - termer, udelukkende er bygget ud fra variable ved hjælp af anvendelse og abstraktion. I første omgang forventes tilstedeværelsen af nogen konstanter ikke.

Anvendelse og abstraktion

λ-regningen er baseret på to grundlæggende operationer:

Applikation ( lat. applicatio - attachment, attachment) betyder anvendelse eller kald af en funktion i forhold til en given værdi. Det er normalt betegnet , hvor er en funktion og er et argument. Dette svarer til den almindeligt anerkendte notation i matematik , som også nogle gange bruges, men det vigtige for λ-regningen er, at den tolkes som en algoritme , der beregner resultatet ud fra en given inputværdi. I denne forstand kan ansøgningen til betragtes på to måder: som et resultat af ansøgningen til eller som en beregningsproces . Den sidste fortolkning af ansøgningen er relateret til begrebet β-reduktion . $f\a$ $f$ $-en$ $f(a)$ $f$ $f$ $-en$ $f$ $-en$ $f\a$

Abstraktion eller λ-abstraktion ( lat. abstractio - distraktion, adskillelse) bygger igen funktioner efter givne udtryk. Nemlig, hvis er et udtryk, der frit indeholder , så betyder notationen: λ er en funktion af argumentet , som har formen , betegner en funktion . Således kan du ved hjælp af abstraktion konstruere nye funktioner. Kravet om, at det frit indgår, er ikke særlig vigtigt – det er nok at antage, at hvis det ikke er det. $t\equiv t[x]$ $x$ $\ \lambda xt[x]$ $x$ $t[x]$ $x\mapsto t[x]$ $x$ $t$ $\lambda xt\equiv t$

α-ækvivalens

Den grundlæggende form for ækvivalens defineret i lambda-termer er alfa-ækvivalens. For eksempel og : er alfa-ækvivalente lambda-udtryk, og begge repræsenterer den samme funktion (identitetsfunktion). Begreber og er ikke alfa-ækvivalente, da de ikke er i en lambda-abstraktion. $\lambda xx$ $\lambda åå$ $x$ $y$

β-reduktion

Da udtrykket angiver en funktion, der tildeler en værdi til hver , så for at evaluere udtrykket $\lambda x.2\cdot x+1$ $x$ $2\cdot x+1$

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

som omfatter både anvendelse og abstraktion , er det nødvendigt at udføre substitution af tallet 3 i termen i stedet for variablen . Resultatet er . Denne idé kan skrives i generel form som $2\cdot x+1$ $x$ $2\cdot 3+1=7$

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

og kaldes β-reduktion . Et udtryk for formen , det vil sige anvendelsen af en abstraktion til et bestemt udtryk, kaldes en redex . Selvom β-reduktionen i det væsentlige er det eneste "essentielle" aksiom for λ-regningen, fører det til en meget rig og kompleks teori. Sammen med det har λ-regningen egenskaben Turing fuldstændighed og er derfor det enkleste programmeringssprog . $(\lambda xt)\ a$

η-transform

$\eta$ -konvertering udtrykker ideen om, at to funktioner er identiske, hvis og kun hvis de, når de anvendes på ethvert argument, producerer de samme resultater. -transformation oversætter formler og til hinanden (kun hvis den ikke har nogen frie forekomster i : ellers vil den frie variabel efter transformationen blive en bundet ekstern abstraktion, eller omvendt). $\eta$ $\lambda xf\ x$ $f$ $x$ $f$ $x$

Currying (currying)

En funktion af to variable og kan betragtes som en funktion af en variabel , returnerer en funktion af en variabel , det vil sige som et udtryk . Denne teknik fungerer nøjagtigt det samme for funktioner af enhver art . Dette viser, at funktioner af mange variable kan udtrykkes i λ-regning og er " syntaktisk sukker ". Den beskrevne proces med at omdanne funktioner af mange variable til en funktion af én variabel kaldes currying (også: currying ), efter den amerikanske matematiker Haskell Curry , selvom den først blev foreslået af Moses Sheinfinkel ( 1924 ). $x$ $y$ $f(x,y)=x+y$ $x$ $y$ $\ \lambda x.\lambda y.x+y$

Semantik af den ikke-typebestemte λ-regning

Den kendsgerning, at λ-regningens vilkår fungerer som funktioner anvendt på λ-regningens vilkår (det vil sige måske for dem selv), fører til vanskeligheder med at konstruere en passende semantik af λ-regningen. For at give λ-regningen nogen betydning, er det nødvendigt at opnå et sæt , hvori dets rum af funktioner ville være indlejret . I det generelle tilfælde eksisterer dette ikke på grund af begrænsninger på kardinaliteterne af disse to sæt, og fungerer fra til : den anden har en større kardinalitet end den første. $D$ $D\to D$ $D$ $D$ $D$ $D$

Dana Scott overvandt denne vanskelighed i begyndelsen af 1970'erne ved at konstruere begrebet en region (først på komplette gitter [1] , senere generalisere det til et komplet delvist ordnet sæt med en speciel topologi ) og skære det ned til kontinuerte funktioner i denne topologi [ 2] . På basis af disse konstruktioner blev den denotationelle semantik af programmeringssprog skabt , især på grund af det faktum, at det ved hjælp af dem er muligt at give en nøjagtig mening til to vigtige programmeringssprogskonstruktioner, som f.eks. som rekursion og datatyper . $D$ $D\to D$

Relation til rekursive funktioner

Rekursion er at definere en funktion ud fra sig selv; ved første øjekast tillader lambdaregningen dette ikke, men dette indtryk er misvisende. Overvej f.eks. en rekursiv funktion, der beregner faktoren :

f(n) = 1, hvis n = 0; ellers n × f(n - 1).

I lambda-regningen kan en funktion ikke direkte referere til sig selv. En funktion kan dog sendes en parameter, der er knyttet til den. Som regel kommer dette argument først. Ved at forbinde det med en funktion får vi en ny, allerede rekursiv funktion. For at gøre dette skal et argument, der refererer til sig selv (her betegnet som ) sendes til funktionslegemet. $r$

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

Dette løser det specifikke problem med at beregne faktoren, men en generel løsning er også mulig. Givet et lambda-udtryk, der repræsenterer kroppen af en rekursiv funktion eller sløjfe, der passerer sig selv som det første argument, vil fastpunktskombinatoren returnere den ønskede rekursive funktion eller sløjfe. Funktioner behøver ikke eksplicit passere sig selv hver gang.

Der er flere definitioner af fikspunktskombinatorer. Den enkleste af dem:

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

I lambdaregning er et fast punkt ; lad os demonstrere det: $\operatørnavn {Y\ g}$ $\operatørnavn {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, for at definere fakultet som en rekursiv funktion, kan vi simpelthen skrive , hvor er det tal, som fakultetet er beregnet for. Lad , vi får: $\operatørnavn {g\ (Y\ g)} n$ $n$ $n=4$

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

Hver rekursiv funktionsdefinition kan repræsenteres som et fast punkt af den tilsvarende funktion, og derfor kan hver rekursiv definition udtrykkes som et lambda-udtryk. Især kan vi definere subtraktion, multiplikation, sammenligning af naturlige tal rekursivt. $\operatørnavn {Y}$

I programmeringssprog

I programmeringssprog forstås "λ-calculus" ofte som mekanismen for " anonyme funktioner " - tilbagekaldsfunktioner , der kan defineres lige på det sted, hvor de bruges, og som har adgang til de lokale variabler for den aktuelle funktion ( lukning ).

Se også

Noter

↑ 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 Gitterteoretiske modeller for forskellige typefrie regning. — I: Proc. 4. Int. Congress for Logic, Methodology, and the Philosophy of Science, Bukarest, 1972.

Litteratur

Barendregt X. Lambdaregning. Dens syntaks og semantik: Pr. fra engelsk. — M.: Mir, 1985. — 606 s.