Document Open Access Logo

On Complexity of Confluence and Church-Rosser Proofs

Authors Arnold Beckmann , Georg Moser

PDF

File

Thumbnail PDF
PDF
LIPIcs.MFCS.2024.21.pdf
  • Filesize: 1.65 MB
  • 16 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
Keywords
  • logic
  • bounded arithmetic
  • consistency
  • rewriting

Metrics

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

Abstract

In this paper, we investigate confluence and the Church-Rosser property - two well-studied properties of rewriting and the λ-calculus - from the viewpoint of proof complexity. With respect to confluence, and focusing on orthogonal term rewrite systems, our main contribution is that the size, measured in number of symbols, of the smallest rewrite proof is polynomial in the size of the peak. For the Church-Rosser property we obtain exponential lower bounds for the size of the join in the size of the equality proof. Finally, we study the complexity of proving confluence in the context of the λ-calculus. Here, we establish an exponential (worst-case) lower bound of the size of the join in the size of the peak.

Cite As Get BibTex

Arnold Beckmann and Georg Moser. On Complexity of Confluence and Church-Rosser Proofs. In 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 306, pp. 21:1-21:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.MFCS.2024.21

Author Details

Arnold Beckmann
  • Department of Computer Science, Swansea University, UK
Georg Moser
  • Department of Computer Science, University of Innsbruck, Austria

Funding

  • Beckmann, Arnold: Royal Society International Exchanges Grant, IESbackslash R3backslash 223051
  • Moser, Georg: Royal Society International Exchanges Grant, IESbackslash R3backslash 223051

References

  1. Martin Avanzini and Georg Moser. Complexity of Acyclic Term Graph Rewriting. In Prof. 1st FSCD, volume 52 of LIPIcs, pages 10:1-10:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPICS.FSCD.2016.10.
  2. Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. Google Scholar
  3. Hendrik Pieter Barendregt. The lambda calculus - its syntax and semantics, volume 103 of Studies in logic and the foundations of mathematics. North-Holland, 1985. Google Scholar
  4. Henk Barendregt and Giulio Manzonetto. A Lambda Calculus Satellite. College Publications, 2022. Google Scholar
  5. Arnold Beckmann. Proving Consistency of Equational Theories in Bounded Arithmetic. J. Symb. Log., 67(1):279-296, 2002. URL: https://doi.org/10.2178/JSL/1190150044.
  6. Samuel R. Buss. Bounded Arithmetic. Bibliopolis, Naples, Italy, 1986. Google Scholar
  7. Samuel R. Buss and Aleksandar Ignjatović. Unprovability of consistency statements in fragments of bounded arithmetic. Ann. Pure Appl. Logic, 74(3):221-244, 1995. Google Scholar
  8. Alonzo Church and J. Barkley Rosser. Some properties of conversion. Transaction of the American Mathematical Society, 39:472-482, 1936. Google Scholar
  9. Anupam Das. From positive and intuitionistic bounded arithmetic to monotone proof complexity. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, pages 126-135, New York, NY, USA, 2016. Association for Computing Machinery. Google Scholar
  10. Ken-etsu Fujita. The Church-Rosser theorem and quantitative analysis of witnesses. Inf. Comput., 263:52-56, 2018. URL: https://doi.org/10.1016/J.IC.2018.09.002.
  11. Jeroen Ketema and Jakob Grue Simonsen. Least upper bounds on the size of confluence and church-rosser diagrams in term rewriting and λ-calculus. ACM Trans. Comput. Log., 14(4):31:1-31:28, 2013. URL: https://doi.org/10.1145/2528934.
  12. Terese. Term Rewriting Systems. Cambridge University Press, 2003. Google Scholar
  13. Yoyuki Yamagata. Consistency proof of a fraement of pv with substitution in bounded arithmetic. The Journal of Symbolic Logic, 83(3):1063-1090, 2018. URL: https://doi.org/10.1017/jsl.2018.14.
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