Non-omega-overlapping TRSs are UN

Smith, Connor Lane, Kahrs, Stefan (2016) Non-omega-overlapping TRSs are UN. In: 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). 2016 Formal Structures for Computation and Deduction. Leibniz International Proceedings in Informatics , 52. 22:1-22:17. Schloss Dagstuhl: Leibniz-Zentrum für Informatik, Porto, Portugal ISBN 978-3-95977-010-1. (doi:10.4230/LIPIcs.FSCD.2016.22) (KAR id:55349)

PDF Author's Accepted Manuscript Language: English This work is licensed under a Creative Commons Attribution 4.0 International License.
Download this file (PDF/526kB)	Preview
Request a format suitable for use with assistive technology e.g. a screenreader
Official URL: http://dx.doi.org/10.4230/LIPIcs.FSCD.2016.22

Abstract

This paper solves problem #79 of RTA’s list of open problems [14] — in the positive. If the

rules of a TRS do not overlap w.r.t. substitutions of infinite terms then the TRS has unique

normal forms. We solve the problem by reducing the problem to one of consistency for “similar”

constructor term rewriting systems. For this we introduce a new proof technique. We define a

relation ⇓ that is consistent by construction, and which — if transitive — would coincide with

the rewrite system’s equivalence relation =R.

We then prove the transitivity of ⇓ by coalgebraic reasoning. Any concrete proof for instances

of this relation only refers to terms of some finite coalgebra, and we then construct an equivalence

relation on that coalgebra which coincides with ⇓.

Item Type:	Conference or workshop item (Paper)
DOI/Identification number:	10.4230/LIPIcs.FSCD.2016.22
Uncontrolled keywords:	term rewriting, functional programming, consistency
Subjects:	Q Science Q Science > QA Mathematics (inc Computing science) Q Science > QA Mathematics (inc Computing science) > QA 9 Formal systems, logics
Divisions:	Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User:	Stefan Kahrs
Date Deposited:	10 May 2016 11:06 UTC
Last Modified:	05 Nov 2024 10:44 UTC
Resource URI:	https://kar.kent.ac.uk/id/eprint/55349 (The current URI for this page, for reference purposes)

University of Kent Author Information

Smith, Connor Lane.

Creator's ORCID:
CReDIT Contributor Roles:

Kahrs, Stefan.

Creator's ORCID:	https://orcid.org/0000-0001-5099-9375
CReDIT Contributor Roles:

Depositors only (login required):

Altmetric

Download Statistics

Total unique views for this document in KAR since July 2020. For more details click on the image.