Document

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

## File

LIPIcs.IPEC.2016.25.pdf
• Filesize: 0.63 MB
• 12 pages

## Cite As

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)
https://doi.org/10.4230/LIPIcs.IPEC.2016.25

## Abstract

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.
##### Keywords
• Linear Term Rewriting Systems
• Ground Reachability
• Ground Joinability
• Fixed Parameter Tractability

## Metrics

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

## References

1. Franz Baader and Tobias Nipkow. Term rewriting and all that. Cambridge university press, 1999.
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.
3. Andrew Beveridge, Alan Frieze, and Colin McDiarmid. Random minimum length spanning trees in regular graphs. Combinatorica, 18(3):311-333, 1998.
4. Marc Bezem, Jan Willem Klop, and Roel de Vrijer. Terese. term rewriting systems. Cambridge Tracts in Theoretical Computer Science, 55, 2003.
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: http://www.grappa.univ-lille3.fr/tata, 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.
7. N. Dershowitz and J. P. Jouannaud. Rewrite systems. Handbook of Theoretical Computer Science (Chapter 6), pages 243-320, 1990.
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.
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.
10. Ferenc Gécseg and Magnus Steinby. Tree languages. In Handbook of formal languages, pages 1-68. Springer, 1997.
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.
12. Rémy Gilleron and Sophie Tison. Regular tree languages and rewrite systems. Fundamenta informaticae, 24(1, 2):157-175, 1995.
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.
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.
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.
16. Jan Willem Klop, Marc Bezem, and RC De Vrijer. Term rewriting systems. Cambridge University Press, 2001.
17. Martin Korp and Aart Middeldorp. Match-bounds revisited. Information and Computation, 207(11):1259-1283, 2009.
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.
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.
20. Rakesh M Verma, Michael Rusinowitch, and Denis Lugiez. Algorithms and reductions for rewriting problems. Fundamenta Informaticae, 46(3):257-276, 2001.
X

Feedback for Dagstuhl Publishing