A reduction-preserving completion for proving confluence of non-terminating term rewriting systems

Takahito Aoto, Yoshihito Toyama

研究成果: Article査読

12 被引用数 (Scopus)

抄録

We give a method to prove con uence of term rewriting systems that contain non-terminating rewrite rules such as commutativity and associativity. Usually, con uence of term rewriting systems containing such rules is proved by treating them as equational term rewriting systems and considering E-critical pairs and/or termination modulo E. In contrast, our method is based solely on usual critical pairs and it also (partially) works even if the system is not terminating modulo E. We first present con uence criteria for term rewriting systems whose rewrite rules can be partitioned into a terminating part and a possibly non-terminating part. We then give a reduction-preserving completion procedure so that the applicability of the criteria is enhanced. In contrast to the well-known Knuth- Bendix completion procedure which preserves the equivalence relation of the system, our completion procedure preserves the reduction relation of the system, by which con uence of the original system is inferred from that of the completed system.

本文言語English
ジャーナルLogical Methods in Computer Science
8
1
DOI
出版ステータスPublished - 2012

ASJC Scopus subject areas

  • 理論的コンピュータサイエンス
  • コンピュータ サイエンス(全般)

フィンガープリント

「A reduction-preserving completion for proving confluence of non-terminating term rewriting systems」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル