Document Open Access Logo

Reductions in Higher-Order Rewriting and Their Equivalence

Authors Pablo Barenbaum, Eduardo Bonelli

PDF
Thumbnail PDF

File

LIPIcs.CSL.2023.8.pdf
  • Filesize: 0.74 MB
  • 18 pages

Document Identifiers

Author Details

Pablo Barenbaum
  • National University of Quilmes (CONICET), Bernal, Argentina
  • University of Buenos Aires, Argentina
Eduardo Bonelli
  • Stevens Institute of Technology, Hoboken, NJ, USA

Funding

  • Barenbaum, Pablo: Partially supported by project ECOS-Sud A17C01.

Cite AsGet BibTex

Pablo Barenbaum and Eduardo Bonelli. Reductions in Higher-Order Rewriting and Their Equivalence. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.CSL.2023.8

Abstract

Proof terms are syntactic expressions that represent computations in term rewriting. They were introduced by Meseguer and exploited by van Oostrom and de Vrijer to study equivalence of reductions in (left-linear) first-order term rewriting systems. We study the problem of extending the notion of proof term to higher-order rewriting, which generalizes the first-order setting by allowing terms with binders and higher-order substitution. In previous works that devise proof terms for higher-order rewriting, such as Bruggink’s, it has been noted that the challenge lies in reconciling composition of proof terms and higher-order substitution (β-equivalence). This led Bruggink to reject "nested" composition, other than at the outermost level. In this paper, we propose a notion of higher-order proof term we dub rewrites that supports nested composition. We then define two notions of equivalence on rewrites, namely permutation equivalence and projection equivalence, and show that they coincide.

Subject Classification

ACM Subject Classification
  • Theory of computation → Equational logic and rewriting
  • Theory of computation → Type theory
Keywords
  • Term Rewriting
  • Higher-Order Rewriting
  • Proof terms
  • Equivalence of Computations

Metrics

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

Related Versions

References

  1. Pablo Barenbaum and Eduardo Bonelli. Rewrites as terms through justification logic. In PPDP '20: 22nd International Symposium on Principles and Practice of Declarative Programming, Bologna, Italy, 9-10 September, 2020, pages 11:1-11:13. ACM, 2020. Google Scholar
  2. Pablo Barenbaum and Eduardo Bonelli. Reductions in higher-order rewriting and their equivalence. CoRR, 2022. Google Scholar
  3. Sander Bruggink. Residuals in higher-order rewriting. In Robert Nieuwenhuis, editor, Rewriting Techniques and Applications, 14th International Conference, RTA 2003, Valencia, Spain, June 9-11, 2003, Proceedings, volume 2706 of Lecture Notes in Computer Science, pages 123-137. Springer, 2003. Google Scholar
  4. Sander Bruggink. Equivalence of reductions in higher-order rewriting. PhD thesis, Utrecht University, 2008. Available from: URL: http://www.ti.inf.uni-due.de/publications/bruggink/thesis.pdf.
  5. P. Dehornoy, F. Digne, E. Godelle, D. Krammer, and J. Michel. Foundations of Garside Theory. EMS tracts in mathematics. European Mathematical Society, 2015. Available from: URL: https://books.google.com.ar/books?id=7ec_SGVzNhEC.
  6. Barney P. Hilken. Towards a proof theory of rewriting: The simply typed 2λ-calculus. Theor. Comput. Sci., 170(1-2):407-444, 1996. Google Scholar
  7. Tom Hirschowitz. Cartesian closed 2-categories and permutation equivalence in higher-order rewriting. Log. Methods Comput. Sci., 9(3), 2013. Google Scholar
  8. Jan Willem Klop. Combinatory Reduction Systems. PhD thesis, Utrecht University, 1980. Google Scholar
  9. Christina Kohl and Aart Middeldorp. Protem: A proof term manipulator (system description). In Hélène Kirchner, editor, 3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018, July 9-12, 2018, Oxford, UK, volume 108 of LIPIcs, pages 31:1-31:8. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. Google Scholar
  10. Christina Kohl and Aart Middeldorp. Composing proof terms. In Pascal Fontaine, editor, Automated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings, volume 11716 of Lecture Notes in Computer Science, pages 337-353. Springer, 2019. Google Scholar
  11. Jean-Jacques Lévy. Réductions correctes et optimales dans le lambda-calcul. PhD thesis, Université de Paris 7, 1978. Google Scholar
  12. Richard Mayr and Tobias Nipkow. Higher-order rewrite systems and their confluence. Theoretical Computer Science, 192:3-29, 1998. Google Scholar
  13. José Meseguer. Conditioned rewriting logic as a united model of concurrency. Theor. Comput. Sci., 96(1):73-155, 1992. Google Scholar
  14. Tobias Nipkow. Higher-order critical pairs. In Proceedings 1991 Sixth Annual IEEE Symposium on Logic in Computer Science, pages 342-343. IEEE Computer Society, 1991. Google Scholar
  15. Terese. Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003. Google Scholar
  16. Vincent van Oostrom. Normalisation in weakly orthogonal rewriting. In Paliath Narendran and Michaël Rusinowitch, editors, Rewriting Techniques and Applications, 10th International Conference, RTA-99, Trento, Italy, July 2-4, 1999, Proceedings, volume 1631 of Lecture Notes in Computer Science, pages 60-74. Springer, 1999. Google Scholar
  17. Vincent van Oostrom and Roel C. de Vrijer. Four equivalent equivalences of reductions. Electron. Notes Theor. Comput. Sci., 70(6):21-61, 2002. 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