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

Takahito Aoto, Yoshihito Toyama

Research output: Chapter in Book/Report/Conference proceedingConference contribution

4 Citations (Scopus)

Abstract

We give a method to prove confluence of term rewriting systems that contain non-terminating rewrite rules such as commutativity and associativity. Usually, confluence 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 usual termination. We first present confluence criteria for term rewriting systems whose rewrite rules can be partitioned into terminating part and 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 confluence of the original system is inferred from that of the completed system.

Original languageEnglish
Title of host publication22nd International Conference on Rewriting Techniques and Applications, RTA 2011
Pages91-106
Number of pages16
DOIs
Publication statusPublished - 2011 Dec 1
Event22nd International Conference on Rewriting Techniques and Applications, RTA 2011 - Novi Sad, Serbia
Duration: 2011 May 302011 Jun 1

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume10
ISSN (Print)1868-8969

Other

Other22nd International Conference on Rewriting Techniques and Applications, RTA 2011
CountrySerbia
CityNovi Sad
Period11/5/3011/6/1

Keywords

  • Completion
  • Confluence
  • Confluence modulo equations
  • Equational term rewriting systems

ASJC Scopus subject areas

  • Software

Cite this

Aoto, T., & Toyama, Y. (2011). A reduction-preserving completion for proving confluence of non-terminating term rewriting systems. In 22nd International Conference on Rewriting Techniques and Applications, RTA 2011 (pp. 91-106). (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 10). https://doi.org/10.4230/LIPIcs.RTA.2011.91