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