Document Open Access Logo

Confluence of nearly orthogonal infinitary term rewriting systems

Author Lukasz Czajka

PDF
Thumbnail PDF

File

LIPIcs.RTA.2015.106.pdf
  • Filesize: 0.56 MB
  • 21 pages

Document Identifiers

Author Details

Lukasz Czajka

Cite As Get BibTex

Lukasz Czajka. Confluence of nearly orthogonal infinitary term rewriting systems. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 106-126, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.RTA.2015.106

Abstract

We give a relatively simple coinductive proof of confluence, modulo
equivalence of root-active terms, of nearly orthogonal infinitary
term rewriting systems. Nearly orthogonal systems allow certain root
overlaps, but no non-root overlaps. Using a slightly more complicated method we also show confluence modulo equivalence of
hypercollapsing terms. The condition we impose on root overlaps is
similar to the condition used by Toyama in the context of finitary
rewriting.

Subject Classification

Keywords
  • infinitary rewriting
  • confluence
  • coinduction

Metrics

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

References

  1. Patrick Bahr. Partial order infinitary term rewriting and Böhm trees. In Christopher Lynch, editor, Proceedings of the 21st International Conference on Rewriting Techniques and Applications, RTA 2010, July 11-13, 2010, Edinburgh, Scottland, UK, volume 6 of LIPIcs, pages 67-84. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010. Google Scholar
  2. Patrick Bahr. Partial order infinitary term rewriting. Logical Methods in Computer Science, 10(2), 2014. Google Scholar
  3. Yves Bertot and Pierre Castéran. Interactive Theorem Proving and Program Development: Coq'Art: the Calculus of Inductive Constructions, chapter 13. Springer, 2004. Google Scholar
  4. Marc Bezem, Keiko Nakata, and Tarmo Uustalu. On streams that are finitely red. Logical Methods in Computer Science, 8:1-20, 2012. Google Scholar
  5. Adam Chlipala. Certified Programming with Dependent Types, chapter 5. The MIT Press, 2013. Google Scholar
  6. Thierry Coquand. Infinite objects in type theory. In Henk Barendregt and Tobias Nipkow, editors, Types for Proofs and Programs, International Workshop TYPES'93, Nijmegen, The Netherlands, May 24-28, 1993, Selected Papers, volume 806 of Lecture Notes in Computer Science, pages 62-78. Springer, 1993. Google Scholar
  7. Łukasz Czajka. A coinductive confluence proof for infinitary lambda-calculus. In 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, pages 164-178. Springer, 2014. Google Scholar
  8. Łukasz Czajka. Coinductive techniques in infinitary lambda-calculus. In preparation, preprint available at http://arxiv.org/abs/1501.04354, 2015.
  9. Brian A. Davey and Hilary A. Priestley. Introduction to Lattices and Order. Cambridge University Press, 2nd edition, 2002. Google Scholar
  10. Jörg Endrullis, Clemens Grabmayer, Dimitri Hendriks, Jan Willem Klop, and Vincent van Oostrom. Unique normal forms in infinitary weakly orthogonal rewriting. In C. Lynch, editor, Proceedings of the Conference on Rewriting Techniques and Applications (RTA 2010), volume 6 of Leibniz International Proceedings in Informatics (LIPIcs), pages 85-102. Dagstuhl, 2010. Google Scholar
  11. Jörg Endrullis, Clemens Grabmayer, Dimitri Hendriks, Jan Willem Klop, and Vincent van Oostrom. Infinitary term rewriting for weakly orthogonal systems: properties and examples. Logical Methods in Computer Science, 10:1-33, 2014. Google Scholar
  12. Jörg Endrullis, Helle Hvid Hansen, Dimitri Hendriks, Andrew Polonsky, and Alexandra Silva. A coinductive treatment of infinitary rewriting. Unpublished, available at http://arxiv.org/abs/1306.6224, 2013.
  13. Jörg Endrullis, Dimitri Hendriks, and Jan Willem Klop. Highlights in infinitary rewriting and lambda calculus. Theoretical Computer Science, 464:48-71, 2012. Google Scholar
  14. Jörg Endrullis, Dimitri Hendriks, Jan Willem Klop, and Andrew Polonsky. Discriminating lambda-terms using clocked Böhm trees. Logical Methods in Computer Science, 10(2), 2014. Google Scholar
  15. Jörg Endrullis and Andrew Polonsky. Infinitary rewriting coinductively. In Nils Anders Danielsson and Bengt Nordström, editors, TYPES, volume 19 of LIPIcs, pages 16-27. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011. Google Scholar
  16. Eduardo Giménez. Codifying guarded definitions with recursive schemes. In Peter Dybjer, Bengt Nordström, and Jan M. Smith, editors, TYPES, volume 996 of Lecture Notes in Computer Science, pages 39-59. Springer, 1994. Google Scholar
  17. Bernhard Gramlich. Confluence without termination via parallel critical pairs. In Hélène Kirchner, editor, Trees in Algebra and Programming - CAAP'96, 21st International Colloquium, Linköping, Sweden, April, 22-24, 1996, Proceedings, volume 1059 of Lecture Notes in Computer Science, pages 211-225. Springer, 1996. Google Scholar
  18. Gérard P. Huet. Confluent reductions: Abstract properties and applications to term rewriting systems. J. ACM, 27(4):797-821, 1980. Google Scholar
  19. Bart Jacobs and Jan J.M.M. Rutten. An introduction to (co)algebras and (co)induction. In Advanced Topics in Bisimulation and Coinduction, pages 38-99. Cambridge University Press, 2011. Google Scholar
  20. Felix Joachimski. Confluence of the coinductive [lambda]-calculus. Theoretical Computer Science, 311(1-3):105-119, 2004. Google Scholar
  21. Richard Kennaway and Fer-Jan de Vries. Infinitary rewriting. In Terese, editor, Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science, chapter 12, pages 668-711. Cambridge University Press, 2003. Google Scholar
  22. Richard Kennaway, Jan Willem Klop, M. Ronan Sleep, and Fer-Jan de Vries. Transfinite reductions in orthogonal term rewriting systems. Information and Computation, 119(1):18-38, 1995. Google Scholar
  23. Richard Kennaway, Vincent van Oostrom, and Fer-Jan de Vries. Meaningless terms in rewriting. Journal of Functional and Logic Programming, 1:1-35, 1999. Google Scholar
  24. Jeroen Ketema. Böhm-like trees for term rewriting systems. In Vincent van Oostrom, editor, Rewriting Techniques and Applications, 15th International Conference, RTA 2004, Aachen, Germany, June 3-5, 2004, Proceedings, volume 3091 of Lecture Notes in Computer Science, pages 233-248. Springer, 2004. Google Scholar
  25. Jeroen Ketema. Comparing Böhm-like trees. In Ralf Treinen, editor, Rewriting Techniques and Applications, 20th International Conference, RTA 2009, Brasília, Brazil, June 29 - July 1, 2009, Proceedings, volume 5595 of Lecture Notes in Computer Science, pages 239-254. Springer, 2009. Google Scholar
  26. Jeroen Ketema. Reinterpreting compression in infinitary rewriting. In Ashish Tiwari, editor, 23rd International Conference on Rewriting Techniques and Applications (RTA'12) , RTA 2012, May 28 - June 2, 2012, Nagoya, Japan, volume 15 of LIPIcs, pages 209-224. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. Google Scholar
  27. Jeroen Ketema and Jakob Grue Simonsen. Infinitary combinatory reduction systems. Information and Computation, 209(6):893-926, 2011. Google Scholar
  28. Jan Willem Klop and Roel C. de Vrijer. Infinitary normalization. In Sergei N. Artëmov, Howard Barringer, Artur S. d'Avila Garcez, Luís C. Lamb, and John Woods, editors, We Will Show Them! Essays in Honour of Dov Gabbay, Volume Two, pages 169-192. College Publications, 2005. Google Scholar
  29. Dexter Kozen and Alexandra Silva. Practical coinduction. Draft, 2014. Google Scholar
  30. Xavier Leroy and Hervé Grall. Coinductive big-step operational semantics. Information and Computation, 207(2):284-304, 2009. Google Scholar
  31. Keiko Nakata and Tarmo Uustalu. Resumptions, weak bisimilarity and big-step semantics for while with interactive I/O: An exercise in mixed induction-coinduction. In L. Aceto and P. Sobociński, editors, Seventh Workshop on Structural Operational Semantics (SOS'10), pages 57-75, 2010. Google Scholar
  32. Jan J.M.M. Rutten. Universal coalgebra: a theory of systems. Theoretical Computer Science, 249(1):3-80, 2000. Google Scholar
  33. Davide Sangiorgi. Introduction to Bisimulation and Coinduction. Cambridge University Press, 2012. Google Scholar
  34. Yoshihito Toyama. Commutativity of term rewriting systems. In K. Fuchi and L. Kott, editors, Programming of Future Generation Computers II, pages 393-407. North-Holland, 1988. Google Scholar
  35. Vincent van Oostrom. Development closed critical pairs. In Gilles Dowek, Jan Heering, Karl Meinke, and Bernhard Möller, editors, HOA, volume 1074 of Lecture Notes in Computer Science, pages 185-200. Springer, 1995. Google Scholar
  36. Vincent van Oostrom. Developing developments. Theoretical Computer Science, 175(1):159-181, 1997. 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 About DROPS Imprint Privacy Contact