Conditions for confluence of innermost terminating term rewriting systems

This paper presents a counterexample for the open conjecture whether innermost joinability of all critical pairs ensures confluence of innermost terminating term rewriting systems. We then show that innermost joinability of all normalized instances of the critical pairs is a necessary and sufficient...

Full description

Saved in:
Bibliographic Details
Published in:Applicable algebra in engineering, communication and computing communication and computing, 2019-08, Vol.30 (4), p.349-360
Main Authors: Ishizuki, Sayaka, Oyamaguchi, Michio, Sakai, Masahiko
Format: Article
Language:English
Subjects:
Artificial Intelligence
Computer Hardware
Computer Science
Original Paper
Symbolic and Algebraic Manipulation
Theory of Computation
Citations: Items that this one cites
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:This paper presents a counterexample for the open conjecture whether innermost joinability of all critical pairs ensures confluence of innermost terminating term rewriting systems. We then show that innermost joinability of all normalized instances of the critical pairs is a necessary and sufficient condition. Using this condition, we give a decidable sufficient condition for confluence of innermost terminating systems. Finally, we enrich the condition by introducing the notion of left-stable rules. As a corollary, confluence of innermost terminating left-weakly-shallow TRSs is shown to be decidable.
ISSN:0938-1279
1432-0622
DOI:10.1007/s00200-018-0377-8