1. Introduction
In [2], Jones introduced consfree programming; roughly readonly programs where data structures cannot be created or altered, only read from the input. For example, consfree programs with data order can compute exactly those decision problems which are in PTIME, while tailrecursive consfree programs with data order characterise PSPACE. The field of research studying such characterisations is called implicit computational complexity (ICC).
Jones’ results can easily be generalised to the area of (higherorder) term rewriting. In term rewriting, systems have no fixed evaluation order (so callbyname or callbyvalue can be introduced as needed, but are not required), and reduction is natively nondeterministic. ICC using consfree term rewriting has been studied by several authors [1, 3].
One important goal of ICC is to provide new separation results between wellknown classes. A standard technique for doing so is diagonalisation via interpreters. Roughly, an interpreter for a rewriting system is a term in another rewriting system that, when applied to (a bit string representation of) any term from , will simulate evaluation of that term. It is tantalising to consider interpreters for, and written in, consfree term rewriting. While interpreters are very wellknown in functional programming, they are very rarely seen in rewriting. Furthermore, typical programming of selfinterpreters in the wild involves maintaining several intermediate data structures, which is patently impossible in consfree rewriting where no data constructors are present.
Our work concerns the construction of consfree interpreters for higherorder term rewriting. As a proof of concept, we consider in this paper an interpreter of type order that will evaluate any, suitably encoded, term of type order . In future work, we hope that studying further constraints to the syntactic form of the rules of higherorder systems (effectively, constraining the types of recursion used) may lead to more refined diagonalisation and that such “faux” diagonalisation may lead to results separating known complexity classes.
2. Preliminaries
We consider higherorder term rewriting with simple types, and reduction as a separate step; we reason modulo conversion only. Function symbols are assigned a type declaration of the form , where does not need to be a base type. Rules are assumed to have the form (so can have a functional type). we additionally limit interest to higherorder constructor TRSs, which is to say that each in the rule above is a constructor term, and does not contain either applications or abstractions.
We will use “data terms” to refer to the set of ground constructor terms containing neither abstractions nor applications. We denote for the set of terms built from symbols in and variables in , and for the set of data terms. We will particularly consider an innermost weak reduction strategy, which disallows reductions below an abstraction, and allows a subterm to be reduced only if all are abstractions or normal forms.
Definition 1.
Let be a class of HOTRSs and be sets indexed by (shortly denoted and instead of and ) such that . A HOTRS with start symbol is an interpreter for with input set and output set , if there exist computable injective functions and such that, for all and :
if and only if
3. Consfree Term Rewriting
Like Jones [2], we limit interest to consfree rules, adapted to term rewriting as follows:
Definition 2 (Consfree Rules).
A rule , presented using conversion in a form where all binders are distinct from the free variables, is consfree if for all subterms of with a constructor, either is a subterm of or, if not, is a data term. A leftlinear (higherorder) constructor TRS is consfree if all rules in are.
Consfree term rewriting enjoys many convenient properties. Most importantly, the set of data terms that may be reduced to using consfree rules is limited by the data terms in the start term and the righthand sides of rules, as described by the following definition:
Definition 3.
For a given ground term , the set contains all data terms which occur as (a) a subterm of or (b) a subterm of the righthand side of some rule in .
is a set of data terms, is closed under subterms and, since is fixed, has a linear number of elements in the size of . The property that no new data is generated by reducing is formally expressed by the following result:
Definition 4 (safety).
Let be a set which (a) is closed under subterms, and (b) contains all data terms occurring in the righthand side of a rule in . A term is safe if for all subterms of : if with a constructor, then .
Lemma 5.
Let be consfree. For all : if is safe and , then is safe.
Thus, for a decision problem (where and all are data terms), all terms occurring in the reduction are safe. This insight allows us to limit interest to safe terms in most cases, and is instrumental to obtain the following results:
Proposition 1.
The class of decision problems in contains exactly those functions which can be accepted by:

a consfree HOTRS of order with a weakinnermost reduction strategy;

a consfree confluent HOTRS of order with a weakinnermost reduction strategy.
That is, adding determinism does not make a difference to the characterisation result. Hence for simplicity we will focus on confluent TRSs in particular.
4. Interpretations
We consider a system with the following constructors:
Bit strings can be used to encode numbers in the usual way, e.g. ; we assume a unique encoding for each bitstring, so without leading zeros. To encode a firstorder TRS , we enumerate the function symbols, writing , and in each rule we assume the variables are in for some . For the term encoding, let:
Here, the list constructor is denoted in an infix, rightassociative way. Writing , the TRS is encoded as the following term:
Of course, strictly speaking an intepreter should operate on bit strings only. We have chosen for this more verbose encoding because it is easier to understand the resulting interpretersystem, and the same ideas can be transferred to a more restrictive encoding.
We seek to define a confluent consfree HOTRS with a weakinnermost reduction strategy which, given a confluent, consfree firstorder TRS with innermost reduction, and a data term , obtains the encoding for , provided this is a data term. Formally, if is encoded as the term , we must have for any ground start term with a data term, and if is not a data term. This can be used to determine whether (but is more general).
Note that, since must be consfree, we cannot represent intermediate terms (e.g. the direct reduct of the start term). Instead, will operate on tuples (,), where is a “substitution”: a term of type mapping the representations of variables in to data terms or (which indicates any term in normal form that is not a data term).
To work! We will recurse over the set of rules, but carry along the complete set, as well as the arguments to the start term (which together define the set ), for later use.
Thus, we normalise just by substituting if is a variable or no rules match (so is in normal form either way); reduces to if is not a data term. The function is used to test whether a rule matches and find the relevant substitution in one go: in case of a match, reduces to for every which does not refer to a variable in , and in case of no match, it reduces to instead (which is not a representation of any term). In the case of a successful match, we continue to normalise .
To define , we note that is always a subterm of either the start term, or the righthand side of a rule, and is not a variable; the result of substituting is a normal form, so we must reduce to a data term—which, by Lemma 5, is a subterm of or of the righthand side of some rule—or to . These observations give the following rules:
Thus, to obtain , we find the subterm of the start term or the rules equal to it. The rules for the latter case—verifying that is a constructorterm and finding a subterm of the righthand side of a rule equal to , or reducing to if either part fails—have been omitted for space reasons.
The next task is to find whether instantiates some lefthand side , and obtain the relevant substitution if so. Here, “instantiates” should not be taken literally as is not necessarily a basic term. Rather, writing , we seek to confirm whether for some . Note that is necessarily leftlinear, and its strict subterms are constructor terms.
Thus, iterates over both and , updating for each such that . This uses the helper function, which assumes that is a data term or . If any of the instantiations fails (so if the rule does not match), is updated to have for all lists which do not correspond to a variable in .
5. Conclusions
Thus we have seen:
There is a secondorder consfree confluent HOTRS
which is an interpreter for the class of firstorder consfree confluent TRSs.
Assuming Proposition 1 holds, we could now use a diagonalisation argument to obtain a new proof for the hierarchy result . Generalising the program to higher orders, we should also be able to obtain that each .
While these are known results, the ideas used in this proof might transfer to more ambitious projects. For example, if we could give a tail recursive variation of the interpreter then, following Jones [2], we might obtain a proof of the proposition .
References
 [1] D. de Carvalho and J. Simonsen. An implicit characterization of the polynomialtime decidable sets by consfree rewriting. In G. Dowek, editor, RTATLCA ’14, volume 8560 of LNCS, pages 179–193, 2014.
 [2] N. Jones. Life without cons. JFP, 11(1):5–94, 2001.
 [3] C. Kop and J. Simonsen. Complexity hierarchies and higherorder consfree rewriting. In D. Kesner and B. Pientka, editors, FSCD ’16, volume 52 of LIPIcs, pages 23:1–23:18, 2016.
Comments
There are no comments yet.