2026-07-22T06:30:42Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:20577 2024-08-23T05:50:28Z ddc:004 open_access

On Complexity of Confluence and Church-Rosser Proofs Beckmann, Arnold Moser, Georg logic bounded arithmetic consistency rewriting 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Arnold Beckmann and Georg Moser 2024 Is Part Of LIPIcs, Volume 306, 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.MFCS.2024.21 urn:nbn:de:0030-drops-205774 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2024.21 eng https://creativecommons.org/licenses/by/4.0/legalcode