LIPIcs.MFCS.2024.21.pdf
- Filesize: 1.65 MB
- 16 pages
Document
On Complexity of Confluence and Church-Rosser Proofs
Authors
Arnold Beckmann 
,
Georg Moser
-
Part of:
Volume:
49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Mathematical Foundations of Computer Science (MFCS) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2024-08-23
File
Document Identifiers
Author Details
Cite AsGet 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
https://doi.org/10.4230/LIPIcs.MFCS.2024.21
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.
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)
0PDF Downloads
References
- 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.
-
Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.
-
Hendrik Pieter Barendregt. The lambda calculus - its syntax and semantics, volume 103 of Studies in logic and the foundations of mathematics. North-Holland, 1985.
-
Henk Barendregt and Giulio Manzonetto. A Lambda Calculus Satellite. College Publications, 2022.
- 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.
-
Samuel R. Buss. Bounded Arithmetic. Bibliopolis, Naples, Italy, 1986.
-
Samuel R. Buss and Aleksandar Ignjatović. Unprovability of consistency statements in fragments of bounded arithmetic. Ann. Pure Appl. Logic, 74(3):221-244, 1995.
-
Alonzo Church and J. Barkley Rosser. Some properties of conversion. Transaction of the American Mathematical Society, 39:472-482, 1936.
-
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.
- 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.
- 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.
-
Terese. Term Rewriting Systems. Cambridge University Press, 2003.
- 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.