Small Term Reachability and Related Problems for Terminating Term Rewriting Systems

TL;DR

The paper investigates the small term reachability problem for terminating and non-terminating term rewriting systems (TRSs), examining how the termination proof method affects computational complexity. By analyzing length-reducing TRSs, termination via polynomial orders, and termination via Knuth–Bendix orders, it derives precise complexity classifications: NP-complete for length-reducing systems (polynomial-time with confluence), $\mathrm{N2ExpTime}$-complete (and $\mathrm{NExpTime}$-complete under linear orders) for polynomial orders, and $\mathrm{PSpace}$-complete for KBO without a special symbol; confluence only reduces complexity in the length-reducing case. The paper also studies a large-term reachability variant and discusses how number encoding (unary vs binary) and the chosen termination method influence upper and lower bounds. These results illuminate the interplay between derivational complexity and reachability in TRSs and have implications for proof-rewriting and automated reasoning where small proofs are desired.

Abstract

Motivated by an application where we try to make proofs for Description Logic inferences smaller by rewriting, we consider the following decision problem, which we call the small term reachability problem: given a term rewriting system $R$, a term $s$, and a natural number $n$, decide whether there is a term $t$ of size $\leq n$ reachable from $s$ using the rules of $R$. We investigate the complexity of this problem depending on how termination of $R$ can be established. We show that the problem is in general NP-complete for length-reducing term rewriting systems. Its complexity increases to N2ExpTime-complete (NExpTime-complete) if termination is proved using a (linear) polynomial order and to PSpace-complete for systems whose termination can be shown using a restricted class of Knuth-Bendix orders. Confluence reduces the complexity to P for the length-reducing case, but has no effect on the worst-case complexity in the other two cases. Finally, we consider the large term reachability problem, a variant of the problem where we are interested in reachability of a term of size $\geq n$. It turns out that this seemingly innocuous modification in some cases changes the complexity of the problem, which may also become dependent on whether the number $n$ is is represented in unary or binary encoding, whereas this makes no difference for the complexity of the small term reachability problem.

Figures (2)

• Figure 1: Three proof rules for $\mathcal{EL}$.
• Figure 2: Proof of the conclusion of $\mathsf{R3}$ from its hypotheses using $\mathsf{R1}$ and $\mathsf{R2}$.

Theorems & Definitions (55)

• Example 2.1
• Example 2.2
• Definition 2.3
• Example 2.4
• Definition 3.1
• Proposition 3.2
• proof
• Lemma 4.1
• proof
• Proposition 4.2