Higher-order Cons-free Interpreters

TL;DR

This paper explores the construction of interpreters for cons-free term rewriting systems, aiming to advance understanding of complexity class separations through refined, higher-order interpreters.

Contribution

It introduces the design of higher-order cons-free interpreters capable of interpreting lower-order terms, with potential applications in complexity class separation proofs.

Findings

Interpreters constructed for type order k > 1

Potential for refined interpreters to aid in complexity separation

Connection established between interpreters and diagonalisation methods

Abstract

Constructor rewriting systems are said to be cons-free if any constructor term occurring in the rhs of a rule must be a subterm of the lhs of the rule. Roughly, such systems cannot build new data structures during their evaluation. In earlier work by several authors, (typed) cons-free systems have been used to characterise complexity classes such as polynomial or exponential time or space by varying the type orders, and the recursion forms allowed. This paper concerns the construction of interpreters for cons-free term rewriting. Due to their connection with proofs by diagonalisation, interpreters may be of use when studying separation results between complexity classes in implicit computational complexity theory. We are interested in interpreters of type order $k > 1$ that can interpret any term of strictly lower type order; while this gives us a well-known separation result E$^k$TIME $\subseteq$ E$^{k+1}$TIME, the hope is that more refined interpreters with syntactically limited constraints can be used to obtain a notion of faux diagonalisation and be used to attack open problems in complexity theory.