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

Author Mateus de Oliveira Oliveira

Thumbnail PDF


  • Filesize: 0.63 MB
  • 12 pages

Document Identifiers

Author Details

Mateus de Oliveira Oliveira

Cite AsGet BibTex

Mateus de Oliveira Oliveira. Ground Reachability and Joinability in Linear Term Rewriting Systems are Fixed Parameter Tractable with Respect to Depth. In 11th International Symposium on Parameterized and Exact Computation (IPEC 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 63, pp. 25:1-25:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


The ground term reachability problem consists in determining whether a given variable-free term t can be transformed into a given variable-free term t' 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 and from t'. 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)*|t_1|*|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*|t_1|*|t_2| whether there exists a ground term u, such that u 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|*2^{O(d)}}*|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.
  • Linear Term Rewriting Systems
  • Ground Reachability
  • Ground Joinability
  • Fixed Parameter Tractability


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Franz Baader and Tobias Nipkow. Term rewriting and all that. Cambridge university press, 1999. Google Scholar
  2. Leo Bachmair. Rewrite techniques in theorem proving. In Proc. of the 5th International Conference on Rewriting Techniques and Applications, LNCS, pages 1-1, 1993. Google Scholar
  3. Andrew Beveridge, Alan Frieze, and Colin McDiarmid. Random minimum length spanning trees in regular graphs. Combinatorica, 18(3):311-333, 1998. Google Scholar
  4. Marc Bezem, Jan Willem Klop, and Roel de Vrijer. Terese. term rewriting systems. Cambridge Tracts in Theoretical Computer Science, 55, 2003. Google Scholar
  5. H. Comon, M. Dauchet, R. Gilleron, C. Löding, F. Jacquemard, D. Lugiez, S. Tison, and M. Tommasi. Tree automata techniques and applications. Available on:, 2007. release October, 12th 2007.
  6. Colin Cooper and Alan Frieze. Component structure of the vacant set induced by a random walk on a random graph. Random Structures &Algorithms, 42(2):135-158, 2013. Google Scholar
  7. N. Dershowitz and J. P. Jouannaud. Rewrite systems. Handbook of Theoretical Computer Science (Chapter 6), pages 243-320, 1990. Google Scholar
  8. Bertram Felgenhauer and René Thiemann. Reachability analysis with state-compatible automata. In Proc. of the 8th International Conference on Language and Automata Theory and Applications, LNCS, pages 347-359. Springer, 2014. Google Scholar
  9. Guillaume Feuillade, Thomas Genet, and Valérie Viet Triem Tong. Reachability analysis over term rewriting systems. Journal of Automated Reasoning, 33(3-4):341-383, 2004. Google Scholar
  10. Ferenc Gécseg and Magnus Steinby. Tree languages. In Handbook of formal languages, pages 1-68. Springer, 1997. Google Scholar
  11. Thomas Genet. Decidable approximations of sets of descendants and sets of normal forms. In Proc. of the 9th International Conference on Rewriting Techniques and Applications, LNCS, pages 151-165, 1998. Google Scholar
  12. Rémy Gilleron and Sophie Tison. Regular tree languages and rewrite systems. Fundamenta informaticae, 24(1, 2):157-175, 1995. Google Scholar
  13. Guillem Godoy, Robert Nieuwenhuis, and Ashish Tiwari. Classes of term rewrite systems with polynomial confluence problems. ACM Transactions on Computational Logic (TOCL), 5(2):321-331, 2004. Google Scholar
  14. Guillem Godoy, Ashish Tiwari, and Rakesh Verma. Characterizing confluence by rewrite closure and right ground term rewrite systems. Applicable Algebra in Engineering, Communication and Computing, 15(1):13-36, 2004. Google Scholar
  15. Lukasz Kaiser. Confluence of right ground term rewriting systems is decidable. In Foundations of Software Science and Computational Structures, pages 470-489. Springer, 2005. Google Scholar
  16. Jan Willem Klop, Marc Bezem, and RC De Vrijer. Term rewriting systems. Cambridge University Press, 2001. Google Scholar
  17. Martin Korp and Aart Middeldorp. Match-bounds revisited. Information and Computation, 207(11):1259-1283, 2009. Google Scholar
  18. Takashi Nagaya and Yoshihito Toyama. Decidability for left-linear growing term rewriting systems. In Proc. of the 10th International Conference on Rewriting Techniques and Applications, LNCS, pages 256-270, 1999. Google Scholar
  19. Vincent van Oostrom. Normalisation in weakly orthogonal rewriting. In Proc. of the 10th International Conference on Rewriting Techniques and Applications, LNCS, pages 60-74, 1999. Google Scholar
  20. Rakesh M Verma, Michael Rusinowitch, and Denis Lugiez. Algorithms and reductions for rewriting problems. Fundamenta Informaticae, 46(3):257-276, 2001. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail