Commutativity of Term Rewriting Systems based on One Side Decreasing Diagrams

• MATOBA Masaki

  Graduate School of Information Sciences, Tohoku University presently with Fujitsu Network Solutions Limited

• AOTO Takahito

  RIEC, Tohoku University

• TOYAMA Yoshihito

  RIEC, Tohoku University

Bibliographic Information

Other Title

• 片側減少ダイアグラム法による項書き換えシステムの可換性証明法

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.

Journal

• Computer Software

  Computer Software 30 (1), 1_187-1_202, 2013

  Japan Society for Software Science and Technology

Details

• CRID: 1390282679713335168
• NII Article ID: 130004549310
• DOI: 10.11309/jssst.30.1_187
• ISSN: 02896540
• Text Lang: ja
• Data Source:
  • JaLC
  • CiNii Articles
  • KAKEN
• Abstract License Flag: Disallowed