Definition av lambdakalkyl

För en allmän introduktion, se Lambdakalkyl .

Lambdakalkyl är ett formellt matematiskt system baserat på lambdaabstraktion och funktionstillämpning . Två definitioner av språket ges här: en standarddefinition och en definition med matematiska formler.

Standard Definition

Denna formella definition gavs av Alonzo Church .

Definition

Lambda-uttryck är sammansatta av

• variabler $v_{1}$ , $v_{2}$ , ..., $v_{n}$ , ...
• abstraktionssymbolerna lambda ' $\lambda$ ' och punkt '.'
• parenteser ( )

Uppsättningen lambda-uttryck, $\Lambda$ , kan definieras induktivt :

1. Om $x$ är en variabel, då $x\in \Lambda$
2. Om $x$ är en variabel och $M\in \Lambda$ , då $(\lambda xM)\in \Lambda$
3. Om $M,N\in \Lambda$ , då $(M\ N)\in \Lambda$

Förekomster av regel 2 är kända som abstraktioner och förekomster av regel 3 är kända som tillämpningar.

Notation

För att hålla notationen av lambda-uttryck ren, tillämpas vanligtvis följande konventioner.

• De yttersta parenteserna tas bort: $M\ N$ istället för $(M\ N)$
• Applikationer antas vara vänsterassociativa: $M\ N\ P$ kan skrivas istället för $((M\ N)\ P)$
• Broppen i en abstraktion sträcker sig så långt till höger som möjligt : $\lambda xM\ N$ betyder $\lambda x.(M\ N)$ och inte $(\lambda xM)\ N$
• En sekvens av abstraktioner dras samman: $\lambda x.\lambda y.\lambda zN$ förkortas till $\lambda xyz.N$

Fria och bundna variabler

Abstraktionsoperatorn, $\lambda$ , sägs binda sin variabel varhelst den förekommer i abstraktionens kropp. Variabler som faller inom ramen för en abstraktion sägs vara bundna . Alla andra variabler kallas fria . Till exempel, i följande uttryck $y$ en bunden variabel och $x$ är fri: $\lambda yx\ x\ y$ . Observera också att en variabel är bunden av sin "närmaste" abstraktion. I följande exempel är den enda förekomsten av $x$ i uttrycket bunden av den andra lambda: $\lambda xy(\lambda xz\ x)$

Uppsättningen av fria variabler för ett lambda-uttryck, $M$ , betecknas som $\operatorname {FV} (M)$ och definieras av rekursion på termernas struktur, som följer:

1. $\operatorname {FV} (x)=\{x\}$ , där $x$ är en variabel
2. $\operatörsnamn {FV} (\lambda xM)=\operatörsnamn {FV} (M)\backslash \{x\}$
3. $\operatörsnamn {FV} (M\ N)=\operatörsnamn {FV} (M)\cup \operatörsnamn {FV} (N)$

Ett uttryck som inte innehåller några fria variabler sägs vara stängt . Slutna lambda-uttryck är också kända som kombinatorer och är ekvivalenta med termer i kombinatorisk logik .

Minskning

Betydelsen av lambda-uttryck definieras av hur uttryck kan reduceras.

Det finns tre typer av reduktion:

• α-omvandling : ändra bundna variabler ( alfa );
• β-reduktion : tillämpa funktioner på deras argument ( beta );
• η-reduktion : som fångar en föreställning om extensionalitet ( eta ).

Vi talar också om de resulterande ekvivalenserna: två uttryck är β-ekvivalenta , om de kan β-konverteras till samma uttryck, och α/η-ekvivalens definieras på liknande sätt.

Termen redex , förkortning för reducerbart uttryck , syftar på deltermer som kan reduceras med någon av reduktionsreglerna. Till exempel, $(\lambda xM)\ N$ är en β-redex för att uttrycka ersättningen av $N$ för $x$ i $M$ ; om $x$ inte är ledig i $M$ , $\lambda xM\ x$ är en η-redex. Uttrycket som en redex reducerar till kallas dess reduktion; med föregående exempel är redukterna av dessa uttryck $M[x:=N]$ respektive $M$ .

α-omvandling

Alfa-konvertering, ibland känd som alfa-döpning, gör att bundna variabelnamn kan ändras. Till exempel alfa-omvandling av $\lambda xx$ kan ge $\lambda yy$ . Termer som skiljer sig endast genom alfa-omvandling kallas α-ekvivalent . Ofta vid användning av lambda-kalkyl anses α-ekvivalenta termer vara ekvivalenta.

De exakta reglerna för alfakonvertering är inte helt triviala. För det första, vid alfakonvertering av en abstraktion, är de enda variabla förekomsterna som byts om de som är bundna till samma abstraktion. Till exempel en alfa-omvandling av $\lambda x.\lambda xx$ kan resultera i $\lambda y.\lambda xx$ , men det kunde inte resultera i $\lambda y.\lambda xy$ . Det senare har en annan betydelse än originalet.

För det andra är alfakonvertering inte möjlig om det skulle resultera i att en variabel fångas av en annan abstraktion. Till exempel, om vi ersätter $x$ med $y$ i $\lambda x.\lambda yx$ , vi får $\lambda y.\lambda yy$ , vilket inte alls är detsamma.

I programmeringsspråk med statisk omfattning kan alfakonvertering användas för att göra namnupplösning enklare genom att säkerställa att inget variabelnamn maskerar ett namn i ett innehållande omfång (se alfabyte för att göra namnupplösning trivialt ) .

Utbyte

Substitution, skriven $E[V:=R]$ , är processen att ersätta alla fria förekomster av variabeln $V$ i uttrycket $E$ med uttryck $R$ . Substitution på termer av lambda-kalkylen definieras av rekursion på strukturen av termer, enligt följande (notera: x och y är endast variabler medan M och N är vilket λ-uttryck som helst).

${\begin{aligned}x[x:=N]&\equiv N\\y[x:= N]&\equiv y{\text{, if }}x\neq y\end{aligned}}$

${\begin{aligned}(M_{1}\ M_{2})[x:=N]&\equiv (M_{1}[x:=N])\ (M_ {2}[x:=N])\\(\lambda xM)[x:=N]&\equiv \lambda xM\\(\lambda yM)[x:=N]&\equiv \lambda y.( M[x:=N]){\text{, om }}x\neq y{\text{, förutsatt }}y\notin FV(N)\end{aligned}}$

För att ersätta till en lambdaabstraktion är det ibland nödvändigt att α-konvertera uttrycket. Till exempel är det inte korrekt att $(\lambda xy)[y:=x]$ resulterar i $(\lambda xx)$ , eftersom den ersatta $x$ var tänkt att vara fri men slutade med att bindas. Den korrekta substitutionen i detta fall är $(\lambda zx)$ , upp till α-ekvivalens. Observera att substitution definieras unikt upp till α-ekvivalens.

β-reduktion

β-reduktion fångar idén om funktionstillämpning. β-reduktion definieras i termer av substitution: β-reduktionen av $((\lambda VE)\ E')$ är ${\ displaystil E[V:=E']}$ .

Om vi ​​till exempel antar någon kodning av $2,7,\times$ , har vi följande β-reduktion: $( (\lambda n.\ n\ gånger 2)\ 7)\högerpil 7\ gånger 2$ .

η-reduktion

η-reduktion uttrycker idén om extensionalitet , som i detta sammanhang är att två funktioner är lika om och bara om de ger samma resultat för alla argument. η-reduktion konverterar mellan $\lambda x.(fx)$ och $f$ när $x$ inte visas ledig i $f$ .

Normalisering

Huvudartikel: Betanormalform

Syftet med β-reduktion är att beräkna ett värde. Ett värde i lambdakalkyl är en funktion. Så β-reduktion fortsätter tills uttrycket ser ut som en funktionsabstraktion.

Ett lambdauttryck som inte kan reduceras ytterligare med antingen β-redex eller η-redex är i normal form. Observera att alfakonvertering kan konvertera funktioner. Alla normalformer som kan omvandlas till varandra genom α-omvandling definieras som lika. Se huvudartikeln om Beta normal form för detaljer.

Normal formtyp	Definition.
Normal form	Inga β- eller η-reduktioner är möjliga.
Huvud Normal Form	I form av en lambdaabstraktion vars kropp inte är reducerbar.
Svagt huvud Normal form	I form av en lambdaabstraktion.

Syntaxdefinition i BNF

Lambda Calculus har en enkel syntax. Ett lambdakalkylprogram har syntaxen för ett uttryck där,

namn	BNF	Beskrivning
Abstraktion	< uttryck > ::= λ < variabellista > . < uttryck >	Anonym funktionsdefinition.
Ansökningsperiod	< expression > ::= < application-term >
Ansökan	< application-term > ::= < application-term > < item >	Ett funktionsanrop.
Artikel	< application-term > ::= < item >
Variabel	< item > ::= < variabel >	T.ex. x, y, fakta, summa, ...
Gruppering	< item > ::= ( < uttryck > )	Uttryck inom parentes.

Variabellistan definieras som,

  <  variabel-lista  >  :=  <  variabel  >  |  <  variabel  >  ,  <  variabel-lista  > 

En variabel som används av datavetare har syntaxen,

    
   
     
    <  variabel  >  ::=  <  alpha  >  <  extension  >  <  extension  >  ::  =  < extension >   :: =   < extension   -char  >  <  extension  >  <  extension-char  >  ::  =  <  alpha  >  |  <  siffra  >  | _  

Matematiker begränsar ibland en variabel till att vara ett enda alfabetiskt tecken. När du använder denna konvention utelämnas kommatecken från variabellistan.

En lambdaabstraktion har lägre prioritet än en applikation, så;

$\lambda xy\ z=\lambda x.(y\ z)$

Ansökningar lämnas associativa;

$x\ y\ z=(x\ y)\ z$

En abstraktion med flera parametrar är likvärdig med flera abstraktioner av en parameter.

$\lambda xyz=\lambda x.\lambda yz$

var,

• x är en variabel
• y är en variabellista
• z är ett uttryck

Definition som matematiska formler

Problemet med hur variabler kan döpas om är svårt. Denna definition undviker problemet genom att ersätta alla namn med kanoniska namn, som är konstruerade utifrån positionen för definitionen av namnet i uttrycket. Tillvägagångssättet är analogt med vad en kompilator gör, men har anpassats för att fungera inom matematikens begränsningar.

Semantik

Utförandet av ett lambdauttryck fortsätter med följande reduktioner och transformationer,

1. α-omvandling - $\operatornamn {alpha-conv} (a) \till \operatörsnamn {kanonym} [A,P]=\operatörsnamn {kanonym} [a[A],P]$
2. β-reduktion - $\operatörsnamn {beta-redex} [\lambda pb\ v]=b[p:=v]$
3. η-reduktion - $x\inte \i \operatörsnamn {FV} (f)\till \operatörsnamn {eta-redex} [\lambda x.(f\ x)]=f$

var,

• canonym är ett byte av ett lambdauttryck för att ge uttrycket standardnamn, baserat på namnets position i uttrycket.
• Substitution Operator , $b[p:=v]$ är ersättningen av namnet $p$ med lambdauttrycket $v$ i lambdauttrycket $b$ .
• Fri variabeluppsättning $\operatorname {FV} (f)$ är uppsättningen av variabler som inte tillhör en lambdaabstraktion i $f$ .

Exekvering är att utföra β-reduktioner och η-reduktioner på deluttryck i kanonymen till ett lambdauttryck tills resultatet är en lambdafunktion (abstraktion) i normalformen .

Alla α-omvandlingar av ett λ-uttryck anses vara ekvivalenta.

Canonym - kanoniska namn

Canonym är en funktion som tar ett lambda-uttryck och byter namn på alla namn kanoniskt, baserat på deras positioner i uttrycket. Detta kan implementeras som,

${\begin{aligned}\operatörsnamn {kanonym} [L,Q]&=\operatörsnamn {kanonym} [L,O,Q]\\\operatörsnamn {kanonym} [\lambda pb,M,Q ]&=\lambda \operatörsnamn {namn} (Q).\operatörsnamn {kanonym} [b,M[p:=Q],Q+N]\\\operatörsnamn {kanonym} [X\ Y,x,Q] &=\operatörsnamn {kanonym} [X,x,Q+F]\ \operatörsnamn {kanonym} [Y,x,E+S]\\\operatörsnamn {kanonym} [x,M,Q]&=\operatörsnamn { namn} (M[x])\end{aligned}}$

Där N är strängen "N", F är strängen "F", S är strängen "S", + är sammanlänkning och "namn" omvandlar en sträng till ett namn

Kartoperatörer

Karta från ett värde till ett annat om värdet finns i kartan. O är den tomma kartan.

1. $O[x]=x$
2. $M[x:=y][x]=y$
3. $x\neq z\to M[x:=y][z]=M[z]$

Ersättningsoperatör

Om L är ett lambdauttryck är x ett namn och y ett lambdauttryck; $L[x:=y]$ betyder att ersätta x med y i L. Reglerna är,

1. $(\lambda pb)[x:=y]=\lambda pb[x:=y]$
2. $(X\,Y)[x:=y]=X[x:=y]\, Y[x:=y]$
3. $z=x\to (z)[x:=y]=y$
4. $z\neq x\to (z)[x:=y]=z$

Observera att regel 1 måste ändras om den ska användas på lambdauttryck som inte har ändrats till kanon. Se Ändringar av substitutionsoperatören .

Fria och bundna variabeluppsättningar

Uppsättningen av fria variabler för ett lambdauttryck, M, betecknas som FV(M). Detta är uppsättningen av variabelnamn som har instanser som inte är bundna (använda) i en lambdaabstraktion, inom lambdauttrycket. De är variabelnamnen som kan bindas till formella parametervariabler utanför lambda-uttrycket.

Uppsättningen av bundna variabler för ett lambda-uttryck, M, betecknas som BV(M). Detta är uppsättningen variabelnamn som har instanser bundna (använda) i en lambdaabstraktion, inom lambdauttrycket.

Reglerna för de två uppsättningarna ges nedan.

$\mathrm {FV} (M)$ - Fri variabeluppsättning	Kommentar	$\mathrm {BV} (M)$ - Bound Variable Set	Kommentar
$\mathrm {FV} (x)=\{x\}$	där x är en variabel	$\mathrm {BV} (x)=\emptyset$	där x är en variabel
$\mathrm {FV} (\lambda xM)=\mathrm {FV} (M)\setminus \{x\}$	Fria variabler för M exklusive x	$\mathrm {BV} (\lambda xM)=\mathrm {BV} (M)\cup \{x\}$	Bundna variabler för M plus x.
$\mathrm {FV} (M\ N)=\mathrm {FV} (M)\cup \mathrm {FV} (N)$	Kombinera de fria variablerna från funktionen och parametern	$\mathrm {BV} (M\ N)=\mathrm {BV} (M)\cup \mathrm {BV} (N)$	Kombinera de bundna variablerna från funktionen och parametern

Användande;

• Free Variable Set, FV används ovan i definitionen av η-reduktionen .
• Bound Variable Set, BV, används i regeln för β-redex av icke-kanoniskt lambdauttryck.

Utvärderingsstrategi

Denna matematiska definition är strukturerad så att den representerar resultatet och inte hur det beräknas. Men resultatet kan skilja sig mellan lat och ivrigt utvärdering. Denna skillnad beskrivs i utvärderingsformlerna.

Definitionerna som ges här förutsätter att den första definitionen som matchar lambda-uttrycket kommer att användas. Denna konvention används för att göra definitionen mer läsbar. Annars skulle vissa villkor krävas för att göra definitionen exakt.

Att köra eller utvärdera ett lambdauttryck L är,

$\operatörsnamn {eval} [\operatörsnamn {kanonym} [L],Q]$

där Q är ett namnprefix, möjligen en tom sträng och eval definieras av,

${\begin{aligned}\operatörsnamn {eval} [x\ y]&=\operatörsnamn {eval} [\operatörsnamn {apply} [\operatörsnamn {eval} [x]\ \operatörsnamn {strategi} [y] ]]\\\operatörsnamn {apply} [(\lambda xy)\ z]&=\operatörsnamn {kanonym} [\operatörsnamn {beta-redex} [(\lambda xy)\ z],x]\\\operatörsnamn { tillämpa} [x]&=x{\text{ om x matchar ovanstående.}}\\\operatörsnamn {eval} [\lambda x.(f\ x)]&=\operatörsnamn {eval} [\operatörsnamn { eta-redex} [\lambda x.(f\ x)]]\\\operatörsnamn {eval} [L]&=L\\\operatörsnamn {lat} [X]&=X\\\operatörsnamn {ivriga} [ X]&=\operatörsnamn {eval} [X]\end{aligned}}$

Då kan utvärderingsstrategin väljas som antingen,

${\begin{aligned}\operatörsnamn {strategi} &=\operatörsnamn {lat} \\\operatörsnamn {strategi} &=\operatörsnamn {eager} \end{aligned}}$

Resultatet kan vara olika beroende på vilken strategi som används. Ivrig utvärdering kommer att tillämpa alla möjliga minskningar, vilket lämnar resultatet i normal form, medan lat utvärdering kommer att utelämna vissa minskningar av parametrar, vilket lämnar resultatet i "svag huvud normal form".

Normal form

Alla nedsättningar som kan tillämpas har tillämpats. Detta är resultatet från en ivriga utvärdering.

${\begin{aligned}\operatörsnamn {normal} [(\lambda xy)\ z]&=\operatörsnamn {false} \\\operatörsnamn {normal} [\lambda x.(f\ x)]&= \operatörsnamn {false} \\\operatörsnamn {normal} [x\ y]&=\operatörsnamn {normal} [x]\land \operatörsnamn {normal} [y]\end{aligned}}$

I alla andra fall,

$\operatörsnamn {normal} [x]=\operatörsnamn {true}$

Svagt huvud normal form

Reduktioner av funktionen (huvudet) har tillämpats, men inte alla minskningar av parametern har tillämpats. Detta är resultatet som erhålls från att tillämpa lat utvärdering.

${\begin{aligned}\operatörsnamn {whnf} [(\lambda xy)\ z]&= \operatörsnamn {false} \\\operatörsnamn {whnf} [x\ y]&=\operatörsnamn {whnf} [x]\end{aligned}}$

I alla andra fall,

$\operatörsnamn {whnf} [x]=\operatörsnamn {true}$

Härledning av standard från den matematiska definitionen

Standarddefinitionen av lambdakalkyl använder några definitioner som kan betraktas som teorem, vilket kan bevisas baserat på definitionen som matematiska formler .

Den kanoniska namndefinitionen behandlar problemet med variabelidentitet genom att konstruera ett unikt namn för varje variabel baserat på positionen för lambdaabstraktionen för variabelnamnet i uttrycket.

Denna definition introducerar reglerna som används i standarddefinitionen och relaterar förklarar dem i termer av den kanoniska omdöpningsdefinitionen.

Fria och bundna variabler

Lambdaabstraktionsoperatorn, λ, tar en formell parametervariabel och ett kroppsuttryck. När den utvärderas identifieras den formella parametervariabeln med värdet på den faktiska parametern.

Variabler i ett lambdauttryck kan antingen vara "bundna" eller "fria". Bundna variabler är variabelnamn som redan är kopplade till formella parametervariabler i uttrycket.

Den formella parametervariabeln sägs binda variabelnamnet varhelst den förekommer fritt i kroppen. Variabler (namn) som redan har matchats till formell parametervariabel sägs vara bundna . Alla andra variabler i uttrycket kallas fria .

Till exempel, i följande uttryck är y en bunden variabel och x är fri: $\lambda yx\ x\ y$ . Observera också att en variabel är bunden av sin "närmaste" lambdaabstraktion. I följande exempel är den enda förekomsten av x i uttrycket bunden av den andra lambda: $\lambda xy\ (\lambda xz\ x)$

Ändringar av substitutionsoperatören

I definitionen av substitutionsoperatören är regeln,

• $(\lambda pb)[x:=y]=\lambda pb[x:=y]$

måste ersättas med,

1. $(\lambda xb)[x:=y]=\lambda xb$
2. $z\neq x\ \to (\lambda zb)[x:=y]=\lambda zb[x:=y]$

Detta för att stoppa bundna variabler med samma namn som ersätts. Detta skulle inte ha inträffat i ett kanoniskt omdöpt lambdauttryck.

Till exempel skulle de tidigare reglerna ha översatts felaktigt,

$(\lambda xx\ z)[x:=y]=(\lambda xy\ z)$

De nya reglerna blockerar denna ersättning så att den förblir som,

$(\lambda xx\ z)[x:=y]=(\lambda xx\ z)$

Omvandling

Betydelsen av lambda-uttryck definieras av hur uttryck kan transformeras eller reduceras.

Det finns tre typer av transformation:

• α-omvandling : ändra bundna variabler ( alfa );
• β-reduktion : tillämpa funktioner på deras argument ( beta ), anropa funktioner;
• η-reduktion : som fångar en föreställning om extensionalitet ( eta ).

Vi talar också om de resulterande ekvivalenserna: två uttryck är β-ekvivalenta , om de kan β-konverteras till samma uttryck, och α/η-ekvivalens definieras på liknande sätt.

Termen redex , förkortning för reducerbart uttryck , syftar på deltermer som kan reduceras med någon av reduktionsreglerna.

α-omvandling

Alfa-konvertering, ibland känd som alfa-döpning, gör att bundna variabelnamn kan ändras. Till exempel alfa-omvandling av $\lambda xx$ kan ge $\lambda yy$ . Termer som skiljer sig endast genom alfa-omvandling kallas α-ekvivalent .

I en α-konvertering kan namn ersättas med nya namn om det nya namnet inte är fritt i kroppen, eftersom detta skulle leda till att fria variabler fångas in .

$(y\not \ i FV(b)\land a(\lambda xb)=\lambda yb[x:=y])\till \operatörsnamn {alpha-con} (a)$

Observera att substitutionen inte kommer att återkomma i kroppen av lambda-uttryck med formell parameter $x$ på grund av ändringen av substitutionsoperatorn som beskrivs ovan.

Se exempel;

α-omvandling	λ-uttryck	Kanoniskt namn	Kommentar
	$\lambda z.\lambda y.(z\ y)$	$\lambda \operatörsnamn {P} .\lambda \operatörsnamn {PN} .(\operatörsnamn {P} \operatörsnamn {PN} )$	Ursprungliga uttryck.
byter namn på y korrekt till k, (eftersom k inte används i kroppen)	$\lambda z.\lambda k.(z\ k)$	$\lambda \operatörsnamn {P} .\lambda \operatörsnamn {PN} .(\operatörsnamn {P} \operatörsnamn {PN} )$	Ingen förändring av kanoniskt omdöpt uttryck.
byter naivt namn på y till z, (fel eftersom z ledig i $\lambda y.(z\ y)$ )	$\lambda z.\lambda z.(z\ z)$	$\lambda \operatörsnamn {P} .\lambda \operatörsnamn {PN} .({\färg {Röd}\operatörsnamn {PN} }\operatörsnamn {PN} )$	$z$ fångas.

β-reduktion (undviker infångning)

β-reduktion fångar idén om funktionstillämpning (även kallat ett funktionsanrop) och implementerar utbytet av det faktiska parameteruttrycket för den formella parametervariabeln. β-reduktion definieras i termer av substitution.

Om inga variabelnamn är fria i den aktuella parametern och bundna i kroppen, kan β-reduktion utföras på lambdaabstraktionen utan kanoniskt byte av namn.

$(\forall z:z\not \in FV(y)\eller z\not \in BV(b))\to \operatorname {beta-redex} [\lambda xb\ y]=b[x: =y]$

Alfabyte kan användas på $b$ för att byta namn på namn som är fria i $y$ men bundna i $b$ , för att uppfylla förutsättningen för denna transformation.

Se exempel;

β-reduktion	λ-uttryck	Kanoniskt namn	Kommentar
	$(\lambda x.\lambda y.(\lambda z.(\ lambda xz\ x)(\lambda yz\ y))(x\ y))$	$(\lambda \operatörsnamn {P} .\lambda \operatörsnamn {PN} .(\lambda \operatörsnamn {PNF} .(\lambda \operatörsnamn {PNFNF} .\operatörsnamn {PNF} \operatörsnamn {PNFNF} )( \lambda \operatörsnamn {PNFNS} .\operatörsnamn {PNF} \operatörsnamn {PNFNS} ))(\operatörsnamn {P} \operatörsnamn {PN} ))$	Ursprungliga uttryck.
Naiv beta 1,	$(\lambda x.\lambda y.((\lambda x.(x) \ y)x)(\lambda y.(x\ y)y)))$	Kanonisk $(\lambda \operatörsnamn {P} .\lambda \operatörsnamn {PN} .((\lambda \operatörsnamn {PNF} .({\color {Blå}\operatörsnamn {P} }\operatörsnamn {PN} )\ operatörsnamn {PNF} )(\lambda \operatörsnamn {PNS} .(\operatörsnamn {P} {\color {Blå}\operatörsnamn {PN} })\operatörsnamn {PNS} )))$ Naturlig $(\lambda \operatörsnamn {P} .\lambda \operatörsnamn {PN} .((\lambda \operatörsnamn {PNF} .({\color {Röd}\operatörsnamn {PNF} }\operatörsnamn {PN} )\ operatörsnamn {PNF} )(\lambda \operatörsnamn {PNS} .(\operatörsnamn {P} {\color {Röd}\operatörsnamn {PNS} )}\operatörsnamn {PNS} )))$	x (P) och y (PN) har fångats i substitutionen.
Alpha byt namn på inre, x → a, y → b	$(\lambda x.\lambda y.(\lambda z.(\ lambda xz\ a)(\lambda bz\ b))(x\ y))$	$(\lambda \operatörsnamn {P} .\lambda \operatörsnamn {PN} .(\lambda \operatörsnamn {PNF} .(\lambda \operatörsnamn {PNFNF} .\operatörsnamn {PNF} \operatörsnamn {PNFNF} )( \lambda \operatörsnamn {PNFNS} .\operatörsnamn {PNF} \operatörsnamn {PNFNS} ))(\operatörsnamn {P} \operatörsnamn {PN} ))$
Beta 2,	$(\lambda x.\lambda y.((\lambda a.(x) \ y)a)(\lambda b.(x\ y)b)))$	Kanonisk $(\lambda \operatörsnamn {P} .\lambda \operatörsnamn {PN } .((\lambda \operatörsnamn {PNF} .(\operatörsnamn {P} \operatörsnamn {PN} )\operatörsnamn {PNF} )(\lambda \operatörsnamn {PNS} .(\operatörsnamn {P} \operatörsnamn {PN} )\operatörsnamn {PNS} )))$ Naturlig $(\lambda \operatörsnamn {P} .\lambda \operatörsnamn {PN } .((\lambda \operatörsnamn {PNF} .(\operatörsnamn {P} \operatörsnamn {PN} )\operatörsnamn {PNF} )(\lambda \operatörsnamn {PNS} .(\operatörsnamn {P} \operatörsnamn {PN} )\operatörsnamn {PNS} )))$	x och y fångas inte.

${\begin{array}{r}((\lambda xz\ x)(\lambda yz\ y))[z:=(x\ y)]\\((\lambda az\ a)(\ lambda bz\ b))[z:=(x\ y)]\end{array}}$

I det här exemplet,

1. I β-redex,
   1. De fria variablerna är, $\operatorname {FV} (x\ y)=\{x,y\}$
   2. De bundna variablerna är $\operatorname {BV} ((\lambda xz\ x)(\lambda yz\ y))=\{x,y\}$
2. Den naiva β-redexen ändrade innebörden av uttrycket eftersom x och y från den faktiska parametern fångades när uttrycken ersattes i de inre abstraktionerna.
3. Alfabytet tog bort problemet genom att ändra namnen på x och y i den inre abstraktionen så att de skiljer sig från namnen på x och y i den faktiska parametern.
   1. De fria variablerna är, $\operatorname {FV} (x\ y)=\{x,y\}$
   2. De bundna variablerna är $\operatorname {BV} ((\lambda az\ a)(\lambda bz\ b))=\{a,b\}$
4. β-redexen fortsatte sedan med den avsedda betydelsen.

η-reduktion

η-reduktion uttrycker idén om extensionalitet , som i detta sammanhang är att två funktioner är lika om och bara om de ger samma resultat för alla argument.

η-reduktion kan användas utan förändring på lambda-uttryck som inte är kanoniskt byta namn.

$x\not \in \mathrm {FV} (f)\to {\text{η-redex}}[\lambda x.(fx)]=f$

Problemet med att använda en η-redex när f har fria variabler visas i detta exempel,

Minskning	Lambda uttryck	β-reduktion
	$(\lambda x.(\lambda yy\,x)\,x)\,a$	$\lambda aa\,a$
Naiv η-reduktion	$(\lambda yy\,x)\,a$	$\lambda aa\,x$

Denna felaktiga användning av η-reduktion ändrar innebörden genom att lämna x i $\lambda yy\,x$ osubstituerad.