Confluent term rewriting systems

Yoshihito Toyama

Research output: Contribution to journalConference articlepeer-review

6 Citations (Scopus)


The confluence property is one of the most important properties of term rewriting systems, and various sufficient criteria for proving this property have been widely investigated. A necessary and sufficient criterion for confluence of terminating term rewriting systems, in which every reduction must terminate, was demonstrated by Knuth and Bendix (1970). For non-terminating term rewriting systems, Rosen (1973) proved that left-linear and non-overlapping term rewriting systems (i.e., no variable occurs twice or more in the left-hand side of a rewriting rule and two left-hand sides of rewriting rules must not overlap) are confluent, and the non-overlapping limitation was somewhat relaxed by Huet (1980), Toyama (1988), and van Oostrom (1997). However, few criteria have been proposed for confluence of term rewriting systems that are nonleft-linear and non-terminating. Thus, it is still worth while extending criteria for these systems. A powerful technique for showing confluence of a non-left-linear non-terminating term rewriting system is a divide-and-conquer method based on modularity by Toyama (1987) or persistency by Zantema (1994), Aoto and Toyama (1997). The method guarantees that if the system is decomposed into small subsystems and each of them is confluent then this system has the confluence property. Another useful technique is a transformational method based on conditional-linearization by Klop and de Vrijer (1991), Toyama and Oyamaguchi (1994), or a labelling technique. In this method we apply a non-confluence preserving transformation on a term rewriting system. Then the term rewriting system is confluent if the transformed system is confluent, because of non-confluence preserving. In this talk we will illustrate these techniques through various examples and discuss the relation among them.

Original languageEnglish
Number of pages1
JournalLecture Notes in Computer Science
Publication statusPublished - 2005
Event16th International Conference on Term Rewriting and Applications, RTA 2005 - Nara, Japan
Duration: 2005 Apr 192005 Apr 21

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Confluent term rewriting systems'. Together they form a unique fingerprint.

Cite this