Commutativity of term rewriting systems based on one side decreasing diagrams

Masaki Matoba, Takahito Aoto, Yoshihito Toyama

Research output: Contribution to journalArticlepeer-review

Abstract

Commutativity is a generalization of confluence. Furthermore, decompositions of term rewriting systems based on the commutativity is useful to prove confluence of term rewriting systems. Several methods for showing commutativity of term rewriting systems are known, where all of them are based on conditions imposed from critical pairs analysis. Apart from this, a sufficient condition of commutativity based on decreasing diagrams has been studied in the framework of abstract rewriting. Decreasing diagrams, however, have not been applied for proving commutativity of term rewriting systems. In this paper, we introduce one side decreasing diagrams, and give a method to prove commutativity of term rewriting systems based on one side decreasing diagrams.

Original languageEnglish
Pages (from-to)187-202
Number of pages16
JournalComputer Software
Volume30
Issue number1
Publication statusPublished - 2013 Feb 1

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Commutativity of term rewriting systems based on one side decreasing diagrams'. Together they form a unique fingerprint.

Cite this