Document Open Access Logo

Confluence of Layered Rewrite Systems

Authors Jiaxiang Liu, Jean-Pierre Jouannaud, Mizuhito Ogawa

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2015.423.pdf
  • Filesize: 0.53 MB
  • 18 pages

Document Identifiers

Subject Classification

Keywords
  • Layers
  • confluence
  • decreasing diagrams
  • critical pairs
  • cyclic unification

Metrics

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

Abstract

We investigate a new, Turing-complete class of layered systems, whose linearized lefthand sides of rules can only be overlapped at the root position. Layered systems define a natural notion of rank for terms: the maximal number of redexes along a path from the root to a leaf. Overlappings are allowed in finite or infinite trees. Rules may be non-terminating, non-left-linear, or non-right- linear. Using a novel unification technique, cyclic unification, we show that rank non-increasing layered systems are confluent provided their cyclic critical pairs have cyclic-joinable decreasing diagrams.

Cite As Get BibTex

Jiaxiang Liu, Jean-Pierre Jouannaud, and Mizuhito Ogawa. Confluence of Layered Rewrite Systems. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 423-440, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.CSL.2015.423

Author Details

Jiaxiang Liu
Jean-Pierre Jouannaud
Mizuhito Ogawa

References

  1. Takahito Aoto, Yoshihito Toyama, and Kazumasa Uchida. Proving confluence of term rewriting systems via persistency and decreasing diagrams. In Dowek [7], pages 46-60. Google Scholar
  2. Hendrik P. Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland, 1984. Google Scholar
  3. Alain Colmerauer. Equations and inequations on finite and infinite trees. In FGCS, pages 85-99, 1984. Google Scholar
  4. Hubert Comon, Max Dauchet, Remi Gilleron, Christof Löding, Florent Jacquemard, Denis Lugiez, Sophie Tison, and Marc Tommasi. Tree automata techniques and applications. Available on: http://www.grappa.univ-lille3.fr/tata, 2007. release October, 12th 2007.
  5. Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite systems. In Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics (B), pages 243-320. North-Holland, 1990. Google Scholar
  6. Nachum Dershowitz, Mitsuhiro Okada, and G. Sivakumar. Confluence of conditional rewrite systems. In Stéphane Kaplan and Jean-Pierre Jouannaud, editors, Conditional Term Rewriting Systems, 1st International Workshop, Orsay, France, July 8-10, 1987, Proceedings, volume 308 of Lecture Notes in Computer Science, pages 31-44. Springer, 1987. Google Scholar
  7. Gilles Dowek, editor. Rewriting and Typed Lambda Calculi - Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, volume 8560 of Lecture Notes in Computer Science. Springer, 2014. Google Scholar
  8. Bertram Felgenhauer. Rule labeling for confluence of left-linear term rewrite systems. In IWC, pages 23-27, 2013. Google Scholar
  9. Jean H. Gallier, Stan Raatz, and Wayne Snyder. Theorem proving using rigid E-unification equational matings. In Proceedings of the Symposium on Logic in Computer Science (LICS'87), Ithaca, New York, USA, June 22-25, 1987, pages 338-346. IEEE Computer Society, 1987. Google Scholar
  10. Hiroshi Gomi, Michio Oyamaguchi, and Yoshikatsu Ohta. On the Church-Rosser property of root-E-overlapping and strongly depth-preserving term rewriting systems. IPSJ, 39(4):992-1005, 1998. Google Scholar
  11. Nao Hirokawa and Aart Middeldorp. Decreasing diagrams and relative termination. J. Autom. Reasoning, 47(4):481-501, 2011. Google Scholar
  12. Gérard P. Huet. Confluent reductions: Abstract properties and applications to term rewriting systems. J. ACM, 27(4):797-821, 1980. Google Scholar
  13. Jean-Pierre Jouannaud and Claude Kirchner. Solving equations in abstract algebras: A rule-based survey of unification. In Computational Logic - Essays in Honor of Alan Robinson, pages 257-321, 1991. Google Scholar
  14. Jean-Pierre Jouannaud and Vincent van Oostrom. Diagrammatic confluence and completion. In Susanne Albers, Alberto Marchetti-Spaccamela, Yossi Matias, Sotiris E. Nikoletseas, and Wolfgang Thomas, editors, Automata, Languages and Programming, 36th International Colloquium, ICALP 2009, Rhodes, Greece, July 5-12, 2009, Proceedings, Part II, volume 5556 of Lecture Notes in Computer Science, pages 212-222. Springer, 2009. Google Scholar
  15. Dominik Klein and Nao Hirokawa. Confluence of non-left-linear TRSs via relative termination. In Nikolaj Bjørner and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning - 18th International Conference, LPAR-18, Mérida, Venezuela, March 11-15, 2012. Proceedings, volume 7180 of Lecture Notes in Computer Science, pages 258-273. Springer, 2012. Google Scholar
  16. Jan Willem Klop. Term rewriting systems. In Handbook of Logic in Computer Science, Vol.2, pages 1-116. Oxford University Press, 1993. Google Scholar
  17. Jiaxiang Liu, Nachum Dershowitz, and Jean-Pierre Jouannaud. Confluence by critical pair analysis. In Dowek [7], pages 287-302. Google Scholar
  18. Jiaxiang Liu and Jean-Pierre Jouannaud. Confluence: The unifying, expressive power of locality. In Shusaku Iida, José Meseguer, and Kazuhiro Ogata, editors, Specification, Algebra, and Software - Essays Dedicated to Kokichi Futatsugi, volume 8373 of Lecture Notes in Computer Science, pages 337-358. Springer, 2014. Google Scholar
  19. Ken Mano and Mizuhito Ogawa. Unique normal form property of compatible term rewriting systems: a new proof of Chew’s theorem. Theor. Comput. Sci., 258(1-2):169-208, 2001. Google Scholar
  20. Kunihiro Matsuura, Michio Oyamaguchi, Yoshikatsu Ohta, and Mizuhito Ogawa. On the E-overlapping property of nonlinear term rewriting systems (in Japanese). IEICE, 80-D-I(11):847-855, 1997. Google Scholar
  21. Greg Nelson and Derek C. Oppen. Fast decision procedures based on congruence closure. J. ACM, 27(2):356-364, 1980. Google Scholar
  22. Satoshi Okui. Simultaneous critical pairs and Church-Rosser property. In Tobias Nipkow, editor, Rewriting Techniques and Applications, 9th International Conference, RTA-98, Tsukuba, Japan, March 30 - April 1, 1998, Proceedings, volume 1379 of Lecture Notes in Computer Science, pages 2-16. Springer, 1998. Google Scholar
  23. Barry K. Rosen. Tree-manipulating systems and Church-Rosser theorems. J. ACM, 20(1):160-187, 1973. Google Scholar
  24. Masahiko Sakai and Mizuhito Ogawa. Weakly-non-overlapping non-collapsing shallow term rewriting systems are confluent. Inf. Process. Lett., 110(18-19):810-814, 2010. Google Scholar
  25. Masahiko Sakai, Michio Oyamaguchi, and Mizuhito Ogawa. Non-E-overlapping, weakly shallow, and non-collapsing TRSs are confluent. In CADE, 2015. to appear. Google Scholar
  26. Terese. Term rewriting systems. In Cambridge Tracts in Theoretical Computer Science, volume 55. Cambridge University Press, 2003. Google Scholar
  27. Yoshihito Toyama and Michio Oyamaguchi. Church-Rosser property and unique normal form property of non-duplicating term rewriting systems. In Nachum Dershowitz and Naomi Lindenstrauss, editors, Conditional and Typed Rewriting Systems, 4th International Workshop, CTRS-94, Jerusalem, Israel, July 13-15, 1994, Proceedings, volume 968 of Lecture Notes in Computer Science, pages 316-331. Springer, 1994. Google Scholar
  28. Vincent van Oostrom. Confluence by decreasing diagrams. Theor. Comput. Sci., 126(2):259-280, 1994. Google Scholar
  29. Vincent van Oostrom. Confluence by decreasing diagrams converted. In Andrei Voronkov, editor, Rewriting Techniques and Applications, 19th International Conference, RTA 2008, Hagenberg, Austria, July 15-17, 2008, Proceedings, volume 5117 of Lecture Notes in Computer Science, pages 306-320. Springer, 2008. Google Scholar
  30. Harald Zankl, Bertram Felgenhauer, and Aart Middeldorp. Labelings for decreasing diagrams. In Manfred Schmidt-Schauß, editor, Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, RTA 2011, May 30 - June 1, 2011, Novi Sad, Serbia, volume 10 of LIPIcs, pages 377-392. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact