Belangrijke stap gezet in het oplossen van Milners probleem over reguliere expressies

Clemens Grabmayer, postdoctoraal onderzoeker bij GSSI in L'Aquila, Italië, en Wan Fokkink, hoogleraar theoretische informatica aan de Vrije Universiteit Amsterdam, hebben een belangrijke stap gezet in de richting van de oplossing van een probleem van Robin Milner. Deze Turing Award-winnaar presenteerde zijn vraagstelling in 1984 en deze is sindsdien onopgelost gebleven. Grabmayer en Fokkink presenteren hun resultaat in juli op het ACM/IEEE Symposium on Logic in Computer Science, dat online zal plaatsvinden.

12-05-2020 | 9:18

Het probleem van Milner betreft reguliere expressies, die fundamenteel zijn voor formele talen theorie en belangrijk voor patroonvergelijking (zoals het grep-commando in Linux). Milner ontwikkelde een equationeel systeem dat het mogelijk maakt reguliere expressies te gebruiken om de correctheid van computerprogramma's te bewijzen.

Milners open vraag, die wereldwijd door onderzoekers is bestudeerd, is of dit systeem alle reguliere expressies gelijkstelt die aanleiding geven tot equivalent programmagedrag.

Grabmayer en Fokkink bewijzen dit resultaat voor een grote klasse van reguliere expressies en leggen uit hoe de nieuwe technieken die ze ontwikkelen de weg kunnen openen naar een positief antwoord op Milners vraag voor alle reguliere expressies.