The Church-Rosser property for ground term-rewriting systems is decidable
type: Item
instance of: scholarly article
title: The Church-Rosser property for ground term-rewriting systems is decidable
zbMATH Open document ID: 0641.68044
DOI: 10.1016/0304-3975(87)90100-9
author: Michio Oyamaguchi
published in: Theoretical Computer Science
publication date: 1987-01-01T00:00:00Z
review text: The paper proves the decidabilty of the Church-Rosser property (i.e. confluency) for any ground term-rewriting system (i.e. term rewriting system with rules not containing any variables), even if the system is not noetherian (i.e. it may contain infinite chains of reductions). While the noetherian property has been known to be decidable for ground term- rewriting systems, the problem solved in this paper has been an open problem for several years. Several technical notions are introduced for the purpose of the proof: For the analysis of reduction sequences, pattern trees and stable pattern trees are defined and their properties studied. A restricted notion of confluency, the k-restricted confluency, is considered, for which it is shown that the confluency problem can be reduced to the k-restricted confluency problem for some \(k>0\). The proof of the decidability of the confluency problem for ground term-rewriting systems is concluded by reducing k-restricted confluency to the equivalence problem for nondeterministic root-to-root automata (already shown to be decidable by Thatcher).
Mathematics Subject Classification ID: 68Q65
Mathematics Subject Classification ID: 20M05
Mathematics Subject Classification ID: 68Q45
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 08A50
Mathematics Subject Classification ID: 20M35
zbMATH DE Number: 4045128
zbMATH Keywords: root-to-frontier automata
zbMATH Keywords: decidabilty
zbMATH Keywords: Church-Rosser property
zbMATH Keywords: confluency
zbMATH Keywords: ground term-rewriting system
zbMATH Keywords: nondeterministic root-to-root automata
reviewed by: Jiří Zlatuška
MaRDI profile type: Publication
full work available at URL: 0304-3975(87)90100-9
OpenAlex ID: W2036985061
cites work: Q3917482
cites work: Proving termination with multiset orderings
cites work: On Proving Uniform Termination and Restricted Termination of Rewriting Systems
cites work: Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
cites work: Q5581665
cites work: Fast Decision Procedures Based on Congruence Closure
cites work: Q3706484
cites work: Tree-Manipulating Systems and Church-Rosser Theorems
description: scientific article; zbMATH DE number 4045128