Document Open Access Logo

Narrowing Trees for Syntactically Deterministic Conditional Term Rewriting Systems

Authors Naoki Nishida , Yuya Maeda

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2018.26.pdf
  • Filesize: 0.59 MB
  • 20 pages

Document Identifiers

Author Details

Naoki Nishida
  • Graduate School of Informatics, Nagoya University, Nagoya, Japan
Yuya Maeda
  • Graduate School of Informatics, Nagoya University, Nagoya, Japan

Funding

This work was partially supported by JSPS KAKENHI Grant Number JP17H01722.

Cite AsGet BibTex

Naoki Nishida and Yuya Maeda. Narrowing Trees for Syntactically Deterministic Conditional Term Rewriting Systems. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 26:1-26:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.FSCD.2018.26

Abstract

A narrowing tree for a constructor term rewriting system and a pair of terms is a finite representation for the space of all possible innermost-narrowing derivations that start with the pair and end with non-narrowable terms. Narrowing trees have grammar representations that can be considered regular tree grammars. Innermost narrowing is a counterpart of constructor-based rewriting, and thus, narrowing trees can be used in analyzing constructor-based rewriting to normal forms. In this paper, using grammar representations, we extend narrowing trees to syntactically deterministic conditional term rewriting systems that are constructor systems. We show that narrowing trees are useful to prove two properties of a normal conditional term rewriting system: one is infeasibility of conditional critical pairs and the other is quasi-reducibility.

Subject Classification

ACM Subject Classification
  • Theory of computation → Rewrite systems
Keywords
  • conditional term rewriting
  • innermost narrowing
  • regular tree grammar

Metrics

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

References

  1. Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. Google Scholar
  2. Adel Bouhoula and Florent Jacquemard. Sufficient completeness verification for conditional and constrained TRS. Journal of Applied Logic, 10(1):127-143, 2012. Google Scholar
  3. Hubert Comon, Max Dauchet, Rémi Gilleron, Florent Jacquemard, Denis Lugiez, Christof Löding, Sophie Tison, and Marc Tommasi. Tree Automata Techniques and Applications, 2007. Release October, 12th 2007. Google Scholar
  4. Nachum Dershowitz, Mitsuhiro Okada, and G. Sivakumar. Canonical conditional rewrite systems. In Proceedings of the 9th International Conference on Automated Deduction, volume 310 of Lecture Notes in Computer Science, pages 538-549. Springer, 1988. Google Scholar
  5. Francisco Durán, Salvador Lucas, José Meseguer, Claude Marché, and Xavier Urbain. Proving termination of membership equational programs. In Nevin Heintze and Peter Sestoft, editors, Proceedings of the 2004 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation, pages 147-158. ACM, 2004. Google Scholar
  6. Guillaume Feuillade and Thomas Genet. Reachability in conditional term rewriting systems. Electronic Notes in Theoretical Computer Science, 86(1):133-146, 2003. Google Scholar
  7. Thomas Genet. Decidable approximations of sets of descendants and sets of normal forms. In Tobias Nipkow, editor, Proceedings of the 9th International Conference on Rewriting Techniques and Applications, volume 1379 of Lecture Notes in Computer Science, pages 151-165. Springer, 1998. Google Scholar
  8. Karl Gmeiner. CoScart: Confluence prover in Scala. In Ashish Tiwari and Takahito Aoto, editors, Proceedings of the 4th International Workshop on Confluence, page 45, 2015. Google Scholar
  9. Karl Gmeiner and Naoki Nishida. Notes on structure-preserving transformations of conditional term rewrite systems. In Manfred Schmidt-Schauß, Masahiko Sakai, David Sabel, and Yuki Chiba, editors, Proceedings of the first International Workshop on Rewriting Techniques for Program Transformations and Evaluation, volume 40 of OpenAccess Series in Informatics, pages 3-14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014. Google Scholar
  10. Karl Gmeiner, Naoki Nishida, and Bernhard Gramlich. Proving confluence of conditional term rewriting systems via unravelings. In Nao Hirokawa and Vincent van Oostrom, editors, Proceedings of the 2nd International Workshop on Confluence, pages 35-39, 2013. Google Scholar
  11. Raúl Gutiérrez, Salvador Lucas, and Patricio Reinoso. A tool for the automatic generation of logical models of order-sorted first-order theories. In Alicia Villanueva, editor, Proceedings of the XVI Jornadas sobre Programación y Lenguages, pages 215-230, 2016. Tool available at URL: http://zenon.dsic.upv.es/ages/.
  12. John V. Guttag. The Specification and Application to Programming of Abstract Data Types. PhD thesis, University of Tronto, Toronto, Canada, 1975. Google Scholar
  13. Manuel V. Hermenegildo and Francesca Rossi. On the correctness and efficiency of independent and-parallelism in logic programs. In Ewing L. Lusk and Ross A. Overbeek, editors, Proceedings of the North American Conference on Logic Programming, pages 369-389. MIT Press, 1989. Google Scholar
  14. Jean-Marie Hullot. Canonical forms and unification. In Wolfgang Bibel and Robert A. Kowalski, editors, Proceedings of the 5th Conference on Automated Deduction, volume 87 of Lecture Notes in Computer Science, pages 318-334. Springer, 1980. Google Scholar
  15. Deepak Kapur, Paliath Narendran, and Hantao Zhang. On sufficient-completeness and related properties of term rewriting systems. Acta Informatica, 24(4):395-415, 1987. Google Scholar
  16. Emmanuel Kounalis. Completeness in data type specifications. In Bob F. Caviness, editor, Proceedings of the European Conference on Computer Algebra, volume 204 of Lecture Notes in Computer Science, pages 348-362. Springer, 1985. Google Scholar
  17. Marija Kulaš. A practical view on renaming. In Sibylle Schwarz and Janis Voigtländer, editors, Proceedings of the 29th and 30th Workshops on (Constraint) Logic Programming and 24th International Workshop on Functional and (Constraint) Logic Programming, and 24th International Workshop on Functional and (Constraint) Logic Programming, volume 234 of Electronic Proceedings in Theoretical Computer Science, pages 27-41, 2017. Google Scholar
  18. Salvador Lucas. A semantic approach to the analysis of rewriting-based systems. In Fabio Fioravanti and John P. Gallagher, editors, Pre-Proceedings of the 27th International Symposium on Logic-Based Program Synthesis and Transformation, 2017. CoRR, abs/1709.05095. Google Scholar
  19. Salvador Lucas and Raúl Gutiérrez. A semantic criterion for proving infeasibility in conditional rewriting. In Beniamino Accattoli and Bertram Felgenhauer, editors, Proceedings of the 6th International Workshop on Confluence, pages 15-20, 2017. Google Scholar
  20. Salvador Lucas and Raúl Gutiérrez. Automatic synthesis of logical models for order-sorted first-order theories. Journal of Automated Reasoning, 60(4):465-01, 2018. Google Scholar
  21. Salvador Lucas, Claude Marché, and José Meseguer. Operational termination of conditional term rewriting systems. Information Processing Letters, 95(4):446-453, 2005. Google Scholar
  22. Massimo Marchiori. Unravelings and ultra-properties. In Michael Hanus and Mario Rodríguez-Artalejo, editors, Proceedings of the 5th International Conference on Algebraic and Logic Programming, volume 1139 of Lecture Notes in Computer Science, pages 107-121. Springer, 1996. Google Scholar
  23. Aart Middeldorp and Erik Hamoen. Completeness results for basic narrowing. Applicable Algebra in Engineering, Communication and Computing, 5:213-253, 1994. Google Scholar
  24. Masanori Nagashima, Masahiko Sakai, and Toshiki Sakabe. Determinization of conditional term rewriting systems. Theoretical Computer Science, 464:72-89, 2012. Google Scholar
  25. Naoki Nishida, Takayuki Kuroda, Makishi Yanagisawa, and Karl Gmeiner. CO3: a COnverter for proving COnfluence of COnditional TRSs. In Ashish Tiwari and Takahito Aoto, editors, Proceedings of the 4th International Workshop on Confluence, page 42, 2015. Google Scholar
  26. Naoki Nishida, Adrián Palacios, and Germán Vidal. Reversible computation in term rewriting. Journal of Logical and Algebraic Methods in Programming, 94:128-149, 2018. Google Scholar
  27. Naoki Nishida and Germán Vidal. Program inversion for tail recursive functions. In Manfred Schmidt-Schauß, editor, Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, volume 10 of Leibniz International Proceedings in Informatics, pages 283-298. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011. Google Scholar
  28. Naoki Nishida and Germán Vidal. Computing more specific versions of conditional rewriting systems. In Elvira Albert, editor, Revised Selected Papers of the 22nd International Symposium on Logic-Based Program Synthesis and Transformation, volume 7844 of Lecture Notes in Computer Science, pages 137-154. Springer, 2013. Google Scholar
  29. Naoki Nishida and Germán Vidal. A finite representation of the narrowing space. In Gopal Gupta and Ricardo Peña, editors, Revised Selected Papers of the 23rd International Symposium on Logic-Based Program Synthesis and Transformation, volume 8901 of Lecture Notes in Computer Science, pages 54-71. Springer, 2014. Google Scholar
  30. Naoki Nishida and Germán Vidal. A framework for computing finite SLD trees. Journal of Logic and Algebraic Methods in Programming, 84(2):197-217, 2015. Google Scholar
  31. Naoki Nishida, Makishi Yanagisawa, and Karl Gmeiner. On proving confluence of conditional term rewriting systems via the computationally equivalent transformation. In Takahito Aoto and Delia Kesner, editors, Proceedings of the 3rd International Workshop on Confluence, pages 24-28, 2014. Google Scholar
  32. Enno Ohlebusch. Advanced Topics in Term Rewriting. Springer, 2002. Google Scholar
  33. Catuscia Palamidessi. Algebraic properties of idempotent substitutions. In Mike Paterson, editor, Proceedings of the 17th International Colloquium on Automata, Languages and Programming, volume 443 of Lecture Notes in Computer Science, pages 386-399. Springer, 1990. Google Scholar
  34. James R. Slagle. Automated theorem-proving for theories with simplifiers, commutativity and associativity. Journal of the ACM, 21(4):622-642, 1974. Google Scholar
  35. Thomas Sternagel and Aart Middeldorp. Conditional confluence (system description). In Gilles Dowek, editor, Proceedings of the Joint International Conference on Rewriting and Typed Lambda Calculi, volume 8560 of Lecture Notes in Computer Science, pages 456-465. Springer, 2014. Google Scholar
  36. Thomas Sternagel and Aart Middeldorp. Infeasible conditional critical pairs. In Ashish Tiwari and Takahito Aoto, editors, Proceedings of the 4th International Workshop on Confluence, pages 13-17, 2015. Google Scholar
  37. Taro Suzuki, Aart Middeldorp, and Tetsuo Ida. Level-confluence of conditional rewrite systems with extra variables in right-hand sides. In Jieh Hsiang, editor, Proceedings of the 6th International Conference on Rewriting Techniques and Applications, volume 914 of Lecture Notes in Computer Science, pages 179-193. Springer, 1995. 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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact