Skip to main content

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)

PDF - Author's Accepted Manuscript

Creative Commons Licence
This work is licensed under a Creative Commons Attribution 4.0 International License.
Download (268kB) Preview Download (268kB)
Official URL


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

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

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

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

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: Faculties > Sciences > School of Computing > Programming Languages and Systems Group
Depositing User: Stefan Kahrs
Date Deposited: 10 May 2016 11:06 UTC
Last Modified: 30 Jan 2020 16:19 UTC
Resource URI: (The current URI for this page, for reference purposes)
  • Depositors only (login required):


Downloads per month over past year