b'\n_START_ARTICLE_\nLambdacalculus\n_START_SECTION_\nApplicatie\n_START_PARAGRAPH_\nApplicatie 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._NEWLINE_De toepassing van  op  wordt in de lambdacalculus genoteerd als . We kunnen  zien als het argument voor ._NEWLINE_Applicatie wordt verwezenlijkt door middel van substitutie zoals voorgeschreven door de \xce\xb2-reductie/het b\xc3\xa8ta-axioma.\n_START_SECTION_\nAbstractie\n_START_PARAGRAPH_\nAbstractie 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 \xc3\xa9\xc3\xa9n variabele benoemd tot (formele) parameter: de geabstraheerde lambdaterm kan dan gereduceerd worden (via \xce\xb2-reductie) door de formele parameter te vervangen door een waarde._NEWLINE_Om aan te geven welke variabele de bijzondere positie inneemt binnen de lambdaterm, wordt de speciale operator lambda (\xce\xbb) 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 \xce\xb2-gelijkheid)._NEWLINE_We zeggen dat de \xce\xbb-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 \xce\xbb-operator. Een dergelijke variabele wordt een gebonden variabele genoemd. In het bovenstaande voorbeeld is de variabele  een gebonden variabele.\n_START_SECTION_\nCurrying\n_START_PARAGRAPH_\nUit de definitie van een lambda-expressie volgt dat een functie in de lambdacalculus slechts \xc3\xa9\xc3\xa9n parameter kan hebben._NEWLINE_Het is echter mogelijk de \xce\xbb-operator zo te defini\xc3\xabren 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\xc3\xb6nfinkel 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 ._NEWLINE_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 \xc3\xa9\xc3\xa9n argument meegeven._NEWLINE_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._NEWLINE_Currying kan ook in de informatica gebruikt worden om gedeeltelijke evaluatie toe te passen wanneer niet alle argumenten van een functie beschikbaar zijn.\n_START_SECTION_\n\xce\xb1-conversie\n_START_PARAGRAPH_\nAlfaconversie laat hernoeming van gebonden variabelen toe. Zo kunnen we bijvoorbeeld  veranderen naar . Lambda-expressies gelijk worden na het toepassen van een of meer \xce\xb1-conversies worden \xce\xb1 -equivalent genoemd._NEWLINE_Bij toepassing van \xce\xb1-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 \xce\xb1-conversie enkel mogelijk als en slechts als er geen vrije variabelen gebonden zouden worden._NEWLINE_Substitutie in de lambdacalculus maakt gebruik van de \xce\xb1-conversie om te vermijden dat vrije variabelen gebonden raken.\n_START_SECTION_\n\xce\xb7-conversie\n_START_PARAGRAPH_\n\xc3\x88taconversie 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.\n_START_SECTION_\nVoorstelling van datatypes\n_START_PARAGRAPH_\nHoewel 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 \xce\xb2-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\xc3\xabncodeerd kunnen worden in de lambdacalculus, evenals enkele voorbeelden van operaties op deze datatypes._NEWLINE_Er is echter een ding waar rekening mee dient gehouden te worden: de lambdacalculus hier gebruikt is niet getypeerd. Er kan dus niet ge\xc3\xabist 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.\n_START_SECTION_\nLeibniz en het Entscheidungsproblem\n_START_PARAGRAPH_\nWiskunde 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._NEWLINE_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 \xe2\x80\x93 het was meer een lappendeken van losse inspanningen en hier en daar een paar inzichten._NEWLINE_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._NEWLINE_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._NEWLINE_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\xc3\xb6del 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._NEWLINE_Na G\xc3\xb6dels 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.\n_START_SECTION_\nTarski en Knaster\n_START_PARAGRAPH_\nIn 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._NEWLINE_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.\n_START_SECTION_\nHet probleem\n_START_PARAGRAPH_\nHet 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._NEWLINE_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._NEWLINE_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._NEWLINE_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.'