Document Open Access Logo

A Coinductive Framework for Infinitary Rewriting and Equational Reasoning

Authors Jörg Endrullis, Helle Hvid Hansen, Dimitri Hendriks, Andrew Polonsky, Alexandra Silva

PDF
Thumbnail PDF

File

LIPIcs.RTA.2015.143.pdf
  • Filesize: 0.52 MB
  • 17 pages

Document Identifiers

Author Details

Jörg Endrullis
Helle Hvid Hansen
Dimitri Hendriks
Andrew Polonsky
Alexandra Silva

Cite AsGet BibTex

Jörg Endrullis, Helle Hvid Hansen, Dimitri Hendriks, Andrew Polonsky, and Alexandra Silva. A Coinductive Framework for Infinitary Rewriting and Equational Reasoning. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 143-159, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/LIPIcs.RTA.2015.143

Abstract

We present a coinductive framework for defining infinitary analogues of equational reasoning and rewriting in a uniform way. The setup captures rewrite sequences of arbitrary ordinal length, but it has neither the need for ordinals nor for metric convergence. This makes the framework especially suitable for formalizations in theorem provers.
Keywords
  • infinitary rewriting
  • coinduction

Metrics

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

References

  1. F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge Univ. Press, 1998. Google Scholar
  2. P. Bahr. Abstract Models of Transfinite Reductions. In Proc. Conf. on Rewriting Techniques and Applications (RTA 2010), volume 6 of Leibniz International Proceedings in Informatics, pages 49-66. Schloss Dagstuhl, 2010. Google Scholar
  3. P. Bahr. Partial Order Infinitary Term Rewriting and Böhm Trees. In Proc. Conf. on Rewriting Techniques and Applications (RTA 2010), volume 6 of Leibniz International Proceedings in Informatics, pages 67-84. Schloss Dagstuhl, 2010. Google Scholar
  4. P. Bahr. Infinitary Term Graph Rewriting is Simple, Sound and Complete. In Proc. Conf. on Rewriting Techniques and Applications (RTA 2012), volume 15 of Leibniz International Proceedings in Informatics, pages 69-84. Schloss Dagstuhl, 2012. Google Scholar
  5. H.P. Barendregt. The Type Free Lambda Calculus. In Handbook of Mathematical Logic, pages 1091-1132. Nort-Holland Publishing Company, Amsterdam, 1977. Google Scholar
  6. H.P. Barendregt and J.W. Klop. Applications of Infinitary Lambda Calculus. Information and Computation, 207(5):559-582, 2009. Google Scholar
  7. C. Coquand and Th. Coquand. On the Definition of Reduction for Infinite Terms. Comptes Rendus de l'Académie des Sciences. Série I, 323(5):553-558, 1996. Google Scholar
  8. Th. 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 LNCS, pages 62-78. Springer, 1994. Google Scholar
  9. \L. Czajka. A Coinductive Confluence Proof for Infinitary Lambda-Calculus. In Rewriting and Typed Lambda Calculi (RTA-TLCA 2014), volume 8560 of Lecture Notes in Computer Science, pages 164-178. Springer, 2014. Google Scholar
  10. Ł. Czajka. Coinductive Techniques in Infinitary Lambda-Calculus. ArXiv e-prints, 2015. Google Scholar
  11. N. Dershowitz, S. Kaplan, and D.A. Plaisted. Rewrite, Rewrite, Rewrite, Rewrite, Rewrite,\dots. Theoretical Computer Science, 83(1):71-96, 1991. Google Scholar
  12. J. Endrullis, R. C. de Vrijer, and J. Waldmann. Local Termination: Theory and Practice. Logical Methods in Computer Science, 6(3), 2010. Google Scholar
  13. J. Endrullis, C. Grabmayer, and D. Hendriks. Complexity of Fractran and Productivity. In Proc. Conf. on Automated Deduction (CADE 22), volume 5663 of LNCS, pages 371-387, 2009. Google Scholar
  14. J. Endrullis, C. Grabmayer, D. Hendriks, J.W. Klop, and R.C de Vrijer. Proving Infinitary Normalization. In Postproc. Int. Workshop on Types for Proofs and Programs (TYPES 2008), volume 5497 of LNCS, pages 64-82. Springer, 2009. Google Scholar
  15. J. Endrullis and D. Hendriks. Lazy Productivity via Termination. Theoretical Computer Science, 412(28):3203-3225, 2011. Google Scholar
  16. J. Endrullis, D. Hendriks, and M. Bodin. Circular Coinduction in Coq Using Bisimulation-Up-To Techniques. In Proc. Conf. on Interactive Theorem Proving (ITP), volume 7998 of LNCS, pages 354-369. Springer, 2013. Google Scholar
  17. J. Endrullis, D. Hendriks, C. Grabmayer, J.W. Klop, and V. van Oostrom. Infinitary term rewriting for weakly orthogonal systems: Properties and counterexamples. Logical Methods in Computer Science, 10(2:7):1-33, 2014. Google Scholar
  18. J. Endrullis, D. Hendriks, and J.W. Klop. Highlights in Infinitary Rewriting and Lambda Calculus. Theoretical Computer Science, 464:48-71, 2012. Google Scholar
  19. J. Endrullis and A. Polonsky. Infinitary Rewriting Coinductively. In Proc. Types for Proofs and Programs (TYPES 2012), volume 19 of Leibniz International Proceedings in Informatics, pages 16-27. Schloss Dagstuhl, 2013. Google Scholar
  20. J. Goguen, K. Lin, and G. Roşu. Circular Coinductive Rewriting. In Proc. of Automated Software Engineering, pages 123-131. IEEE, 2000. Google Scholar
  21. B. Jacobs and J.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
  22. F. Joachimski. Confluence of the Coinductive Lambda Calculus. Theoretical Computer Science, 311(1-3):105-119, 2004. Google Scholar
  23. S. Kahrs. Infinitary Rewriting: Foundations Revisited. In Proc. Conf. on Rewriting Techniques and Applications (RTA 2010), volume 6 of Leibniz International Proceedings in Informatics, pages 161-176. Schloss Dagstuhl, 2010. Google Scholar
  24. S. Kahrs. Infinitary Rewriting: Closure Operators, Equivalences and Models. Acta Informatica, 50(2):123-156, 2013. Google Scholar
  25. J.R. Kennaway and F.-J. de Vries. Infinitary Rewriting, chapter 12. Cambridge University Press, 2003. in [Terese, 2003]. Google Scholar
  26. J.R. Kennaway, J.W. Klop, M.R. Sleep, and F.-J. de Vries. Transfinite Reductions in Orthogonal Term Rewriting Systems. Information and Computation, 119(1):18-38, 1995. Google Scholar
  27. J. Ketema and J.G. Simonsen. Computing with Infinite Terms and Infinite Reductions. Unpublished manuscript. Google Scholar
  28. J.W. Klop. Term Rewriting Systems. In Handbook of Logic in Computer Science, volume II, pages 1-116. Oxford University Press, 1992. Google Scholar
  29. J.W. Klop and R.C de Vrijer. Infinitary Normalization. In We Will Show Them: Essays in Honour of Dov Gabbay (2), pages 169-192. College Publications, 2005. Google Scholar
  30. C. Lombardi, A. Ríos, and R.C de Vrijer. Proof Terms for Infinitary Rewriting. In Rewriting and Typed Lambda Calculi (RTA-TLCA 2014), volume 8560 of Lecture Notes in Computer Science, pages 303-318. Springer, 2014. Google Scholar
  31. J.G. Simonsen. On Confluence and Residuals in Cauchy Convergent Transfinite Rewriting. Information Processing Letters, 91(3):141-146, 2004. Google Scholar
  32. Terese. Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003. Google Scholar
  33. M. Vermaat. Infinitary Rewriting in Coq. Available at url URL: http://martijn.vermaat.name/master-project/.
  34. H. Zantema. Normalization of Infinite Terms. In Proc. Conf. on Rewriting Techniques and Applications (RTA 2008), number 5117 in LNCS, pages 441-455, 2008. Google Scholar
  35. H. Zantema and M. Raffelsieper. Proving Productivity in Infinite Data Structures. In Proc. Conf. on Rewriting Techniques and Applications (RTA 2010), volume 6 of Leibniz International Proceedings in Informatics, pages 401-416. Schloss Dagstuhl, 2010. 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