ICHOR zal de computationele complexiteit van en met behulp van hogere-orde begripsherschrijfsystemen bestuderen. Dit bouwt voort op recente vooruitgang van verschillende internationale onderzoeksgroepen die vormen van herschrijving gebruiken om complexiteit te analyseren, en op het eerdere werk van de hoofdonderzoeker waarin de gevolgen van non-determinisme in een hogere-orde situatie worden onderzocht.
Begripsherschrijving is een formeel systeem dat kan worden gebruikt om algoritmen te specificeren. Zijn eenvoudige, rigoureuze definitie maakt het zeer geschikt voor formele analyse; bijgevolg zijn zijn eigenschappen goed bestudeerd. hogere-orde begripsherschrijfsystemen breidt standaard begripsherschrijven uit met anonieme functies en binders zoals in de lambda-calculus, en biedt zo een zeer liberale klasse van systemen.
Computationele complexiteit is de studie van de middelen (meestal tijd en ruimte) die nodig zijn om een probleem algoritmisch op te lossen. In plaats van programma's rechtstreeks te analyseren, tracht het gebied van de impliciete complexiteit vragen te coderen in rekenmodellen - of zelfs termherschrijving. Aldus kunnen methoden uit zeer verschillende gebieden worden toegepast op complexiteitsvraagstukken.
De doelstellingen van ICHOR zijn tweeledig. Ten eerste het ontwikkelen van theorie om complexiteitsgrenzen van gegeven hogere-orde term herschrijfsystemen te analyseren. Ten tweede het analyseren van computationele complexiteitsklassen met behulp van hogere-orde term herschrijving, in de richting van een karakterisering van een brede hiërarchie van zowel deterministische als niet-deterministische complexiteitsklassen.
De eerste fase van het project zal een methodologie onderzoeken om runtime bounds te verkrijgen van (onbeperkte) hogere-orde begripsherschrijving. In de tweede fase zullen twee verwante lijnen van onderzoek 1 rijp voor succes: het ontwerpen van een karakterisering van een hiërarchie van complexiteitsklassen voor tijd en ruimte met behulp van hogere-orde begripsherschrijving.
