Veertig jaar geleden verdedigde ik mijn proefschrift, over de lambda calculus, een gestyleerde programmeertaal. Deze taal wordt tegenwoordig ook gebruikt voor het verifiëren van bewijzen, met als toepassing het certificeren van hardware en software. In mijn proefschrift bewees ik dat het mogelijk is om alle zogenaamd onoplosbare termen gelijk te stellen, zonder dat alles gelijk wordt. Dat werd een nieuwe lambda-theorie.
In de jaren daarna bewees ik een stelling die voor vrijwel alle lambda-theorieën geldt: Een lambda-term beeldt alle termen af hetzij op een enkele term, hetzij op oneindig vele. In 1984 verscheen mijn eerste boek: The Lambda Calculus, its Syntax and Semantics. Slechts voor één theorie in het boek – nota bene mijn eigen theorie die de onoplosbare termen identificeerde – kon ik de stelling niet bewijzen. In het boek vermeldde ik de uitspraak als vermoeden, en gaf ik hints voor een bewijs. Een aantal uitstekende onderzoekers – onder andere uit Italië en Amerika – hebben eraan gewerkt, echter zonder een bewijs te vinden.
De lambda calculus werd uitgevonden door de Amerikaanse logicus Alonzo Church (1903-1995). Het begrip functie speelt een centrale rol in deze theorie. In de jaren dertig van de vorige eeuw was er nog geen duidelijke inzicht in wat het begrip ‘berekenbaarheid’ precies inhoudt. Church stelde voor dat berekenbaarheid ‘gevangen’ kan worden door de door hem geïntroduceerde lambda calculus.
De Engelse logicus Alan Turing (1912-1954) kwam enige tijd later met een ander voorstel voor berekenbaarheid, gebaseerd op machines, dat uiteindelijk op hetzelfde neer bleek te komen. Church en Turing waren beiden in staat een precies gesteld probleem te formuleren, dat geen berekenbare oplossing heeft. Dat is een zogenaamd onoplosbaar probleem. Die problemen waren gesteld in hun eigen formalisme (functies, respectievelijk machines).
Later kon men ook van vele wiskundige problemen aantonen dat ze onoplosbaar zijn. Zo liet de Russische wiskundige Yuri Matijasevic in 1970 zien dat voor een willekeurige Diophantische vergelijking (bijvoorbeeld x3 + y3 – z3 = 0) niet door berekening bepaald kan worden of er een oplossing is in de gehele getallen. Voor genoemde vergelijking is er overigens geen oplossing; dat werd bewezen door Euler in 1770 als bijzonder geval van de laatste stelling van Fermat.
Naast Church is Haskell Curry (1900-1982) een belangrijke naam binnen de lambda calculus. Curry heeft de zogeheten types voor de lambda calculus geïntroduceerd. Beide logici heb ik nog gekend: toen ik twintig was, waren zij in de zestig. Nu ben ik in de zestig en heb ik foto’s van deze twee heren toen zij als student rond de twintig waren, geplaatst in mijn tweede boek. Dat boek Lambda calculus with types, geschreven met Wil Dekkers en Richard Statman, zal volgend jaar bij Cambridge University Press verschijnen.
Ik trad in de voetsporen van Church en Curry, en – zoals dat gaat in de wetenschap – is er nu weer een nieuwe generatie van jonge wiskundigen die mij navolgt. Onlangs zat ik in de promotiecommissie van Andrew Polonsky, een jongeman uit de Oekraïne, die promoveerde aan de universiteit van de Noorse stad Bergen. Hij heeft op een schitterende manier het bovengenoemde probleem opgelost dat ik ruim dertig jaar geleden formuleerde.
Polonsky heeft heel goed naar de voorbeelden uit mijn boek uit 1984 gekeken, die ik aangaf in een poging om het vermoeden te bewijzen. Die heeft hij op verbluffende wijze gecombineerd met eigen ideeën. Hij vond een term die de lambda-termen op precies twee termen afbeeldt, hetgeen mijn vermoeden weerlegt. Het is prachtig dat dit puzzelstuk nu eindelijk is gelegd.
Lees hier een achtergrondartikel van Henk Barendregt: (pdf).