Conference Paper/Proceeding/Abstract 40 views
On Complexity of Confluence and Church-Rosser Proofs
Arnold Beckmann 
,
Georg Moser
,
Georg Moser
Mathematical Foundations of Computer Science (MFCS)
Swansea University Author:
Arnold Beckmann
Full text not available from this repository: check for access using links below.
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...
| Published in: | Mathematical Foundations of Computer Science (MFCS) |
|---|---|
| Published: |
|
| 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. |
|---|---|
| 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 |