Mateus de Oliveira Oliveira: Ground Reachability and Joinability in Linear Term Rewriting Systems are Fixed Parameter Tractable with Respect to Depth

Abstract:
The ground term reachability problem consists in determining whether a given variable-free term \(t_1\) can be transformed into a given variable-free term \(t_2\) by the application of rules from a term rewriting system \(R\).  The joinability problem, on the other hand, consists in determining whether there exists a variable-free term \(t\) which is reachable both from \(t_1\) and from \(t_2\). Both problems have proven to be of fundamental importance for several subfields of computer science. Nevertheless, these problems are undecidable even when restricted to linear term rewriting systems.
In this work, we approach reachability and joinability in linear term rewriting systems from the perspective of parameterized complexity theory, and show that these problems are fixed parameter tractable with respect to the depth of derivations. More precisely, we consider a notion of parallel rewriting, in which an unbounded number of rules can be applied simultaneously to a term as long as these rules do not interfere with each other. A term \(t_1\) can reach a term \(t_2\) in depth \(d\) if \(t_2\) can be obtained from \(t_1\) by the application of \(d\) parallel rewriting steps.
Our main result states that for some function \(f(R,d)\), and for any linear term rewriting system $R$, one can determine in time \(f(R,d)\cdot |t_1|\cdot |t_2|\) whether a ground term \(t_2\) can be reached from a ground term \(t_1\) in depth at most \(d\) by the application of rules from \(R\). Additionally, one can determine in time \(f(R,d)^2 \cdot|t_1|\cdot|t_2|\) whether there exists a ground term \(t\), such that \(t\) can be reached from both \(t_1\) and \(t_2\) in depth at most \(d\). Our algorithms improve exponentially on exhaustive search (which terminates in time \(2^{|t_1|\cdot 2^{O(d)}} \cdot |t_2|\) and can be applied with regard to any linear term rewriting system, irrespective of whether the rewriting system in question is terminating or confluent.