title: Lambdacalculus
text: 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  kan via vaste regels herschreven worden naar een term . 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  een deel  te vervangen door een ander deel  om zo een term  te bekomen. We noteren dit als
  
  Door middel van meta-expressies kunnen we over de lambdacalculus redeneren. Voorbeelden hiervan zijn de substitutieoperator  en , om de verzameling van vrije variabelen in een expressie  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
  
  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:
  
   Voorbeeld 
  Als voorbeeld van een berekening door reducties beschouwen we eerst een simpele, rekenkundige term:
  
  We kunnen dus ook opschrijven  en ook .
  
  Daarbij hadden we ook een andere volgorde kunnen kiezen:
  
  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 .
  
  Zij V een verzameling variabelen, dan wordt de verzameling van lambdatermen (ook wel lambda-expressies genoemd) Λ als volgt gedefinieerd:
   Een variabele is een lambdaterm: 
   Zijn M en N lambdatermen, dan is de applicatie van M op N een lambdaterm:  (applicatie);
   Is x een variabele en M een lambdaterm, dan is de abstractie over x van M een lambdaterm:  (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  niet in  voor hoeft te komen;  is ook een geldige lambdaterm en wel een abstractie over  in de lambdaterm  (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  in plaats van .
   Applicatie is links associatief. Men kan dus  afkorten tot . De term  wordt dus gelezen als  en niet als . De term reduceert dan ook naar  en niet naar .
   Meerdere opeenvolgende abstracties worden samengevoegd: wordt als  geschreven. 
   Abstractie is rechts associatief. Men kan dus  schrijven als .
   Men kan haakjes weglaten indien dit niet tot ambigue termen of tot fouten leidt. Zo kan men dus in de term  de haakjes weglaten maar in  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
   ; ; ;'''
   en
  .
  
   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  op  wordt in de lambdacalculus genoteerd als . We kunnen  zien als het argument voor .
  
  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  de afbeelding . Zo is bijvoorbeeld  de identiteitsfunctie . 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  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  geldt dat de vrije variabelen, genoteerd als  (of als ), als volgt gedefinieerd zijn:
  
   
   
   
  
  Abstractie bindt parameters. In  wordt de variabele  gebonden in . Een variabele die niet gebonden is heet een vrije (of ongebonden) variabele.
  
  Van een lambdaterm  zegt men dat
    een binding is van  in ;
   het bereik van de binding  is. Dit houdt in dat alle nog niet gebonden voorkomens van  in  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  binnen haakjes gebonden, die erbuiten is vrij:
  
  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  willen uitwerken, moeten we in  ieder voorkomen van  dat gebonden wordt door  vervangen door , met andere woorden moeten we in  de vrije voorkomens van  vervangen door de expressie . Dit noteren we als  en is dus de substitutie van  voor  in . We moeten hierbij echter opletten dat we geen vrije voorkomens van variabelen in  binden, aangezien dit een fout zou genereren.
  
  Zij ,  en  geldige lambdatermen en ,  en  variabelen uit . Dan definiëren we de substitutie van  voor  in , ofwel , als volgt:
   
    als y verschillend is van z
   
   
    als  verschillend is van  en  geen vrije variabele is in 
    als  verschillend is van ,  een vrije variabele is in  en als  geen vrije variabele is in 
  
  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 's in de te substitueren expressie zijn immers gebonden. 
  De laatste regel zorgt ervoor dat we vermijden om per ongeluk vrije variabelen uit  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  is niet verschillend van de term . 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 .
  
  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 ), een verzameling axioma's waar bovenstaande reductietypes op steunen.
  
  De relatie  wordt door volgende axioma's gedefinieerd:
  
  De β-gelijkheid is een equivalentierelatie, zoals aangegeven door de eigenschappen reflexiviteit, transitiviteit en symmetrie en wordt genoteerd als . Bij toepassing van het alfa-axioma kan men er voor kiezen om meer specifiek te zijn en dit te noteren met . De η-reductie kan analoog als  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  gebruiken.
  
   α-conversie 
  Alfaconversie laat hernoeming van gebonden variabelen toe. Zo kunnen we bijvoorbeeld  veranderen naar . 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 . De formele parameter in deze functie is  (in de wiskunde wordt dit de veranderlijke of variabele genoemd). Willen we nu deze functie toepassen op de waarde  (de actuele parameter), dan vullen we deze waarde in het functievoorschrift in. We krijgen . Het bèta-axioma geeft deze situatie weer:  stelt de applicatie van de functie (in de lambdacalculus kunnen we niet echt van een functie spreken, enkel van een lambdaterm)  op het argument (idem)  voor, waarbij  de formele parameter is.
  
  Een aantal voorbeelden:
  
  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  in ) met daarin de gebonden variabele (de  in ) vervangen door de term waarop de abstractie werd toegepast. Dit komt neer op het volgende:
  
  .
  
  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  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 ( en ) zijn de Churchbooleans. Deze worden als volgt gedefinieerd:
  
   is een functie die, gegeven twee argumenten, steeds haar eerste argument teruggeeft,  is een functie die steeds haar tweede argument teruggeeft.
  
  Met behulp van deze voorstellingen kunnen de booleaanse operatoren voorgesteld worden als volgt:
   Logische conjunctie
   
   Logische disjunctie
   
   Logische negatie
   
  
  De operaties op booleans maken gebruik van het feit dat  en  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 . 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  genoemd en de tweede projectie .
  
   Dataconstructor
   
   Eerste projectie
   
   Tweede projectie
   
  
  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  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,  (successor), een aantal keer toe te passen op een basisterm  (zero).
  
  Laat, voor iedere ,  een metaoperatie zijn die twee expressies neemt (bijvoorbeeld  en ) en toelaat om de term  kort te noteren als , waarbij  en .
  
  Met behulp van deze notatie kunnen de Churchnumeralen als volgt gedefinieerd worden:
  
  , met .
  
  De eerste natuurlijke getallen zien er dan als volgt uit:
  
  ...
  
  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: 
   
   De optelling: 
   
   De vermenigvuldiging: 
   
   De predecessorfunctie:  met 
   
   
   
   De aftrekking:    Als , dan is .
   
  
  Deze functies zijn voorbeelden van hoe eenvoudige arithmetische operaties in de lambdacalculus gedefinieerd kunnen worden. Met uitzondering van  zijn deze functies vrij eenvoudig.
  
   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  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 .
  
   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:
  
   : de identiteitscombinator; voor iedere lambdaterm M geldt 
   : de leftfunctie; voor alle lambdatermen M en N geldt 
   : de rightfunctie; voor alle lambdatermen M en N geldt 
   
  
  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:
  
   
  
  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 . 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:
  
  die hij afkortte tot het geordende paar
  
  .
  
  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  en de term "False" als . Immers:
  
  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:  staat voor de weergave in Barendregtnotatie van het cijfer nOm 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  (successor), een term zo dat . Deze term is ; dat dit inderdaad de optelling is, is triviaal zichtbaar.
   Aftrekken in Barendregts notatie gaat met de term  (predecessor), een term zo dat . Deze term is ; 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  en . Deze term is ; immers
   
   
  
  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 , dan kunnen we deze twee getallen optellen door B over te hevelen naar A; als , dan:
  
  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
  
  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:
  
   
   
  
  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 .
  Een dekpunt van f is een element  zo dat .
  
  In 1955 bewezen Tarski en Knaster het volgende:
  Zij  een partieel geordende verzameling
  Zij  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:
  
  Bewijs:
  Definieer  en 
  Dan 
  
  Sterker nog, er is een combinator die, voor iedere term F, een dekpunt oplevert:
  
  Definieer 
  Dan 
  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
  
  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