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

• 的場 正樹

  東北大学大学院情報科学研究科 現在，富士通ネットワークソリューションズ株式会社

• 青戸 等人

  東北大学電気通信研究所

• 外山 芳人

  東北大学電気通信研究所

書誌事項

タイトル別名

• Commutativity of Term Rewriting Systems based on One Side Decreasing Diagrams

抄録

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.

収録刊行物

• コンピュータ ソフトウェア

  コンピュータ ソフトウェア 30 (1), 1_187-1_202, 2013

  日本ソフトウェア科学会

詳細情報

• CRID: 1390282679713335168
• NII論文ID: 130004549310
• DOI: 10.11309/jssst.30.1_187
• ISSN: 02896540
• 本文言語コード: ja
• データソース種別:
  • JaLC
  • CiNii Articles
  • KAKEN
• 抄録ライセンスフラグ: 使用不可