Oneindige objecten definiëren en analyseren
Oneindige datastructuren kunnen worden bestudeerd met een vereenvoudigde techniek, dankzij onderzoek van Jurriaan Rot, waarop hij op 15 oktober 2015 cum laude promoveerde met zijn proefschrift Enhanced Coinduction.
Het proefschrift van Jurriaan Rot behoort tot de 5% beste proefschriften op het gebied van informatica. Jurriaan is de eerste PhD student van het Leiden Institute of Advanced Computer Science die cum laude is gepromoveerd.
Systemen als black-box
Het onderzoek van Jurriaan Rot werd gefinancierd door het NWO-project CORE – Coinductive Calculi of Regular Expressions. Dit project is een voorbeeld van succesvolle samenwerking tussen de groep van Formal Methods van het Centrum Wiskunde & Informatica in Amsterdam en de groep van Foundations of Software Technology van het Leiden Institute of Advanced Computer Science.
Onder leiding van Dr. Bonsangue en Prof.dr. Rutten, en in samenwerking met Prof.dr. Boer, werd in dit project de wiskundige theorie van coalgebras gebruikt als unificerend raamwerk voor het beschrijven en analyseren van dynamische systemen in brede zin. Voorbeelden zijn oneindige data-structuren (bijvoorbeeld oneindige rijen en bomen), formele automaten (zoals transitiesystemen en probabilistische automaten), computersystemen en software.
Artist impression van een oneindige data-structuur. Foto van een licht installatie van Numen.
Het abstract formalisme van coalgebra is heel geschikt voor het ontwerpen en analyseren van het uitwendig waarneembare gedrag van een systeem, dat zelf als een zogeheten `black box’ kan worden beschouwd: we kunnen niet binnen in het systeem kijken maar kunnen slechts van buitenaf observeren hoe het zich gedraagt.
Vereenvoudigen bestande technieken
In zijn proefschrift beschrijft Rot nieuwe technieken die coinductief redeneren vereenvoudigen en verbeteren. Coinductie, tegenhanger van (wiskundige) inductie, is een fundamenteel principe in de theorie van coalgebras voor het definiëren van oneindige objecten en het bewijzen van eigenschappen van zulke objecten. De kern van coinductie is dat een bewijs wordt gevonden dat verschillende toestanden van een system hetzelfde observeerbaar gedrag vertonen, en daarmee als gelijk kunnen worden beschouwd.
In de informatica bijvoorbeeld, kunnen bepaalde vormen van equivalentie tussen systemen met oneindig of circulair gedrag, zoals bisimulatie, coinductief gegeneraliseerd worden tot een concrete en krachtige bewijsmethode.
Dankzij de nieuwe technieken die Rot in zijn proefschrift beschrijft, kunnen coinductieve methoden beter, efficiënter en succesvoller toegepast worden op een verscheidenheid aan wetenschapsgebieden, zoals informatica en wiskunde. Dit is in het bijzonder het geval in de theorie van formele automaten, de theorie van concurrency, de studie van oneindige datastructuren, software engineering, systeemtheorie, logica, functioneel programmeren, typetheorie, semantiek, security; daarbuiten ook in gebieden als economie en ecologie.
In november vertrekt Jurriaan Rot naar de Écoles Normales Supérieure in Lyon, Frankrijk, waar hij als postdoc zijn onderzoek naar coalgebra en coinductie zal voortzetten.
Zie ook
Digitale versie van het proefschrift: Enhanced coinduction