Infinite data structures can be studied with a simplified technique, thanks to research done by PhD student Jurriaan Rot. He received his PhD degree with honours (cum laude) for his thesis ‘Enhanced Coinduction’ at Leiden University on 15 October 2015. This thesis belongs to the 5% best dissertations in the field of computer science. Jurriaan is the first PhD student at the Leiden Institute of Advanced Computer Science (LIACS) to graduate with honours. For his research, Jurriaan was seconded at the Formal Methods Group of CWI. His promotors are Frank de Boer (CWI and UL) and Jan Rutten (CWI and RU), and his co-promotor is Marcello Bonsangue (UL).
Jurriaan Rot's research was funded by the NWO project CORE - Coinductive Calculi of Regular Expressions. This project is an example of a successful cooperation between the Formal Methods group of the Centrum Wiskunde & Informatica (CWI) in Amsterdam and the Foundations of Software Technology research group from LIACS.
More information: see the full news item on 'Defining and analyzing infinite objects' from Leiden University (in Dutch) below.
Source: Leiden University
Oneindige objecten definiëren en analyseren
Bron: Universiteit Leiden
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 lichtinstallatie van Numen. Bron: LIACS, Universiteit Leiden.
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 de digitale versie van het proefschrift: Enhanced coinduction
Persoonlijke pagina van promotor prof.dr. Frank de Boer
