Lambdacalculus

Uit Wikipedia, de vrije encyclopedie
Ga naar: navigatie, zoeken
Principes
Computationele complexiteitstheorie
Modellen
Algoritme
Turingmachine
Lambdacalculus
Theorieën
Berekenbaarheid
Complexiteitsgraad
NP-volledig

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 Turing-volledig en vormt de basis van het paradigma voor functionele programmeertalen.

De rest van dit artikel gaat over de oorspronkelijke, ongetypeerde lambdacalculus. De meeste toepassingen gebruiken varianten daarvan met een type-aanduiding.

Ongetypeerde lambdacalculus[bewerken]

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. 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. Vanuit iedere term T in de reeks volgt de opvolgende term T door T volgens een vaste regel om te schrijven naar T'. De lambdacalculus is dus een voorbeeld van een herschrijfsysteem.

Principe van berekening in lambdacalculus[bewerken]

Het principe van berekening in lambdacalculus is het nemen van een term T en dan een stuk van T (te noemen E) vervangen door een ander stuk (te noemen E' ). Zo vinden we een volgende term T' . We noteren dit als

T[E'/E] = T'

Het vervangen van een onderdeel E door E' heet in een termherschrijfsysteem een reductie, omdat in het algemeen E' een vereenvoudigde vorm van E is. 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'

Een dergelijke berekening eindigt als er geen stukken meer zijn die vervangen kunnen worden. Een doel binnen herschrijven, en dus in het bijzonder binnen de lambdacalculus (als model van berekenbaarheid), is om ieder berekenbaar probleem te kunnen modelleren in de vorm van een beginterm zodanig dat de berekening niet oneindig veel stappen kan duren.

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 reduceren; er leiden dan meerdere wegen naar Rome.

Termen[bewerken]

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.

Voor de vorm van lambdatermen geldt het volgende:

Zij V de verzameling variabelen en Λ de verzameling lambdatermen. Dan geldt:
  • 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
  • Is x een variabele en M een lambdaterm, dan is de abstractie over x van M een lambdaterm: x \in V \and M \in \Lambda \Rightarrow \lambda x.M[x] \in \Lambda
Als een expressie niet met behulp van de bovenstaande regels kan worden opgebouwd, is het geen lambdaterm.

Bij het voorlaatste 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).

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:


\begin{matrix}
v\\
v' w\\
\lambda f.\lambda y.f y\\
(\lambda w.f w) q\\
q (\lambda w.f w)\\
\end{matrix}

Het verrassende is, dat met behulp van deze twee basisconstructies, elk mogelijke algoritme kan worden gerepresenteerd.

Abstractie[bewerken]

Abstractie is een operatie binnen de lambdacalculus waarin een term "gegeneraliseerd" wordt naar een bepaalde variabele. In plaats van een vaste (of constante) variabele te zijn, wordt één variabele benoemd tot naam voor een open plek in de lambdaterm: de geabstraheerde lambdaterm kan dan gereduceerd worden (via β-reductie) door op de open plek een specifieke term in te vullen.

Om aan te geven welke variabele de bijzondere positie inneemt binnen de lambdaterm, wordt de speciale operator λ gebruikt, hiernaar is ook de lambdacalculus genoemd. Zij M een in het algemeen van x afhankelijke uitdrukking. Dan is

\lambda x.M

de afbeelding

x\mapsto M.

Bijvoorbeeld:

\lambda x.x

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.

Een niet-gebonden variabele wordt daarentegen een vrije variabele genoemd. In het volgende voorbeeld is x gebonden en zijn y en z vrij:

z\ \lambda x. yx

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 FV(M), als volgt zijn:

  • x \in V \Rightarrow FV(x) = \{x\}
  • M, N \in \Lambda \Rightarrow FV(MN) = FV(M)\cup FV(N)
  • M \in \Lambda, x \in V \Rightarrow FV(\lambda x.M[x]) = FV(M) - \{x\}

Qua notatie wordt de λ-operator door een punt gescheiden van de lambdaterm die de operator bindt. Binnen die term is ieder voorkomen van de gebonden variabele een verwijzing, dus gebonden. Binnen de gebonden term kan de gebonden variabele niet ook als vrije variabele voorkomen. 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, waar we ons in het vervolg aan zullen houden, dat voor gebonden variabelen nooit dezelfde namen gebruikt zullen worden als voor vrije variabelen. Dit wordt algemeen de Barendregt-afspraak 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; dit heet α-conversie of α-reductie en bestaat uit de totale vervanging van een gebonden variabele in een gebonden term:

\lambda x.M \longrightarrow_\alpha \lambda y.M[y/x]

Als één term door α-conversie overgaat in een andere, zeggen we dat deze termen α-gelijk aan elkaar zijn:

\lambda x.M =_\alpha \lambda y.M[y/x]

Bijvoorbeeld:

\lambda x.xyzx \longrightarrow_\alpha \lambda w.wyzw, dus
\lambda x.xyzx =_\alpha \lambda w.wyzw

We vinden in feite dat dit dezelfde termen zijn (omdat een gebonden variabele niet echt een variabele is, maar een naam voor een open plek waar iets ingevuld kan worden). We onderscheiden twee termen dus alleen als hun vrije variabelen niet hetzelfde zijn, dat wil zeggen, M \not= N \Leftrightarrow FV(M) \cap FV(N) = \empty.

Het is 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 x,y,z.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 bovenstaande dus gelezen dient te worden als

\lambda x.(\lambda y.(\lambda z.(xyzzyx)))

Ten slotte nog één definitie: een abstractie zonder vrije variabelen heet een combinator.

Applicatie[bewerken]

Applicatie binnen de lambdacalculus is de analogie van het toepassen van een functie op een argument. Behalve natuurlijk dat de lambdacalculus die dingen helemaal niet kent als concept, de lambdacalculus kan alleen termen toepassen op andere termen.

Een applicatie in de lambda bestaat eruit een term, de toegepaste term, voor een andere term, de andere term, te plaatsen. De toepassing van M op N in de lambdacalculus bijvoorbeeld is

M.N

wat vaak afgekort wordt tot

MN

β-reductie[bewerken]

Een applicatie van een abstractie op een andere term is een speciale situatie in de lambdacalculus. In dit geval ontstaat er namelijk een term, een redex genoemd, een afkorting van reducable expression, waarop een reductie toegepast kan worden. In dit speciale geval wordt zo'n reductie een β-reductie genoemd. De redex, de gehele applicatie, reduceert dan naar de gebonden term van de abstractie met daarin de gebonden variabele vervangen door de term waarop de abstractie werd toegepast. Dit klinkt ingewikkelder dan het is; het komt in feite neer op het volgende:

(\lambda x.M) N \longrightarrow_{\beta} M[N/x],

ook bekend als het basisaxioma van de lambdacalculus.

De Barendregt-afspraak, die we hierboven hebben vastgesteld, is hierbij belangrijk. Zonder die afspraak zou het voor kunnen komen, dat een vrije variabele uit N na de reductie door een abstractie uit M wordt gebonden en dit is niet de bedoeling. Mocht zo'n ongewenste binding toch voorkomen, dan moeten we de betrokken gebonden variabele eerst middels α-conversie hernoemen.

Een aantal voorbeelden:

\begin{matrix}(\lambda x.x)M \longrightarrow_\beta M \\
(\lambda f.f a) (\lambda g.g b) \longrightarrow_\beta (\lambda g.g b) a \longrightarrow_\beta a b \\
(\lambda x.y) M \longrightarrow_\beta y \end{matrix}

Deze voorbeelden tonen een aantal zaken die wellicht niet intuïtief zijn. In het tweede voorbeeld wordt bijvoorbeeld een abstractie op een abstractie toegepast. In de lambdacalculus mag dit; iedere term kan op iedere andere term toegepast worden, ongeacht wat de verschillende termen precies zijn in de functionele programmeertalen die van de lambdacalculus zijn afgeleid, zegt men ook wel dat functies 'first class citizens' zijn, het zijn niet alleen toepasbare taalonderdelen, maar ook opzichzelfstaande objecten waarmee kan worden gerekend. Zoals uit het voorbeeld duidelijk wordt, kan het resultaat van een dergelijke reductie ook weer een redex zijn.
Het derde voorbeeld laat zien dat het reduceren van een redex niet altijd wil zeggen dat het argument weer terugkomt, het derde voorbeeld waarbij in y de x niet voorkomt is een constante functie, waarvan de reductie altijd y is. Merk op dat dit niet wil zeggen dat je voor \lambda x.y meteen y mag opschrijven! Er moet echt een reductie plaatsvinden, met een argument.

Applicatie is links-associatief. Dat wil zeggen dat (\lambda f.\lambda g. f g x)F G wordt gelezen als (((\lambda f.\lambda g. f g x)F) G) en niet als (\lambda f.\lambda g. f g x)(F G). De term reduceert dan ook naar F G x en niet naar \lambda g. (F G) g x.

Lambdacalculus en algoritmen[bewerken]

In deze sectie zullen we proberen gevoelsmatig aan te tonen dat de lambdacalculus, hoe weinig het ook lijkt op de rekenkunde die bekend is van basisschool en middelbare school, toch in staat is om berekeningen uit te drukken. Sterker nog, we zullen laten zien dat de lambdacalculus even uitdrukkingsrijk is als de wiskunde, zoals velen die in de klassieke uitdrukkingswijze hebben leren kennen en ook even uitdrukkingsrijk is als enige programmeertaal.

Enige axioma's[bewerken]

Om te beginnen, noemen we even kort een aantal axioma's van de lambdacalculus. Deze axioma's zullen niet verrassen, maar het is toch belangrijk ze te hebben genoemd.

Om te beginnen zijn er de axioma's van de gelijkheid, niet te verwarren met α-, β- en η-gelijkheid, wat meer vormen van equivalentie zijn:

Voor alle M,N,L \in \Lambda:

Er zijn ook een aantal compatibiliteitsregels die in feite de basis vormen van η-reductie:

  • M = M' \Rightarrow MZ = M'Z
  • M = M' \Rightarrow ZM = ZM'
  • M = M' \Rightarrow \lambda x.M = \lambda x.M'
Churchnumeralen[bewerken]

Churchnumeralen zijn een manier om in de lambdacalculus natuurlijke getallen weer te geven. Met deze Churchnumeralen, bedacht door Alonzo Church, valt gemakkelijk de basisrekenkunde in de lambdacalculus te demonstreren.

Het idee achter Churchnumeralen is geleend van de structuur van de natuurlijke getallen. Een manier om de natuurlijke getallen te beschrijven is als volgt:

0 \in \N
n \in \N \Rightarrow n + 1 \in \N

Introduceren we nu een functie succ (de successor, opvolger) op de natuurlijke getallen als succ(n) = n + 1, dan staat hierboven in feite

0 \in \N
n \in \N \Rightarrow succ(n) \in \N

Oftewel, de natuurlijke getallen zijn 0, succ(0), succ(succ(0)), succ(succ(succ(0))), enzovoorts.

Deze structuur wordt ook gebruikt in Churchnumeralen, waarin een natuurlijk getal wordt gerepresentateerd als een aantal toepassingen van een term F op een basisterm M. Definieer inductief de betekenis van F^{n}(M) als volgt:

F^{0}(M) = M
F^{n+1}(M) = F(F^{n}(M))

Dan worden de Churchnumeralen als volgt gedefinieerd:

c_{n} =_\eta \lambda fx.f^{n}(x), met n \in \{0, 1, 2, 3, 4, 5, \ldots\}

Nu introduceren we de term A_{+}, een term die de optelling van Churchnumeralen bewerkstelligt:

A_{+} =_\eta \lambda xypq.xp(ypq)

Er geldt namelijk:

\begin{matrix} & A_{+}c_{n}c_{m} \\
=_\beta & \lambda pq. c_{n} p (c_{m} p q) \\
=_\beta & \lambda pq. c_{n} p (p^{m} q) \\
=_\beta & \lambda pq.p^{n}(p^{m} q) \\
=_\eta & \mbox{(Herhaald toepassen bovenstaande definitie:) } & \lambda pq. p^{n + m}(q) \\
=_\alpha & \lambda fx. f^{n + m}(x)\\
=_\eta & c_{n + m}
\end{matrix}

Naast A_{+} kennen we ook A_{*}, de vermenigvuldiging van Churchnumeralen. Deze term is A_{*} =_\eta \lambda xyz.x(yz). Om dit aan te tonen, maken we gebruik van een hulpstelling.

\mbox{Lemma 0: } (c_{n}x)^{m}(y) = x^{n*m}(y)
Bewijs door volledige inductie naar m:
  • Inductiehypothese IH: Zij m = 0; dan (c_{n}x)^{m}(y) = (c_{n}x)^{0}(y) = y = x^{0}(y) = x^{n * 0}(y) = x^{n * m}(y)
  • Stap: neem aan dat voor m \in \N geldt (c_{n}x)^{m}(y) = x^{n*m}(y).
  • \begin{matrix} & (c_{n}x)^{m+1}(y) \\
=_\beta & c_{n}x(c_{n}x)^{m}(y)) \\
=_\beta & \mbox{dankzij IH:} c_{n}x(x^{n*m}(y)) \\
=_\beta & x^{n}(x^{n*m}(y)) \\
=_\beta & \mbox{(Herhaald toepassen bovenstaande definitie:)} & x^{n + n*m}(y) \\
=_\beta; & x^{n*(m+1)}(y)
\end{matrix}

Hiermee kunnen we aantonen dat A_{*} inderdaad een term is die vermenigvuldiging van Churchnumeralen mogelijk maakt:

\begin{matrix} & A_{*} c_{n} c_{m} \\
=_\eta & (\lambda xyz.x(yz)) c_{n} c_{m} \\
=_\beta & \lambda z.c_{n} (c_{m} z) \\
=_\beta & \lambda zx. (c_{m} z)^{n} (x) \\
=_\beta & \mbox{dankzij lemma 0:} & \lambda zx. z^{m*n} (x) \\
=_\alpha & \lambda fx. f^{n*m} (x) \\
=_\eta & c_{n*m}
\end{matrix}

Ten slotte behandelen we nog A_{exp} =_{\eta} \lambda xy.yx het machtsverheffen met Churchnumeralen voor exponenten groter dan 0. Ook hiervoor gebruiken we een hulpstelling:

\mbox{Lemma 0: } (c_{n})^{m}(x) = c_{n^m}(x), \mbox{ als } m > 0
Bewijs door volledige inductie naar m:
  • Inductiehypothese IH: Zij m = 1; dan (c_{n})^{m}(x) = (c_{n})^{1}(x) = c_{n}((c_{n})^{0}(x)) = c_{n}(x) = c_{n^1}(x) = c_{n^m}(x)
  • Stap: neem aan dat voor m \in \N geldt (c_{n})^{m}(x) = c_{n^m}(x).
\begin{matrix} & (c_{n})^{m + 1}(x) \\
=_\beta & c_{n}((c_{n})^{m}(x)) \\
=_\beta & \mbox{dankzij IH:} & c_{n}(c_{n^m}(x)) \\
=_\beta & \lambda y. (c_{n^m}(x))(y) \\
=_\beta & \mbox{dankzij lemma 0:} & \lambda y. x^{n^m * n}(y)\\
=_\beta & c_{n^{m+1}} x
\end{matrix}

Nu kunnen we aantonen voor m > 0:

\begin{matrix} & A_{exp} c_{n} c_{m} \\
=_\eta & (\lambda xy.yx) c_{n} c_{m} \\
=_\beta & c_{m} c_{n} \\
=_\beta & \lambda x.(c_{n})^{m}(x) \\
=_\beta & \mbox{dankzij lemma 1:} & \lambda x. c_{n^m}(x)\\
=_\beta & \lambda xy. x^{n^m}(y) \\
=_\alpha & \lambda fx.f^{n^m}{x} \\
=_\eta & c_{n^m}
\end{matrix}

De termen A_{+}, A_{*} \mbox{ en } A_{exp} zijn bedacht door John B. Rosser.

Standaardcombinatoren en Barendregtse rekenkunde[bewerken]

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 left-functie; voor alle lambdatermen M en N geldt \mathfrak{K}MN =_\beta M
  • \mathfrak{K}_{*} =_\eta \lambda xy.y: de right-functie; 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. f M N

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. Een paar vertalingen met behulp van η-gelijkheid en de lezer zal meemaken dat zijn vertaling van voren af aan begint. De vertaling wordt dus een oneindig lange rij lambda's als directe vertaling toegepast wordt. 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[bewerken]

Leibniz en het Entscheidungsproblem[bewerken]

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[bewerken]

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 overeen komt met hetgeen berekenbaar is, hoewel dat niet bewijsbaar is. Vrijwel onmiddellijk na de introductie van de Machine begon er een trans-Atlantisch touwtrekken tussen 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.

Eigenschappen van de lambdacalculus[bewerken]

Tarski en Knaster[bewerken]

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 grote 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[bewerken]

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. Totdat Park en Landin erop wezen dat hun dekpuntcombinator een zeer onaangename eigenschap van de lamdacalculus aantoonde. Beschouw namelijk de functie

succ: \R \rightarrow \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[bewerken]

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[bewerken]