No Cover Image

Conference Paper/Proceeding/Abstract 40 views

On Complexity of Confluence and Church-Rosser Proofs

Arnold Beckmann Orcid Logo, Georg Moser

Mathematical Foundations of Computer Science (MFCS)

Swansea University Author: Arnold Beckmann Orcid Logo

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...

Full description

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!
first_indexed 2024-09-03T09:38:36Z
last_indexed 2024-09-03T09:38:36Z
id cronfa67544
recordtype SURis
fullrecord <?xml version="1.0" encoding="utf-8"?><rfc1807 xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xsd="http://www.w3.org/2001/XMLSchema"><bib-version>v2</bib-version><id>67544</id><entry>2024-09-03</entry><title>On Complexity of Confluence and Church-Rosser Proofs</title><swanseaauthors><author><sid>1439ebd690110a50a797b7ec78cca600</sid><ORCID>0000-0001-7958-5790</ORCID><firstname>Arnold</firstname><surname>Beckmann</surname><name>Arnold Beckmann</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2024-09-03</date><deptcode>MACS</deptcode><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.</abstract><type>Conference Paper/Proceeding/Abstract</type><journal>Mathematical Foundations of Computer Science (MFCS)</journal><volume/><journalNumber/><paginationStart/><paginationEnd/><publisher/><placeOfPublication/><isbnPrint/><isbnElectronic/><issnPrint/><issnElectronic/><keywords/><publishedDay>0</publishedDay><publishedMonth>0</publishedMonth><publishedYear>0</publishedYear><publishedDate>0001-01-01</publishedDate><doi>10.4230/LIPIcs.MFCS.2024.21</doi><url/><notes/><college>COLLEGE NANME</college><department>Mathematics and Computer Science School</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>MACS</DepartmentCode><institution>Swansea University</institution><apcterm/><funders>Arnold Beckmann: Royal Society International Exchanges Grant, IES\R3\223051 Georg Moser: Royal Society International Exchanges Grant, IES\R3\223051</funders><projectreference/><lastEdited>2024-09-03T10:38:37.0757455</lastEdited><Created>2024-09-03T10:33:17.7931484</Created><path><level id="1">Faculty of Science and Engineering</level><level id="2">School of Mathematics and Computer Science - Computer Science</level></path><authors><author><firstname>Arnold</firstname><surname>Beckmann</surname><orcid>0000-0001-7958-5790</orcid><order>1</order></author><author><firstname>Georg</firstname><surname>Moser</surname><order>2</order></author></authors><documents/><OutputDurs/></rfc1807>
spelling v2 67544 2024-09-03 On Complexity of Confluence and Church-Rosser Proofs 1439ebd690110a50a797b7ec78cca600 0000-0001-7958-5790 Arnold Beckmann Arnold Beckmann true false 2024-09-03 MACS 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. Conference Paper/Proceeding/Abstract Mathematical Foundations of Computer Science (MFCS) 0 0 0 0001-01-01 10.4230/LIPIcs.MFCS.2024.21 COLLEGE NANME Mathematics and Computer Science School COLLEGE CODE MACS Swansea University Arnold Beckmann: Royal Society International Exchanges Grant, IES\R3\223051 Georg Moser: Royal Society International Exchanges Grant, IES\R3\223051 2024-09-03T10:38:37.0757455 2024-09-03T10:33:17.7931484 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Arnold Beckmann 0000-0001-7958-5790 1 Georg Moser 2
title On Complexity of Confluence and Church-Rosser Proofs
spellingShingle On Complexity of Confluence and Church-Rosser Proofs
Arnold Beckmann
title_short On Complexity of Confluence and Church-Rosser Proofs
title_full On Complexity of Confluence and Church-Rosser Proofs
title_fullStr On Complexity of Confluence and Church-Rosser Proofs
title_full_unstemmed On Complexity of Confluence and Church-Rosser Proofs
title_sort On Complexity of Confluence and Church-Rosser Proofs
author_id_str_mv 1439ebd690110a50a797b7ec78cca600
author_id_fullname_str_mv 1439ebd690110a50a797b7ec78cca600_***_Arnold Beckmann
author Arnold Beckmann
author2 Arnold Beckmann
Georg Moser
format Conference Paper/Proceeding/Abstract
container_title Mathematical Foundations of Computer Science (MFCS)
institution Swansea University
doi_str_mv 10.4230/LIPIcs.MFCS.2024.21
college_str Faculty of Science and Engineering
hierarchytype
hierarchy_top_id facultyofscienceandengineering
hierarchy_top_title Faculty of Science and Engineering
hierarchy_parent_id facultyofscienceandengineering
hierarchy_parent_title Faculty of Science and Engineering
department_str School of Mathematics and Computer Science - Computer Science{{{_:::_}}}Faculty of Science and Engineering{{{_:::_}}}School of Mathematics and Computer Science - Computer Science
document_store_str 0
active_str 0
description 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.
published_date 0001-01-01T10:38:36Z
_version_ 1809167224614682624
score 11.028798

Similar Items