Automating Confluence Check of Term Rewriting Systems

• YOSHIDA Junichi

  RIEC, Tohoku University

• AOTO Takahito

  RIEC, Tohoku University

• TOYAMA Yoshihito

  RIEC, Tohoku University

Bibliographic Information

Other Title

• 項書き換えシステムの合流性自動判定
• コウ カキカエ システム ノ ゴウリュウセイ ジドウ ハンテイ

Abstract

We propose an automated confluence checker for term rewriting systems (TRSs) that combines several criteria for proving the confluence property of TRSs. For a TRS to which none of confluence criteria directly applies, our checker automatically decomposes it into small components using direct sum decomposition and commutative decomposition, and applies the confluence criteria to each component so that the confluence of the whole system is checked by combining these results. For the best of our knowledge, an automated confluence checker based on such an approach has been unknown. We have implemented our checker, and have successfully applied our checker to automatically check the confluence of a complex TRS, to which none of known confluence criteria applies directly. We also construct a collection of sample TRSs mainly extracted from papers on confluence of TRSs and perform an experiment to this collection.

Journal

• Computer Software

  Computer Software 26 (2), 76-92, 2009

  Japan Society for Software Science and Technology

Details

• CRID: 1390282679713201536
• NII Article ID: 10025982412
• NII Book ID: AN10075819
• DOI: 10.11309/jssst.26.2_76
• NDL BIB ID: 10290066
• ISSN: 02896540
• Web Site: http://id.ndl.go.jp/bib/10290066
• Web Site: https://ndlsearch.ndl.go.jp/books/R000000004-I10290066
• Data Source:
  • JaLC
  • NDL
  • CiNii Articles
  • KAKEN
• Abstract License Flag: Disallowed