No Cover Image

Conference Paper/Proceeding/Abstract 106 views 4 downloads

On Complexity of Confluence and Church-Rosser Proofs

Arnold Beckmann Orcid Logo, Georg Moser

Mathematical Foundations of Computer Science (MFCS), Volume: 306

Swansea University Author: Arnold Beckmann Orcid Logo

  • 67544.pdf

    PDF | Version of Record

    © Arnold Beckmann and Georg Moser. Licensed under Creative Commons License CC-BY 4.0.

    Download (1.74MB)

Check full text

DOI (Published version): 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, measure...

Full description

Published in: Mathematical Foundations of Computer Science (MFCS)
ISBN: 978-3-95977-335-5
ISSN: 1868-8969
Published: Schloss Dagstuhl – Leibniz-Zentrum für Informatik 2024
Online Access: Check full text

URI: https://cronfa.swan.ac.uk/Record/cronfa67544
Tags: Add Tag
No Tags, Be the first to tag this record!
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.
Keywords: logic, bounded arithmetic, consistency, rewriting
College: Faculty of Science and Engineering
Funders: Arnold Beckmann: Royal Society International Exchanges Grant, IES\R3\223051 Georg Moser: Royal Society International Exchanges Grant, IES\R3\223051

Similar Items