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; consequently, its properties are well studied. Higher-order term rewriting extends standard term rewriting with anonymous functions and binders as in the lambda-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 attack two related lines of research ripe for success: to devise a characterisation of a hierarchy of complexity classes for time and space using higher-order cons-free rewriting.
