  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.
