Lambdacalculus

Van Wikipedia

Principes

Complexiteitstheorie

Modellen

Algoritme

Turingmachine

Lambdacalculus

Theorieën

Berekenbaarheid

Complexiteitsgraad

NP-compleet

De lambdacalculus is een model van berekening dat in 1936 geïntroduceerd werd door Alonzo Church en Stephen Kleene in hun speurtocht naar de limieten van de berekenbaarheid. In de informatica vormt het de basis voor functionele programmeertalen.

We onderscheiden twee vormen van lambdacalculus: de getypeerde lambdacalculus en de (oudere) ongetypeerde lambdacalculus. In eerste instantie zullen we de ongetypeerde lambdacalculus en haar rol binnen de informatica beschrijven, daarna de moeilijkheden die binnen dit systeem bestaan en tenslotte de getypeerde varianten bespreken.

[bewerk] Ongetypeerde lambdacalculus

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 termherschrijfsysteem.

[bewerk] Principe van berekening in lambdacalculus

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 wel β-reductie en de gelijkheid van hierboven heet β-gelijkheid; we horen dus eigenlijk op te schrijven

T [E' / E] = β T'

maar we zullen de β weglaten als het duidelijk genoeg is dat het om β-gelijkheid gaat. Als een term door een of andere β-reductie overgaat in een andere term, noteren we dat als volgt:

$T \longrightarrow_\beta T'$

Bestaat de overgang van T naar T' uit nul of meer β-reducties, dan noteren we als volgt:

$T \longrightarrow_\beta^{*} T'$

Ook hier zullen we de β weglaten als voldoende duidelijk is dat het over β-reductie gaat.

Een dergelijke berekening eindigt als er geen stukken meer zijn die vervangen kunnen worden. Een doel 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 β-reductie beschouwen we eerst een simpele, rekenkundige term:

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

We kunnen dus ook opschrijven $(10 + 8 * 4) - (6 / 3) \longrightarrow_\beta^{*} 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_\beta (10 + 8 * 4) - 2 \\ \longrightarrow_\beta (10 + 32) - 2 \\ \longrightarrow_\beta 42 - 2 \\ \longrightarrow_\beta 40 \end{matrix}$

Een term kan dus soms op meerdere manieren reduceren; er leiden dan meerdere wegen naar Rome. Uiteraard is het in de lambdacalculus wel de kunst de situatie te vermijden dat één mogelijke berekening wel eindigt en de andere niet (alhoewel dit niet altijd lukt).

[bewerk] Termen

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:

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 in M een lambdaterm: $x \in V \and M \in \Lambda \Rightarrow \lambda x.M[x] \in \Lambda$

Bij dit laatste punt dient opgemerkt te worden dat x niet in M voor hoeft te komen; $λ 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 bewijstechniek van structuurinductie is gebaseerd op het bestaan van deze structuur.

Voorbeelden van lambdatermen:

v

v' w

λ f .λ y . f y

(λ w . f w) q

q (λ w . f w)

[bewerk] Abstractie

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 vernoemd). Zij M een in het algemeen van x afhankelijke uitdrukking. Dan is

λ x . M

de afbeelding

$x\mapsto M$ .

Bijvoorbeeld:

λ 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 al even inductief gedefinieerd als de calculus zelf. 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:

(λ 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:

λ x . M = α λ y . M [y / x]

Bijvoorbeeld:

$\lambda x.xyzx \longrightarrow_\alpha \lambda w.wyzw$ , dus

λ x . x y z x = α λ w . w y z w

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 meerdere 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 Brooks 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

λ x, y, z . x y z z y x

is niet verschillend van de term

λ x .λ y .λ z . x y z z y x

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

λ x .(λ y .(λ z .(x y z z y x)))

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

[bewerk] Applicatie

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

M N

Een applicatie van een abstractie op een andere term is een speciale situatie in de lambdacalculus. In dit geval ontstaat er namelijk een term (genaamd een redex) waarop een β-reductie toegepast kan worden. Om precies te zijn, 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 (ook bekend als het basisaxioma van de lambdacalculus):

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

Merk op dat het niet nodig is voorwaarden te stellen zoals "x ongelijk aan N" of "N komt niet voor in M": we hadden tenslotte afgesproken (in de Barendregt-afspraak) dat we dit niet zouden doen. Mocht het een keer voorkomen doordat we niet goed opgelet hebben, dan gelden de volgende regels om het op te lossen:

x = N : gebruik α-reductie om x aan te passen
N komt anderszins in M voor : in dit geval moet het om dezelfde, vrije variabele gaan

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 afgeleid zijn, zegt men ook wel dat functies "first class citizens" zijn - het zijn niet alleen toepasbare taalonderdelen, maar ook op zichzelf staande objecten waarmee gerekend kan worden). 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 $λ x . y$ meteen y mag opschrijven! Er moet echt een reductie plaatsvinden, met een argument.

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

Zoals we nog zullen zien, kunnen lamdatermen behoorlijk lang worden. Zeker de applicaties van termen op termen op termen op et cetera. In de lambdacalculus wordt daarom veel gebruik gemaakt van substitutie: het vervangen van een deelterm door een andere. Dit is handig om te gebruiken als afkorting.

Het substitueren van de ene term voor de andere wordt η-reductie genoemd. Twee termen die op η-reductie na hetzelfde zijn, zijn η-gelijk aan elkaar. η-Reductie mag echter alleen toegepast worden op vrije variabelen (de mogelijkheden van α-reductie en vervanging bij β-reductie van gebonden variabelen laat zich niet verenigen met η-reductie). We noteren als volgt:

$M[x] \longrightarrow_\eta M[x:=N] (als\ x \in FV(M))$

Bijvoorbeeld:

$\lambda x.x W \longrightarrow_\eta \lambda x. x (\lambda y. yzzcabttr)$

η-Reductie introduceert het concept van isomorfie in de lambdacalculus.

[bewerk] Lambdacalculus en algoritmen

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.

[bewerk] Enige axioma's

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

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$ :

$M = M$ : iedere term is gelijk aan zichzelf
$M = N \Rightarrow N = M$ : gelijkheid in de lambdacalculus is reflexief
$M = N \wedge N = L \Rightarrow M = L$ : gelijkheid in de lambdacalculus is transitief

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'$

[bewerk] Churchnumeralen

Churchnumeralen zijn een manier om in de lambdacalculus natuurlijke getallen te representeren. Met deze Churchnumeralen (bedacht door Alonzo Church) valt gemakkelijk de basisrekenkunde in de lambdacalculus te demonsteren.

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 = η λ f x . 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 + = η λ x y p q . x p (y p q)$

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 * = η λ x y z . x (y z)$ . Om dit aan te tonen, maken we gebruik van een hulpstelling.

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}$

Tenslotte behandelen we nog $A e x p = η λ x y . y x$ 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 * en A e x p$ zijn bedacht door John B. Rosser.

[bewerk] Standaardcombinatoren en Barendregtse rekenkunde

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

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

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

$\mathfrak{I} =_\eta \lambda x.x$ : de identiteitscombinator; voor iedere lambdaterm M geldt $\mathfrak{I}M =_\beta M$
$\mathfrak{K} =_\eta \lambda xy.x$ : de 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 ${T r u e, F a l s e}$ . 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:

λ 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 en . Deze term is ; 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 modeleren in de lambdacalculus. Niet alleen de basisbewerkingen, maar ook datastructuren als lijsten en de bijbehorende bewerkingen passen op natuurlijke wijze in dit schema. Wij hopen dat de lezer dit van ons aan zal nemen, of (nog beter) de moeite zal nemen de geciteerde bronnen erop na te slaan.

[bewerk] Lambdacalculus als model van berekening

[bewerk] 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 Wilhelm 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 (mensen als George Boole) bleven druk zoeken naar antwoorden op zijn vragen.

Rond 1877 publiceerde Georg Ferdinand 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.

[bewerk] 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 overeen komt met hetgeen berekenbaar is (hoewel dat niet bewijsbaar is). Vrijwel onmiddellijk na de introductie van de Machine begon er een transatlantisch touwtrekken tussen tussen Turing en Alonzo Church (bedenker van de lambdacalculus) om wiens mechanisme het meest algemeen was. De briefwisseling tussen de twee (feitelijk een intercontinentaal wedstrijdje verpissen) 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:

$(\lambda x. xx)(\lambda x. xx) \Rightarrow_\beta (\lambda x.xx)(\lambda x.xx)$
$(\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.

[bewerk] Eigenschappen van de lambdacalculus

[bewerk] 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 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.

[bewerk] De dekpuntcombinator

Gegeven is een functie $f:V \rightarrow V$ . Een dekpunt (Engels: fixed point) 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 = η λ x . F (x x)

X = η W W

Dan

X = η W W = η (λ x . F (x x)) W = β F (W W) = η F X

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

Definieer

Y = η λ f .(λ x . f (x x))(λ x . f (x x))

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$

s u c c (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 teveel 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.

[bewerk] 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.

[bewerk] De getypeerde lambdacalculus

[bewerk] Types binnen de lambdacalculus

[bewerk] De lambdakubus

[bewerk] Externe bronnen

Introduction to Lambda Calculus - Revised edition of October 1994
Henk Barendregt and Erik Barendsen
The theory of the foundation of mathematics : 1870 to 1940 - Ir. Mark Scheffer, maart 2002

Categorieën: Logica | Theoretische informatica

Lambdacalculus

Van Wikipedia

Inhoud

[bewerk] Ongetypeerde lambdacalculus

[bewerk] Principe van berekening in lambdacalculus

[bewerk] Termen

[bewerk] Abstractie

[bewerk] Applicatie

[bewerk] Lambdacalculus en algoritmen

[bewerk] Enige axioma's

[bewerk] Churchnumeralen

[bewerk] Standaardcombinatoren en Barendregtse rekenkunde

[bewerk] Lambdacalculus als model van berekening

[bewerk] Leibniz en het Entscheidungsproblem

[bewerk] Lambdacalculus en de Turingmachine

[bewerk] Eigenschappen van de lambdacalculus

[bewerk] Tarski en Knaster

[bewerk] De dekpuntcombinator

[bewerk] Het probleem

[bewerk] De getypeerde lambdacalculus

[bewerk] Types binnen de lambdacalculus

[bewerk] De lambdakubus

[bewerk] Externe bronnen

Views

Navigatie

Informatie

Zoeken

in andere talen