Implicit Complexity through Higher Order Rewriting (ICHOR)

From September 2019 to September 2023 I will lead the NWO TOP project Implicit Complexity through Higher Order Rewriting.

Scientific summary

ICHOR will study computational complexity of and using higher-order term rewriting systems. This builds on recent advances from several international research groups which use forms of rewriting to analyse complexity, and on the principal investigator's earlier work exploring the consequences of non-determinism within a higher-order setting.

Term rewriting is a formal system which can be used to specify algorithms. Its simple, rigorous definition makes it very suitable for formal analysis, and as a result, its properties are well studied. Higher-order term rewriting extends standard term rewriting with anonymous functions and binders as in the λ-calculus, thus providing a highly liberal class of systems.

Computational complexity is the study of resources (typically time and space) required to algorithmically solve a problem. Rather than analysing programs directly, the area of implicit complexity seeks to encode queries into calculi or logics – or indeed, term rewriting. Thus, methods from widely different areas can be brought to bear on the questions of complexity.

The aims of ICHOR are twofold. First, to devise theory to analyse complexity bounds of given higher-order term rewriting systems. Second, to analyse computational complexity classes using higher-order term rewriting, towards a characterisation of a broad hierarchy of both deterministic and non-deterministic complexity classes.

The first phase of the project will explore a methodology to obtain runtime bounds of (unrestricted) higher-order term rewriting. The second phase will seek to devise a characterisation of a hierarchy of complexity classes for time and space using higher-order cons-free term rewriting.

Abstract for laymen (Dutch)

Dit project combineert twee gebieden van de theoretische informatica: berekeningscomplexiteitstheorie en hogere-orde termherschrijven. Dit is zuiver onderzoek, gericht op verruiming van onze kennis, niet op praktische toepassingen.

Berekeningscomplexiteitstheorie gaat (min of meer) over de moeilijkheid van problemen die een computer kan oplossen. Zulke problemen worden gecategoriseerd in klassen gebaseerd op de tijd, geheugen of andere kosten die nodig zijn om een oplossing te vinden. Bijvoorbeeld:

Één van de bekendste open problemen in de informatica is het P/NP probleem: de vraag of de problemen die in de klasse NP zitten ook in P zitten. Waarschijnlijk is dat niet zo, maar het is nooit bewezen. Het Clay Mathematics Institute heeft zelfs een miljoen dollar uitgeloofd voor een bewijs. Buiten dit bekende probleem zijn er nog heel veel andere open vragen over de relaties tussen complexiteitsklassen.

Termherschrijfsystemen zijn een soort van programma's die hele simpele, formele regels volgen. Dit maakt het relatief makkelijk om er wiskundig over te redeneren. Er zijn verschillende variaties van termherschrijfsystemen, waaronder hogere orde. Zulke termherschrijfsystemen lijken op programma's in functionele programmeertalen zoals Haskell.

In dit project gebruiken we hogere-orde-termherschrijfsystemen om complexiteitsklassen te analyseren. Dit kan door stellingen zoals: "een beslissingsprobleem is in P precies dan als er een termherschrijfsysteem bestaat dat dit probleem oplost, en aan zekere eisen voldoet". Het mooie van zo'n beschrijving is dat we over complexiteitsklassen kunnen praten zonder direct naar tijd of geheugen te kijken, maar slechts naar eenvoudig controleerbare eigenschappen van termherschrijfsystemen.

Dit is niet een volledig nieuw idee: de methode valt onder de impliciete complexiteit. Dit vakgebied beschrijft complexiteitsklassen op alternatieve manieren, zoals vormen van logica of programmeertalen. Vaak gaat dit echter slechts over ééen klasse (bijvoorbeeld NP), en niet over een groep. Ook zijn veel methodes beperkt tot de deterministische complexiteitsklassen zoals P en EXPSPACE: klassen van beslissingsproblemen die in een bepaalde tijd of geheugen opgelost kunnen worden, en niet klassen zoals NP waarbij een oplossing "geraden" moet worden, die dan onder bepaalde beperkingen gecontroleerd kan worden.

Het doel van ICHOR is om een grote verzameling complexiteitsklassen te beschrijven door middel van termherschrijfsystemen met verschillende beperkingen – zowel deterministische als non-deterministische klassen. Een dergelijke beschrijving kan nieuwe inzichten geven in de relaties tussen de verschillende klassen – en ook in eigenschappen van termherschrijfsystemen. Om dit voor elkaar te krijgen gaan de onderzoekers hogere-orde-termherschrijfsystemen gebruiken, wat vooralsnog vrijwel niet gedaan is maar heel veel potentie heeft vanwege de vorm en mogelijkheden van herschrijven en hogere orde.