No Cover Image

Conference Paper/Proceeding/Abstract 120 views

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

Full text not available from this repository: check for access using links below.

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
first_indexed 2024-09-03T09:38:36Z
last_indexed 2024-11-25T14:20:23Z
id cronfa67544
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2024-10-10T11:09:52.5476626</datestamp><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 &#x3BB;-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 &#x3BB;-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>306</volume><journalNumber/><paginationStart/><paginationEnd/><publisher>Schloss Dagstuhl &#x2013; Leibniz-Zentrum f&#xFC;r Informatik</publisher><placeOfPublication/><isbnPrint/><isbnElectronic>978-3-95977-335-5</isbnElectronic><issnPrint/><issnElectronic>1868-8969</issnElectronic><keywords>logic, bounded arithmetic, consistency, rewriting</keywords><publishedDay>23</publishedDay><publishedMonth>8</publishedMonth><publishedYear>2024</publishedYear><publishedDate>2024-08-23</publishedDate><doi>10.4230/LIPIcs.MFCS.2024.21</doi><url>https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2024.21</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-10-10T11:09:52.5476626</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><document><filename>67544__31248__56e005fcd17840718deaf52c309284ce.pdf</filename><originalFilename>67544.pdf</originalFilename><uploaded>2024-09-03T10:38:25.7252052</uploaded><type>Output</type><contentLength>1819889</contentLength><contentType>application/pdf</contentType><version>Version of Record</version><cronfaStatus>true</cronfaStatus><documentNotes>&#xA9; Arnold Beckmann and Georg Moser. Licensed under Creative Commons License CC-BY 4.0.</documentNotes><copyrightCorrect>true</copyrightCorrect><language>eng</language><licence>https://creativecommons.org/licenses/by/4.0/</licence></document></documents><OutputDurs/></rfc1807>
spelling 2024-10-10T11:09:52.5476626 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) 306 Schloss Dagstuhl – Leibniz-Zentrum für Informatik 978-3-95977-335-5 1868-8969 logic, bounded arithmetic, consistency, rewriting 23 8 2024 2024-08-23 10.4230/LIPIcs.MFCS.2024.21 https://drops.dagstuhl.de/entities/document/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-10-10T11:09:52.5476626 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 67544__31248__56e005fcd17840718deaf52c309284ce.pdf 67544.pdf 2024-09-03T10:38:25.7252052 Output 1819889 application/pdf Version of Record true © Arnold Beckmann and Georg Moser. Licensed under Creative Commons License CC-BY 4.0. true eng https://creativecommons.org/licenses/by/4.0/
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)
container_volume 306
publishDate 2024
institution Swansea University
isbn 978-3-95977-335-5
issn 1868-8969
doi_str_mv 10.4230/LIPIcs.MFCS.2024.21
publisher Schloss Dagstuhl – Leibniz-Zentrum für Informatik
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
url https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2024.21
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 2024-08-23T08:34:02Z
_version_ 1821393753352437760
score 11.087994

Similar Items