Lambdacalculus

De lambdacalculus, soms ook als λ-calculus geschreven, is een formeel systeem dat in de wiskunde en theoretische informatica wordt gebruikt om het definiëren en uitvoeren van berekenbare functies te onderzoeken. Hij werd in 1936 door Alonzo Church en Stephen Kleene geïntroduceerd als onderdeel van hun onderzoek naar de grondbeginselen van de wiskunde, maar wordt tegenwoordig vooral gebruikt bij het onderzoeken van berekenbaarheid. De lambdacalculus kan worden gezien als een soort minimale programmeertaal die in staat is elk algoritme te beschrijven. De lambdacalculus is turingvolledig en vormt de basis van het paradigma voor functionele programmeertalen.

De rest van dit artikel gaat over de oorspronkelijke, ongetypeerde lambdacalculus, waarin er geen beperkingen opgelegd worden aan functieapplicatie. De ongetypeerde lambdacalculus heeft geen notie van een domein van een functie. De meeste toepassingen van de lambdacalculus gebruiken echter varianten met een typeaanduiding.

Ongetypeerde lambdacalculus en berekeningsprincipe

De ongetypeerde lambdacalculus is de lambdacalculus zoals ze in 1936 werd geïntroduceerd door Church en Kleene. Deze lambdacalculus beschrijft een berekening als een opeenvolging van termen (ook wel expressies genoemd). De eerste term is de initiële beschrijving van het probleem, al dan niet op te vatten als een algoritme en een invoer voor dat algoritme. De lambdacalculus bestaat uit een verzameling van geldige expressies, die herschreven (lees: vereenvoudigd) kunnen worden. Deze calculus is dan ook een herschrijfsysteem: een term $T$ kan via vaste regels herschreven worden naar een term $T'$. Dit stopt wanneer we de term niet meer kunnen herschrijven door middel van de regels. Het doel is vaak om ieder berekenbaar probleem te schrijven (modelleren) in de vorm van een beginterm, zodat de berekening in een eindig aantal stappen voltooid kan worden.

De lambdacalculus is dus een systeem dat enkel uit geldige λ-expressies bestaat die door middel van een vast systeem omgevormd kunnen worden naar (hopelijk) simpelere expressies. Het schrijven van een expressie naar een simpelere, maar equivalente vorm, heet reductie. Een reductie wordt vaak uitgevoerd door in een term $T$ een deel $E$ te vervangen door een ander deel $E'$ om zo een term $T'$ te bekomen. We noteren dit als

$[E'/E]T=T'$

Door middel van meta-expressies kunnen we over de lambdacalculus redeneren. Voorbeelden hiervan zijn de substitutieoperator $[./.].$ en $VV(E)$, om de verzameling van vrije variabelen in een expressie $E$ aan te duiden. We gebruiken hier dus de metaoperatie voor substitutie. Als deze gelijkheid van links naar rechts wordt toegepast, en dat is meestal het geval, schrijven we ook

$T\longrightarrow T'$

Bestaat de overgang van T naar T' uit een willekeurig aantal reducties (dat wil zeggen geen enkele, precies een, of meer dan een), dan noteren we dat als volgt:

$T\longrightarrow ^{*}T'$

Voorbeeld

Als voorbeeld van een berekening door reducties beschouwen we eerst een simpele, rekenkundige term:

${\begin{matrix}(10+8*4)-(6/3)\ \longrightarrow (10+32)-(6/3)\ \longrightarrow 42-(6/3)\ \longrightarrow 42-2\ \longrightarrow 40\end{matrix}}$

We kunnen dus ook opschrijven $(10+8*4)-(6/3)\longrightarrow ^{*}40$ en ook $(10+8*4)-(6/3)=40$.

Daarbij hadden we ook een andere volgorde kunnen kiezen:

${\begin{matrix}(10+8*4)-(6/3)\ \longrightarrow (10+8*4)-2\ \longrightarrow (10+32)-2\ \longrightarrow 42-2\ \longrightarrow 40\end{matrix}}$

Een term kan dus soms op meerdere manieren gereduceerd worden. Daarbij kan het zijn dat de ene manier veel makkelijker en sneller is dan een andere.

Basisbegrippen

Termen (expressies)

Termen binnen de lambdacalculus worden opgebouwd door het toepassen van een tweetal basisoperaties (abstractie en applicatie) op variabelen uit een oneindige verzameling. In het vervolg zullen we variabelen in lambdatermen aangeven met een aantal typische namen, zoals $x,y,z,v,v',w,\ldots$.

Zij V een verzameling variabelen, dan wordt de verzameling van lambdatermen (ook wel lambda-expressies genoemd) Λ als volgt gedefinieerd:

• Een variabele is een lambdaterm: $v\in V\Rightarrow v\in \Lambda$
• Zijn M en N lambdatermen, dan is de applicatie van M op N een lambdaterm: $M,N\in \Lambda \Rightarrow (MN)\in \Lambda$ (applicatie);
• Is x een variabele en M een lambdaterm, dan is de abstractie over x van M een lambdaterm: $x\in V\land M\in \Lambda \Rightarrow (\lambda x.M)\in \Lambda$ (abstractie).

Door middel van deze definitie kan in de lambdacalculus ieder mogelijk algoritme als lambdaterm voorgesteld worden. Een expressie die niet met behulp van de bovenstaande regels kan worden opgebouwd is geen geldige lambda-expressie.

Bij het laatste punt dient opgemerkt te worden dat $x$ niet in $M$ voor hoeft te komen; $\lambda x.y$ is ook een geldige lambdaterm en wel een abstractie over $x$ in de lambdaterm $y$ (we zullen hieronder zien dat deze term op te vatten valt als een constante).

Vaak wordt de standaardnotatie afgekort, of gebruikt men een eigen, alternatieve notatie. Dit kan, mits men de eigen notatie systematisch toepast, om verwarring te vermijden.

Om de notatie overzichtelijker te maken, worden vaak de volgende conventies gehanteerd:

• De buitenste haakjes worden weggelaten. Men schrijft $MN$ in plaats van $(MN)$.
• Applicatie is links associatief. Men kan dus $((MN)P)$ afkorten tot $MNP$. De term $(\lambda f.\lambda g.fgx)FG$ wordt dus gelezen als $(((\lambda f.\lambda g.fgx)F)G)$ en niet als $(\lambda f.\lambda g.fgx)(FG)$. De term reduceert dan ook naar $FGx$ en niet naar $\lambda g.(FG)gx$.
• Meerdere opeenvolgende abstracties worden samengevoegd:$\lambda x.\lambda y.M$ wordt als $\lambda xy.M$ geschreven.
• Abstractie is rechts associatief. Men kan dus $\lambda x.(\lambda y.(\lambda z.(xyzzyx)))$ schrijven als $\lambda x.\lambda y.\lambda z.xyzzyx$.
• Men kan haakjes weglaten indien dit niet tot ambigue termen of tot fouten leidt. Zo kan men dus in de term $(MN)$ de haakjes weglaten maar in $M(NP)$ niet.

Het is duidelijk dat lambdatermen altijd opgebouwd zijn volgens een bepaalde structuur. Dit is ook de basis van veel bewijzen aangaande de lambdacalculus, de methode van structuurinductie is gebaseerd op het bestaan van deze structuur.

Voorbeelden van lambdatermen zijn $v$ ; $v'w$ ; $\lambda f.\lambda y.fy$ ; $(\lambda w.fw)q$ en $q(\lambda w.fw)$.

Applicatie

Applicatie binnen de lambdacalculus is de analogie van het toepassen van een functie op een argument. In de lambdacalculus kunnen we slechts een term toepassen op een andere term, aangezien de lambdacalculus slechts bestaat uit termen.

De toepassing van $M$ op $N$ wordt in de lambdacalculus genoteerd als $MN$. We kunnen $N$ zien als het argument voor $M$.

Applicatie wordt verwezenlijkt door middel van substitutie zoals voorgeschreven door de β-reductie/het bèta-axioma.

Abstractie

Abstractie is een operatie binnen de lambdacalculus waarin een term "gegeneraliseerd" wordt naar een bepaalde variabele. We construeren m.a.w. het voorschrift van een nieuwe functie. In plaats van een vaste (of constante) variabele te zijn, wordt één variabele benoemd tot (formele) parameter: de geabstraheerde lambdaterm kan dan gereduceerd worden (via β-reductie) door de formele parameter te vervangen door een waarde.

Om aan te geven welke variabele de bijzondere positie inneemt binnen de lambdaterm, wordt de speciale operator lambda (λ) gebruikt. Zij M een in het algemeen van x afhankelijke uitdrukking. Dan is $\lambda x.M$ de afbeelding $x\mapsto M(x)$. Zo is bijvoorbeeld $\lambda x.x$ de identiteitsfunctie $I(x)=x$. Bij applicatie zal men immers steeds het argument terugkrijgen (zie β-gelijkheid).

We zeggen dat de λ-operator een variabele binnen een term bindt: ieder voorkomen van deze variabele binnen de lambdaterm is een verwijzing naar de variabele die genoemd wordt bij de λ-operator. Een dergelijke variabele wordt een gebonden variabele genoemd. In het bovenstaande voorbeeld is de variabele $x$ een gebonden variabele.

Vrije en gebonden variabelen

Het toepassen van een functie op een argument wordt in de lambdacalculus voorgesteld als het vervangen van de formele parameter door een actuele parameter. Hiervoor gebruikt men substitutie. We moeten echter voorzichtig zijn bij het gebruik van substitutie, net zoals in programmeertalen, kan er ook hier shadowing van variabelen optreden.

Het voorkomen van vrije variabelen binnen de lambdacalculus is evenals de calculus zelf inductief gedefinieerd. Voor een lambdaterm $M$ geldt dat de vrije variabelen, genoteerd als $VV(M)$ (of als $FV(M)$), als volgt gedefinieerd zijn:

• $\forall x\in V:VV(x)=\{x\}$
• $VV(MN)=VV(M)\cup VV(N)$
• $VV(\lambda x.M)=VV(M)\setminus \{x\}$

Abstractie bindt parameters. In $\lambda x.M$ wordt de variabele $x$ gebonden in $M$. Een variabele die niet gebonden is heet een vrije (of ongebonden) variabele.

Van een lambdaterm $\lambda x.M$ zegt men dat

• $\lambda x$ een binding is van $x$ in $M$;
• het bereik van de binding $M$ is. Dit houdt in dat alle nog niet gebonden voorkomens van $x$ in $M$ door deze abstractie gebonden worden.

Mocht het nodig zijn de gebonden term af te bakenen, dan gebeurt dat met haakjes om de hele term heen; zo is in het volgende voorbeeld de $x$ binnen haakjes gebonden, die erbuiten is vrij:

$(\lambda x.x)x$

Overigens is het binnen de lambdacalculus gemeengoed om het bovenstaande niet te doen – dat werkt verwarrend. Daarom geldt de afspraak, dat voor gebonden variabelen nooit dezelfde namen gebruikt zullen worden als voor vrije variabelen. Dit wordt algemeen de Barendregtafspraak genoemd. Om aan deze afspraak te voldoen, kan het soms nodig zijn een variabele van naam te veranderen alvorens verder te rekenen. Deze naamsveranderingen worden alleen maar toegepast op gebonden variabelen en kan opgelost worden door middel van de zogenaamde α-reductie.

Een term zonder vrije variabelen heet een gesloten term, ofwel een combinator.

Substitutie

Een functieaanroep, ook wel functieapplicatie genoemd, wordt gerealiseerd door in het functievoorschrift de formele parameters (de variabelen gebruikt in de functiedefinitie) te vervangen door de actuele parameters (de huidige waarden van de formele parameters), zoals beschreven in het bèta-axioma. Wanneer we bijvoorbeeld in $(\lambda y.R)E$ willen uitwerken, moeten we in $R$ ieder voorkomen van $y$ dat gebonden wordt door $\lambda y$ vervangen door $E$, met andere woorden moeten we in $R$ de vrije voorkomens van $y$ vervangen door de expressie $E$. Dit noteren we als $[E/y]R$ en is dus de substitutie van $y$ voor $E$ in $R$. We moeten hierbij echter opletten dat we geen vrije voorkomens van variabelen in $E$ binden, aangezien dit een fout zou genereren.

Zij $E$, $P$ en $R$ geldige lambdatermen en $a$, $y$ en $z$ variabelen uit $V$. Dan definiëren we de substitutie van $y$ voor $E$ in $R$, ofwel $[E/y]R$, als volgt:

1. $[E/y]y=E$
2. $[E/y]z=z$ als y verschillend is van z
3. $[E/y](RP)=([E/y]R)([E/y]P)$
4. $[E/y]\lambda y.R=\lambda y.R$
5. $[E/y]\lambda z.R=\lambda z.[E/y]R$ als $y$ verschillend is van $z$ en $z$ geen vrije variabele is in $R$
6. $[E/y]\lambda z.R=\lambda a.[E/y][a/z]R$ als $y$ verschillend is van $z$, $z$ een vrije variabele is in $R$ en als $a$ geen vrije variabele is in $R$

De derde regel zegt dat bij een applicatie de substitutie moet toegepast worden op beide deelexpressies.
De vierde regel zegt dat als we een substitutie van een variabele moeten toepassen op een binding van die variabele, we niets moeten doen. Alle $y$'s in de te substitueren expressie zijn immers gebonden.
De laatste regel zorgt ervoor dat we vermijden om per ongeluk vrije variabelen uit $R$ te binden. We voeren dan eerst een andere substitutie uit, waarbij we een variabele hernoemen om zo de binding van die variabele te voorkomen. In de laatste regel is ook duidelijk de toepassing van het alfa-axioma te zien.

Currying

Uit de definitie van een lambda-expressie volgt dat een functie in de lambdacalculus slechts één parameter kan hebben. Het is echter mogelijk de λ-operator zo te definiëren dat deze meer variabelen tegelijkertijd kan binden. We spreken dan van een gebonden vector van variabelen. Dit wordt echter vaak achterwege gelaten, omdat zowel Schönfinkel als Haskell Curry rond 1934 bewezen dat deze vectorbinding in feite neerkomt op een meervoudig geabstraheerde term. Het bewijs van Curry leidt tot een omschrijvingsproces voor een dergelijke vector dat nog altijd currying wordt genoemd. Oftewel, een term van de vorm $\lambda xyz.xyzzyx$ is niet verschillend van de term $\lambda x.\lambda y.\lambda z.xyzzyx$. Hierbij is het handig op te merken dat de abstractie als operator rechts associatief is en dat het voorgaande dus gelezen dient te worden als $\lambda x.(\lambda y.(\lambda z.(xyzzyx)))$.

Bekijken we dit even anders. We kunnen een functie van n variabelen namelijk steeds beschouwen als een functie van n-1 variabelen, die als resultaat een functie van 1 variabele heeft. Om de functie dan aan te roepen, roepen we deze meermalen aan, waarbij we telkens één argument meegeven.

Currying is mogelijk in de lambdacalculus omdat de lambdacalculus toelaat dat functies als resultaat opnieuw een functie hebben. Er is met andere woorden ondersteuning voor functies van hogere orde.

Currying kan ook in de informatica gebruikt worden om gedeeltelijke evaluatie toe te passen wanneer niet alle argumenten van een functie beschikbaar zijn.

Equivalentie en reductie

De lambdacalculus is een herschrijfsysteem, dat slechts bestaat uit welgevormde lambda-expressies. De betekenis van die expressies hangt af van hoe deze gereduceerd kunnen worden tot simpelere expressies.

We onderscheiden 3 types van reductie:

• α-conversie: het veranderen van gebonden variabelen;
• β-reductie: het toepassen van een functie op zijn argumenten:
• η-conversie: legt de notie van extensionaliteit vast.

De lambdacalculus kan dus gezien worden als een theorie die de gelijkheid tussen lambdatermen bestudeerd. Om een term verder uit te werken, kan men gebruikmaken van de β-gelijkheid (genoteerd als $=_{\beta }$), een verzameling axioma's waar bovenstaande reductietypes op steunen.

De relatie $=_{\beta }\subset \Lambda \times \Lambda$ wordt door volgende axioma's gedefinieerd:

β	$(\lambda x.M)N=_{\beta }[N/x]M$	β-reductie vertolkt het idee van applicatie: vervanging van de formele parameters door de actuele parameters. Dit is het basisaxioma van de lambdacalculus.
α	$\lambda x.P=_{\beta }\lambda y.[y/x]P$ als $y\not \in VV(P)$	Het alfa-axioma geeft aan dat de naam van de formele parameter in een functiedefinitie onbelangrijk is en vervangen mag worden.
reflexief	$M=_{\beta }M$
transitief	$M=_{\beta }N\wedge N=_{\beta }L\Rightarrow M=_{\beta }L$
symmetrisch	$M=_{\beta }N\Rightarrow N=_{\beta }M$
congruent	$M=_{\beta }M'\Rightarrow \lambda x.M=_{\beta }\lambda x.M'$	Bij een abstractie mogen we het voorschrift reduceren.
congruent	$M=_{\beta }M'\Rightarrow MP=_{\beta }M'P$	We mogen de eerste deelexpressie van een applicatie reduceren alvorens de applicatie zelf te reduceren.
congruent	$P=_{\beta }P'\Rightarrow MP=_{\beta }MP'$	We mogen de eerste deelexpressie van een applicatie reduceren alvorens de applicatie zelf te reduceren.

De β-gelijkheid is een equivalentierelatie, zoals aangegeven door de eigenschappen reflexiviteit, transitiviteit en symmetrie en wordt genoteerd als $=_{\beta }$. Bij toepassing van het alfa-axioma kan men er voor kiezen om meer specifiek te zijn en dit te noteren met $=_{\alpha }$. De η-reductie kan analoog als $=_{\eta }$ geschreven worden.

De axioma's die de equivalentierelatie bepalen (met name de reflexiviteit, de transitiviteit en de symmetrie), horen eigenlijk niet echt bij de β-gelijkheid en worden de axioma's van de gelijkheid genoemd, niet te verwarren met α-, β- en η-gelijkheid. Ook de congruentieregels (ook wel compatibiliteitsregels genoemd) horen niet echt bij de β-gelijkheid, maar zijn zelfstandige axioma's die de basis voor de η-reductie vormen. Toch worden deze axioma's vaak bij de β-gelijkheid vermeld, zoals hierboven. We kunnen bij toepassing hiervan dan ook de notatie $=_{\beta }$ gebruiken.

α-conversie

Alfaconversie laat hernoeming van gebonden variabelen toe. Zo kunnen we bijvoorbeeld $\lambda x.x$ veranderen naar $\lambda q.q$. Lambda-expressies gelijk worden na het toepassen van een of meer α-conversies worden α -equivalent genoemd.

Bij toepassing van α-conversie moet er wel rekening gehouden worden met de bestaande bindingen. Enkel de voorkomens van de variabele die door een bepaalde binding (abstractie) gebonden zijn moeten hernoemd worden. Bovendien is α-conversie enkel mogelijk als en slechts als er geen vrije variabelen gebonden zouden worden.

Substitutie in de lambdacalculus maakt gebruik van de α-conversie om te vermijden dat vrije variabelen gebonden raken.

β-reductie

Het bèta-axioma wordt gezien als het basisaxioma van de lambdacalculus en beschrijft hoe een functieapplicatie moet worden toegepast.

In de informatica wordt functieapplicatie verwezenlijkt door in het functievoorschrift de formele parameters te vervangen door de actuele parameters. Dit kunnen we concreet voorstellen door middel van een voorbeeld uit de wiskunde: neem de kwadraatfunctie $f(x)=x^{2}$. De formele parameter in deze functie is $x$ (in de wiskunde wordt dit de veranderlijke of variabele genoemd). Willen we nu deze functie toepassen op de waarde $4$ (de actuele parameter), dan vullen we deze waarde in het functievoorschrift in. We krijgen $f(4)=4^{2}=16$. Het bèta-axioma geeft deze situatie weer: $(\lambda x.M)N=_{\beta }[N/x]M$ stelt de applicatie van de functie (in de lambdacalculus kunnen we niet echt van een functie spreken, enkel van een lambdaterm) $M$ op het argument (idem) $N$ voor, waarbij $x$ de formele parameter is.

Een aantal voorbeelden:

$(\lambda x.x)M=_{\beta }M$	Wanneer we $xx$ moeten vervangen door $M$, krijgen we uiteraard $M$.
$(\lambda f.fa)(\lambda g.gb)=_{\beta }(\lambda g.gb)a=_{\beta }ab$	Dit voorbeeld toont aan dat in de lambdacalculus iedere term op iedere (andere) term toegepast mag worden, ongeacht de betekenis van deze termen. De lambdacalculus heeft immers geen notie van betekenis en kent enkel lambdatermen. Men zegt dat functies first class (citizens) zijn: niet alleen zijn het toepasbare (taal)onderdelen, maar ook zelfstandige objecten waarmee gerekend kan worden.
$(\lambda x.y)M=_{\beta }y$	Reductie van een redex betekent niet altijd dat het argument deel uitmaakt van de resulterende expressie. De functie die gereduceerd wordt is namelijk een constante functie, die altijd $y$ teruggeeft. Let op dat $(\lambda x.y)M$ niet zomaar geschreven mag worden als $y$! Dit mag enkel na reductie van de applicatie van de functie op een argument.

Een applicatie van een abstractie op een andere term is eigenlijk een speciale situatie in de lambdacalculus. In dit geval ontstaat er namelijk een term die de redex genoemd wordt (als afkorting van reducable expression) en waarop dus een reductie toegepast kan worden. In dit geval wordt zo'n reductie een β-reductie genoemd. De redex reduceert dan naar de gebonden term van de abstractie (bijvoorbeeld $M$ in $\lambda x.M$) met daarin de gebonden variabele (de $x$ in $\lambda x.M$) vervangen door de term waarop de abstractie werd toegepast. Dit komt neer op het volgende:

$(\lambda x.M)N=_{\beta }[N/x]M$.

Dit staat ook bekend als het basisaxioma van de lambdacalculus.

η-conversie

Ètaconversie bepaalt legt de notie van extensionaliteit vast, met andere woorden dat twee functies hetzelfde zijn als en slechts als ze hetzelfde resultaat geven voor ieder mogelijk argument.

Voorstelling van datatypes

Hoewel de lambdacalculus niets anders dan lambdatermen kent, is ze toch even uitdrukkingsrijk als de gewone wiskunde. Voor ieder datatype dat voorgesteld kan worden (bv. getallen en booleanse waarden), kunnen twee types termen onderscheiden worden: enerzijds zijn er de lambdatermen (combinatoren) die de waarden van een datatype zelf voorstellen, anderzijds zijn er combinatoren die de operaties op deze datawaarden voorstellen. Met behulp van β-reductie kan de correctheid van deze combinatoren eenvoudig gecontroleerd worden. Met dit systeem kunnen de datatypes en de operaties op deze datatypes gesimuleerd worden. Vaak zijn echter meerdere datavoorstellingen mogelijk. In deze sectie geven we enkele voorbeelden van datatypes en hoe deze geëncodeerd kunnen worden in de lambdacalculus, evenals enkele voorbeelden van operaties op deze datatypes.

Er is echter een ding waar rekening mee dient gehouden te worden: de lambdacalculus hier gebruikt is niet getypeerd. Er kan dus niet geëist worden dat een bepaalde expressie enkel op bepaalde andere expressies toegepast kan worden. Dit vereist enige systematiek. We kunnen dus perfect de combinator $PLUS$ toepassen op twee booleans, maar het resultaat zal onnuttig zijn. Het voorstellen van datatypes met lambdatermen is dus perfect mogelijk, maar de combinatoren die gebruikt worden hebben op zich eigenlijk geen vaste betekenis en kunnen voor allerlei zaken gebruikt worden. Het is enkel omdat we aan bepaalde combinatoren een bepaalde semantiek toekennen, dat de gevormde datatypes en de operaties op die datatypes nuttig zijn.

Booleans

Een veelgebruikte voorstelling voor booleaanse waarden ($TRUE$ en $FALSE$) zijn de Churchbooleans. Deze worden als volgt gedefinieerd:

$TRUE\equiv \lambda t.\lambda f.t$
$FALSE\equiv \lambda t.\lambda f.f$

$TRUE$ is een functie die, gegeven twee argumenten, steeds haar eerste argument teruggeeft, $FALSE$ is een functie die steeds haar tweede argument teruggeeft.

Met behulp van deze voorstellingen kunnen de booleaanse operatoren voorgesteld worden als volgt:

• Logische conjunctie

$AND\equiv \lambda b_{1}\lambda b_{2}.b_{1}\ \ b_{2}\ \ FALSE$

• Logische disjunctie

$OR\equiv \lambda b_{1}.\lambda b_{2}.b_{1}\ \ TRUE\ \ b_{2}$

• Logische negatie

$NOT\equiv \lambda b.b\ \ FALSE\ \ TRUE$

De operaties op booleans maken gebruik van het feit dat $TRUE$ en $FALSE$ steeds een bepaald argument teruggeven.

Pairs

Pairs (tweetupels) kunnen eveneens eenvoudig in de lambdacalculus voorgesteld worden. Een pair is een datatype dat geconstrueerd kan worden met $CONS$. Deze functie neemt twee argumenten en genereert een tupel, met het eerste argument in de eerste positie en het tweede argument in de tweede positie van het tupel zit. Met behulp van projecties kunnen deze argumenten dan terug uit het tupel verkregen worden. In sommige programmeertalen, zoals bijvoorbeeld Scheme, wordt de eerste projectie $CAR$ genoemd en de tweede projectie $CDR$.

• Dataconstructor

$CONS\equiv \lambda f.\lambda s.\lambda b.b\ \ f\ \ s$

• Eerste projectie

$CAR\equiv \lambda p.p\ \ TRUE$

• Tweede projectie

$CDR\equiv \lambda p.p\ \ FALSE$

In deze voorstelling kan een pair aanzien worden als een functie van één argument die, gegeven een boolean, deze boolean gebruikt om het juiste element uit het pair terug te geven. De projectiefuncties voorzien de juiste boolean. Het is dus de bedoeling dat aan $CONS$ slechts de eerste twee argumenten meegegeven worden voor de constructie van een pair. Deze partiële applicatie is mogelijk door Currying.

Natuurlijke getallen

In de lambdacalculus worden natuurlijke getallen meestal voorgesteld met behulp van zogenaamde Churchgetallen, ook wel Churchnumeralen genoemd. Met deze Churchnumeralen, bedacht door Alonzo Church, valt gemakkelijk de basisrekenkunde in de lambdacalculus te demonstreren.

Een natuurlijk getal wordt voorgesteld door een bepaalde term, $s$ (successor), een aantal keer toe te passen op een basisterm $z$ (zero).

Laat, voor iedere $n$, $(.)^{n}.$ een metaoperatie zijn die twee expressies neemt (bijvoorbeeld $F$ en $M$) en toelaat om de term $FFFF\ldots FM$ kort te noteren als $(F)^{n}M$, waarbij $F^{0}(M)=M$ en $F^{n+1}(M)=F(F^{n}(M))$.

Met behulp van deze notatie kunnen de Churchnumeralen als volgt gedefinieerd worden:

$c_{n}\equiv \lambda s.\lambda z.(s^{n})z$, met $n\in \mathbb {N}$.

De eerste natuurlijke getallen zien er dan als volgt uit:
$0\equiv \lambda s.\lambda z.z$
$1\equiv \lambda s.\lambda z.s\ \ z$
$2\equiv \lambda s.\lambda z.s\ \ (s\ \ z)$
...

Gegeven deze getalvoorstelling kunnen verschillende operatoren gedefinieerd worden. Er zijn wel verschillende manieren op deze operatoren te definiëren. De constructie van deze operatoren zorgt ervoor dat na applicatie het resultaat opnieuw een Churchgetal is.

• De successorfunctie: $succ(n)=n+1$

$SUCC\equiv \lambda n.\lambda s.\lambda z.s\ \ (n\ \ s\ \ z)$

• De optelling: $plus(m,n)=m+n$

$PLUS\equiv \lambda m.\lambda n.\lambda s.\lambda z.m\ \ s\ \ (n\ \ s\ \ z)$

• De vermenigvuldiging: $mult(m,n)=m\cdot n$

$MULT\equiv \lambda m.\lambda n.m\ \ (PLUS\ \ n)\ \ 0$

• De predecessorfunctie: $pred(n)=n-1$ met $pred(0)=0$

$Z\equiv PAIR\ \ 0\ \ 0$

$S\equiv \lambda p.CONS\ \ (CDR\ \ p)\ \ (PLUS\ \ 1\ \ (CDR\ \ p))$

$PRED\equiv \lambda n.CAR\ \ (n\ \ S\ \ Z)$

• De aftrekking: $min(m,n)=m-n$ Als $n<m$, dan is $min(m,n)=0$.

$MIN\equiv \lambda m.\lambda n.n\ \ PRED\ \ m$

Deze functies zijn voorbeelden van hoe eenvoudige arithmetische operaties in de lambdacalculus gedefinieerd kunnen worden. Met uitzondering van $PRED$ zijn deze functies vrij eenvoudig.

$PRED$ maakt gebruik van pairs om de voorganger van een getal te berekenen. Dit werkt op een iteratieve manier. In het pair zitten telkens twee getallen, in de eerste positie zit de voorganger van het getal in de tweede positie. Na $n$ keer de tweede posities te verhogen, en de oude waarde naar de eerste positie van het pair te verplaatsen, vindt men in de eerste positie van het pair het benodigde getal, namelijk $n-1$.

Standaardcombinatoren en Barendregtse rekenkunde

In het voorgaande gedeelte hebben we gezien dat we in de lambdacalculus kunnen rekenen met natuurlijke getallen in de vorm van Churchnumeralen. We hebben gezien dat het mogelijk is termen te definiëren die het mogelijk maken bepaalde, arithmetische operaties uit te voeren op Churchnumeralen.

Churchnumeralen zijn knap gevonden, maar een beetje lastig om mee te werken als je verder wilt kijken dan alleen het rekenen met natuurlijke getallen. In 1979 introduceerde Henk Barendregt een nieuwe notatie voor het rekenen binnen de lambdacalculus die zich makkelijker leent tot andere vormen van rekenen. Om nog verder het gevoel te kweken dat je met de ongetypeerde lambdacalculus alle kanten op kunt, zullen we een aantal termen bespreken die Barendregt zo uitdacht.

Om te beginnen zullen we enige combinatoren, lambdatermen zonder vrije variabelen, definiëren die van belang zijn bij het rekenen met lambdatermen volgens Barendregt:

• ${\mathfrak {I}}=_{\eta }\lambda x.x$: de identiteitscombinator; voor iedere lambdaterm M geldt ${\mathfrak {I}}M=_{\beta }M$
• ${\mathfrak {K}}=_{\eta }\lambda xy.x$: de leftfunctie; voor alle lambdatermen M en N geldt ${\mathfrak {K}}MN=_{\beta }M$
• ${\mathfrak {K}}_{*}=_{\eta }\lambda xy.y$: de rightfunctie; voor alle lambdatermen M en N geldt ${\mathfrak {K}}_{*}MN=_{\beta }N$
• ${\mathfrak {S}}=_{\eta }\lambda xyz.xz(yz)$

Daarnaast wordt een zeer bijzondere positie in Barendregts systeem ingenomen door de dekpuntcombinator. De introductie van de dekpuntcombinator heeft de gehele lambdacalculus veranderd. We zullen de dekpuntcombinator hier alleen maar introduceren; verderop zullen we hem uitgebreid bespreken, samen met een beschouwing van wat het bestaan ervan betekent voor de lambdacalculus. De dekpuntcombinator Y is als volgt gedefinieerd:

• $\mathbb {Y} =_{\eta }\lambda f.(\lambda x.f(xx))(\lambda x.f(xx))$

Barendregt heeft met de bovenstaande combinatoren een redelijk gemakkelijk te begrijpen systeem van termen geïntroduceerd die in uitdrukkingskracht bewijsbaar gelijk zijn aan de turingmachine. Hij deed dit door uit te gaan van de soorten dingen die een taal moet bevatten om dergelijke uitdrukkingskracht te bezitten en deze zaken in de lambdacalculus in te voeren als bruikbare termen.

De twee soorten termen die nodig zijn om een taal te maken die evenveel uitdrukkingskracht heeft als een turingmachine, zijn de repetitie en de selectie. De repetitie is een term die subtermen herhaalt, een loop in termen van een imperatieve programmeertaal. De selectie is een term die een keuze maakt tussen twee mogelijke deeltermen.

Op de repetitie komen we verderop terug. Voor de selectie bedacht Barendregt het volgende, gebaseerd op de veelvoorkomende vorm van een selectie bij de imperatieve talen: als B dan M anders N. Hierin is B een criterium dat evalueert tot een element van de bekende verzameling van George Boole $\{True,False\}$. Als B evalueert tot true wordt M gekozen, als B evalueert tot false wordt N gekozen. Barendregt bedacht dus dat de codering hiervan in de lambdacalculus de volgende vorm moest hebben:

$\lambda f.fMN$

die hij afkortte tot het geordende paar

$[M,N]$.

Barendregt bedacht hiermee dat hij een criterium dat tot True evalueert zou coderen als een term die, gevoed met twee andere termen, als resultaat de eerste van zijn twee argumenten op zou leveren. En een criterium dat tot False evalueert zou dan het tweede op moeten leveren. Gegeven de speciale aandacht die we hebben gegeven aan de bovengenoemde combinatoren, zal het de oplettende lezer niet verbazen dat Barendregt True codeerde als de term ${\mathfrak {K}}$ en de term "False" als ${\mathfrak {K}}_{*}$. Immers:

$[M,N]True\ =_{\beta }\ (\lambda xy.x)MN\ =_{\beta }\ M$

$[M,N]False\ =_{\beta }\ (\lambda xy.y)MN\ =_{\beta }\ N$

Hoe handzaam deze notatie is, blijkt uit de grote hoeveelheid zaken die ermee weergegeven kunnen worden. Zo bedacht Barendregt dat hij natuurlijke getallen kon coderen met deze notatie, analoog aan de eerder besproken Churchnumeralen. In plaats van algemene termen f en x te gebruiken, gebruikte Barendregt echter een vaste terminologie voor de herhaalde f en de x:

Afkorting: $\lceil n\rceil$ staat voor de weergave in Barendregtnotatie van het cijfer n

$\lceil 0\rceil ={\mathfrak {I}}$

$\lceil n+1\rceil =[{\mathfrak {K}}_{*},\lceil n\rceil ]$

Om aan te geven hoe veelzijdig deze notatie van Barendregt is en om het gevoel te kweken dat het een notatie is met een enorme uitdrukkingskracht, zullen we een drietal operaties bespreken die Barendregt op zijn notatie bedacht heeft. Twee van deze notaties zijn rekenkundig, om aan te geven dat Barendregts notatie voor natuurlijke getallen rekenen toestaat. De derde is een term die vaststelt of een bepaald getal gelijk is aan 0, een booleaanse functie dus, die true of false oplevert.

• Optelling in Barendregts notatie gaat met de term $S^{+}$ (successor), een term zo dat $S^{+}\lceil n\rceil =\lceil n+1\rceil$. Deze term is $S^{+}=_{\eta }\lambda x.[{\mathfrak {K}}_{*},x]$; dat dit inderdaad de optelling is, is triviaal zichtbaar.
• Aftrekken in Barendregts notatie gaat met de term $P^{-}$ (predecessor), een term zo dat $P^{-}\lceil n+1\rceil =\lceil n\rceil$. Deze term is $P^{-}=_{\eta }\lambda x.x{\mathfrak {K}}_{*}$; immers, False als argument aan een tupel geven levert de rechterterm van dat tupel op en de rechterterm van een getal in Barendregts notatie is de directe voorganger van dat getal. Merk ook op dat het niet werkt voor 0; dit klopt ook precies, want 0 heeft geen voorganger in de natuurlijke getallen.
• De functie ZERO van Barendregt is een term zo dat $ZERO\lceil 0\rceil =True$ en $ZERO\lceil n+1\rceil =False$. Deze term is $ZERO=_{\eta }\lambda x.x{\mathfrak {K}}$; immers
  • $ZERO\lceil 0\rceil =_{\beta }(\lambda y.y){\mathfrak {K}}=_{\beta }{\mathfrak {K}}=_{\eta }True$
  • $ZERO\lceil n+1\rceil =_{\beta }[{\mathfrak {K}}_{*},\lceil n\rceil ]{\mathfrak {K}}=_{\beta }{\mathfrak {K}}_{*}=_{\eta }False$

Naast een mechanisme om een keuze te maken tussen twee deeltermen gebruikte Barendregt ook een termenmechanisme dat herhaling van deeltermen mogelijk maakt. Hiermee breidde hij zijn notatiesysteem uit tot het bereik qua uitdrukkingskracht van de turingmachine. Barendregt maakte daarvoor gebruik van een bijzonder soort herhaling, die binnen de lambdacalculus echter vaak gebruikt wordt: de recursie, het definiëren van een term A waarbij A een deelterm is van zichzelf.

Als voorbeeld hiervan bespreken we een mogelijkheid om twee natuurlijke getallen op te tellen, die bestaat uit een recursieve functie. Stel dat we de getallen A en B bij elkaar op willen tellen. Nemen we aan dat $B\not =0$, dan kunnen we deze twee getallen optellen door B over te hevelen naar A; als $B\not =0$, dan:

$A+B=(A+1)+(B-1)$

Is B wel gelijk aan 0, dat is de uitkomst A en zijn we klaar. We zouden dus als volgt een optelalgoritme kunnen maken:

ADD.A.B = ALS B = 0 DAN A ANDERS ADD.(A+1).(B-1)

Barendregt introduceerde herhaling in zijn lambdacalculus door gebruik te maken van dit soort recursie.

Het probleem dat zich aandient voor de lezer die hetzelfde wil proberen, is dat het bovenstaande niet eindig uit te drukken is in de lambdacalculus. Na een paar vertalingen met behulp van η-gelijkheid zal de lezer meemaken dat zijn vertaling van voren af aan begint. Als directe vertaling toegepast wordt, wordt de vertaling dus een oneindig lange rij lambda's. Een vertaling is echter wel mogelijk als we opmerken dat we op zoek zijn naar een uitdrukking dusdanig dat

ADD = ALS.ADD

waarbij we de lambdanotatie een beetje misbruiken; we zoeken dus een uitdrukking dusdanig dat ADD een term is gelijk aan de ALS-term toegepast op ADD. Om redenen die we verderop uiteen zullen zetten, kan een dergelijke term uitgerekend worden; zij is gelijk aan

$ADD\ XY=_{\eta }\mathbb {Y} {\mbox{ALS Y = 0 DAN X ANDERS a }}(S^{+}X)(P^{-}Y)$

waarmee ook het enorme belang van de dekpuntcombinator binnen de lambdacalculus duidelijk wordt.

Naast deze uitdrukkingen toonde Barendregt aan dat het met zijn notatie mogelijk is alle mogelijkheden van de functionele programmeertalen direct te modelleren in de lambdacalculus. Niet alleen de basisbewerkingen, maar ook datastructuren als lijsten en de bijbehorende bewerkingen passen op natuurlijke wijze in dit schema.

Lambdacalculus als model van berekening

Leibniz en het Entscheidungsproblem

Wiskunde is sinds de eerste dagen der mensheid een onderdeel van de kennisbundel van de mensheid geweest. Beginnend bij de dagen dat het nodig werd zakken graan te tellen tot aan het in een bepaalde windrichting richten van tempels en piramiden, van het voorspellen van overstromingen van de Nijl tot aan de prachtigste architectuur, wiskunde heeft altijd een rol gespeeld.

Sinds de hoogtijdagen van de oude, Griekse beschavingen zijn er ook mensen geweest die niets anders deden dan zich intellectueel richten op de uitbreiding van de wiskundige kennis en het begrijpen van hoe het rekenen in zijn werk gaat: de wiskundigen. Hun inspanningen waren echter tot aan het einde van de 17e eeuw niet aan te merken als een verbonden geheel – het was meer een lappendeken van losse inspanningen en hier en daar een paar inzichten.

Vanaf 1675 begon dat allemaal te veranderen met de publicaties van Gottfried Leibniz. Hij begon voor het eerst vragen te stellen over de diepere structuur van de wiskunde, te zoeken naar een systeem in het geheel van inzichten en kennis dat zo langzamerhand opgebouwd was. Hij stelde als ideaalbeeld een universele taal voor waarin alle wiskundige problemen uitgedrukt konden worden en een universele methode waarmee al deze problemen opgelost konden worden. Leibniz stierf in 1716 en zijn opvolgers, waaronder George Boole, bleven druk zoeken naar antwoorden op zijn vragen.

Rond 1877 publiceerde Georg Cantor zijn werk over verzamelingenleer. Het was het begin van een serie aardverschuivingen in de wiskunde die tot 1950 zou duren en het wezen van de wiskunde voor eeuwig zou veranderen. Met de verzamelingenleer, na aanpassingen door Ernst Zermelo en Adolf Fraenkel, was Leibniz' universele taal geboren.

Het vraagstuk van de universele methode bleef echter langer open. David Hilbert nam het vraagstuk der berekening op in zijn lijst van uitdagingen aan de wiskunde van 1900. In 1931 maakte Kurt Gödel een ruw einde aan Leibniz' droom door te bewijzen dat sommige dingen niet berekenbaar zijn in de universele taal van de wiskunde. Sterker nog, hij bewees dat in iedere, universele taal zaken moeten zitten die onberekenbaar zijn.

Na Gödels onthutsende ontdekking maakte het probleem van berekening plaats voor het probleem van beslisbaarheid, inmiddels bekend als het Entscheidungsproblem: het probleem van het bepalen of iets berekenbaar is of niet. Dit probleem kon niet direct beantwoord worden, want eerst moest bepaald worden hoe een berekening precies plaatsvond.

Lambdacalculus en de turingmachine

In 1936 volgden twee antwoorden op het openstaande probleem van berekenbaarheid: de turingmachine van Alan Turing en de lambdacalculus van Alonzo Church. Beide zijn absolute modellen van berekening.

Zoals eerder uiteengezet, is het in de lambdacalculus mogelijk zowel de selectie- als de herhalingsfunctie van de turingmachine te modelleren. Ook is het mogelijk, door middel van het doorgeven van argumentwaarden van de ene functieaanroep naar de volgende, de toestand bij te houden. Hiermee wordt de lambdacalculus in uitdrukkingskracht gelijk aan de turingmachine, die in feite niets anders doet dan het eindeloos herhalen van de slag "lees de toestand uit, kies een reactie om uit te voeren, voer hem uit, ga verder".

De turingmachine werd rond 1936 ontwikkeld door Alan Turing als antwoord op het Entscheidungsproblem van Leibniz, Hilbert en Gödel: het is een model van berekening waarin bepaald kan worden of een probleem opgelost kan worden of niet. Sindsdien is het algemeen geaccepteerd dat de uitdrukkingskracht van deze machine overeenkomt met hetgeen berekenbaar is, hoewel dat niet bewijsbaar is. Vrijwel onmiddellijk na de introductie van de Machine begon er een trans-Atlantisch touwtrekken tussen Turing en Alonzo Church, bedenker van de lambdacalculus, om wiens mechanisme het meest algemeen was. De briefwisseling tussen de twee nam de vorm aan van A stuurt B een algoritme uitgedrukt in zijn mechanisme, B reageert met een equivalente uitwerking in zijn mechanisme. In 1938 was Turing het zat en publiceerde hij een algemeen mechanisme om turingmachines te vertalen in lambdacalculus en omgekeerd. Sindsdien twijfelt niemand er meer aan dat de beide mechanismen totaal verschillend en geheel equivalent zijn.

Tegelijkertijd zijn beide mechanismen een bedroevend antwoord op het beslissingsprobleem: niet alle problemen zijn beslisbaar. Het antwoord van Turing was een machine die oneindig door zou kunnen lopen, het antwoord van Church een term die eindeloos groter wordt, of een die gelijk van grootte blijft, en nooit convergeert tot een eindterm:

1. $(\lambda x.xx)(\lambda x.xx)\Rightarrow _{\beta }(\lambda x.xx)(\lambda x.xx)$
2. $(\lambda x.xxx)(\lambda x.xxx)\Rightarrow _{\beta }(\lambda x.xxx)(\lambda x.xxx)(\lambda x.xxx)$

De equivalentie van de twee mechanismen heeft grote gevolgen gehad. Met name van belang voor de lambdacalculus is dat zij niet verdwenen is toen het turingmodel het model van de algemeen bekende computer werd. De elegantie in combinatie met kracht van de lambdacalculus zorgt er niet alleen voor dat er voortgaand onderzoek aan gedaan wordt en dat de lambdacalculus zich een plaats heeft gewonnen als achterliggend model voor een hele klasse van eigen programmeertalen naast de op de turingmachine gebaseerde talen, maar dat de lambdacalculus naast de turingmachine een basis is geworden voor het menselijk begrip van berekenbaarheid, uitdrukkingsmechanisme en van het wezen van de wiskunde als geheel. Uiteenlopend van de basisrekenkunde tot de formalismen van taalvorming en beschouwingen over compleetheid en consistentie van de formele talen is de lambdacalculus een mechanisme waarop wetenschappers steeds weer teruggrijpen om hun begrip aan op te hangen en om hen door het onbekende gebied van het wiskundig onderzoek te leiden naar nieuwe inzichten en dieper begrip van de wiskundige realiteit.

Tarski en Knaster

In 1955 publiceerden Alfred Tarski en Bronislaw Knaster een cruciaal gebleken artikel over dekpunten. Hun werk maakte het voor onderzoekers in de lambdacalculus mogelijk een hoge vlucht te nemen door recursie in de lambdacalculus te integreren als model van berekening.

In 1969 publiceerden David Park en Scott Landin echter een vervolg waarin zij demonstreerden dat de lambdacalculus inherent een bijzonder grove fout bevat waardoor het geen goed model van berekening is. Daarvoor baseerden zij zich op de dekpunten van Tarski en Knaster. In tegenstelling tot de verwachtingen bleek het slechte nieuws van Park en Landin het begin van een geheel nieuwe tak van lambdacalculus die niet alleen wel een accuraat model van berekening bleek, maar zelfs veelzijdiger was dan de al bekende calculus.

De dekpuntcombinator

Gegeven is een functie $f:V\rightarrow V$. Een dekpunt van f is een element $v\in V$ zo dat $f(v)=v$.

In 1955 bewezen Tarski en Knaster het volgende:

Zij $V$ een partieel geordende verzameling

Zij $f:V\rightarrow V$ een functie die de ordening op V in stand houdt

Zij het ook zo dat iedere, eindige deelverzameling van V een supremum en een infimum heeft

Dan is de verzameling van dekpunten van f in V een verzameling

die niet leeg is

die partieel geordend is

waarvan iedere, eindige deelverzameling een supremum en een infimum heeft.

Het belang hiervan voor de lambdacalculus is evident en in het voorgaande al gedemonstreerd: voor een interessante klasse van termen is het mogelijk een dekpunt te vinden en zo een recursieve functie te definiëren.

In 1969 kwamen Park en Landin met onthutsend nieuws, dat in eerste instantie niet zo slecht leek. In de lambdacalculus bestonden er namelijk wel veel meer dekpunten dan beschreven door Tarski en Knaster. Sterker nog, Park en Landin bewezen dat in de lambdacalculus voor iedere term F een dekpunt bestond:

$\forall _{F\in \Lambda }(\exists _{X\in \Lambda }:(FX=_{\beta }X))$

Bewijs:

Definieer $W=_{\eta }\lambda x.F(xx)$ en $X=_{\eta }WW$

Dan $X=_{\eta }WW=_{\eta }(\lambda x.F(xx))W=_{\beta }F(WW)=_{\eta }FX$

Sterker nog, er is een combinator die, voor iedere term F, een dekpunt oplevert:

Definieer $Y=_{\eta }\lambda f.(\lambda x.f(xx))(\lambda x.f(xx))$

Dan $\forall _{F\in \Lambda }(F(YF)=_{\beta }YF)$

Bewijs:Schrijf de rechterkant uit – uit de voorgaande stelling volgt dan deze stelling

Merk op dat de dekpuntcombinator de droom is van iedereen die met recursie werkt: vul een functie of vergelijking in en hij wordt recursief opgelost.

Op zich klinkt hier niets slechts aan. Sterker nog, het bovenstaande klinkt als geweldig nieuws: alles wat je maar bedenken kunt, is op te lossen. Echter, Park en Landin wezen erop dat hun dekpuntcombinator een zeer onaangename eigenschap van de lamdacalculus aantoonde. Beschouw namelijk de functie

$succ:\mathbb {R} \rightarrow \mathbb {R}$

$succ(r)=r+1$

Intuïtief zal duidelijk zijn: deze functie heeft geen dekpunt. Er is geen reëel getal r zo dat r + 1 = r. Met de dekpuntcombinator is een dergelijke waarde er echter wel.

Het is nu verleidelijk te zeggen dat dit betekent dat de lambdacalculus dus te veel kan. Maar de realistische kijk op de ontdekking van Park en Landin is niet dat de lambdacalculus te sterk is, maar dat de lamdacalculus bepaalde dingen gewoon verkeerd doet. Bepaalde aspecten van de lambdacalculus zijn onwenselijk. De lambdacalculus is geen goed model van berekening.

Het probleem

Het probleem dat door Landin en Park aan de oppervlakte gebracht werd, heeft kort door de bocht de volgende oorzaak: de lambdacalculus heeft geen concept van het idee dat bepaalde termen niet op andere termen mogen worden toegepast.

Blijven we even bij het voorbeeld van de successorfunctie van hierboven, dan merken we op dat de dekpuntcombinator voor deze functie een dekpunt oplevert. Kijken we wat indringender naar dit dekpunt, bijvoorbeeld met behulp van de eerder gegeven definitie van succ, dan merken we het volgende op: het gevonden dekpunt is weliswaar een dekpunt gegeven de definitie van succ, maar het dekpunt is niet een getal zoals wij getallen gedefinieerd hadden. Het was nooit onze bedoeling succ toe te passen op een term van de vorm van het gevonden dekpunt.

Het ontbeert de ongetypeerde lambdacalculus dus aan een manier om aan te geven dat bepaalde termen niet van toepassing zijn op bepaalde andere termen. Of, omgekeerd, om aan te geven op welke termen een gegeven term wel toegepast mag worden.

Het antwoord op het probleem van Park en Landin kwam al snel, met de introductie van nieuwe soorten lambdacalculus, calculi die wel een manier hadden om aan te geven welke combinaties wel en niet toegestaan zijn. Deze calculi maken gebruik van schema's om, bij een term, de vorm van toegestane argumenten aan te geven. Er zijn veel specifieke soorten van dit soort schema's, maar als verzamelnaam worden deze schema's typesystemen genoemd. Hun combinatie met de lambdacalculus resulteerde in wat wij tegenwoordig de getypeerde lambdacalculus noemen.

Externe bronnen

• Henk Barendregt & Erik Barendsen, Introduction to Lambda Calculus, Revised edition October 1994
• Henk Barendregt & Erik Barendsen, Introduction to Lambda Calculus, Revised edition December 1998, March 2000
• Mark Scheffer, The theory of the foundations of mathematics – 1870 to 1940, maart 2002