Smith, Connor and Kahrs, Stefan (2016) Non-omega-overlapping TRSs are UN. In: Formal Structures for Computation and Deduction, 22-26 Jun 2016, Porto, Portugal. (doi:https://doi.org/10.4230/LIPIcs.FSCD.2016.22) (Full text available)

PDF - Author's Accepted Manuscript

 Preview
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 --- 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 $\invariant$ that is consistent by construction, and which --- if transitive --- would coincide with the rewrite system's equivalence relation. We then prove the transitivity of $\invariant$ 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 $\invariant$.

Item Type: Conference or workshop item (Paper) term rewriting, functional programming, consistency Q ScienceQ Science > QA Mathematics (inc Computing science)Q Science > QA Mathematics (inc Computing science) > QA 9 Formal systems, logics Faculties > Sciences > School of Computing > Programming Languages and Systems Group Stefan Kahrs 10 May 2016 11:06 UTC 11 Sep 2017 08:37 UTC https://kar.kent.ac.uk/id/eprint/55349 (The current URI for this page, for reference purposes)