[Submit a comment] [RTALooP home] [Index] [Previous] [Next] [Postscript] [PDF] [BibTeX Source] [LaTeX Source]

Problem #16

Originator: Yoshihito Toyama
Date: April 1991

Summary: Under what conditions does confluence of a normal semi-equational conditional term rewriting system imply confluence of the associated oriented system?

For a normal conditional term-rewriting system R = { s →! t ⇒ l → r }, where t must be a ground normal from of s, we can consider the corresponding semi-equational conditional rewrite system Rse = { s ↔* t ⇒ l → r }. Under what conditions does confluence of Rse imply confluence of R? In general, this is not the case, as can be seen from the following non-confluent system R (due to Aart Middeldorp):

a → b
a → c
b →! c ⇒    b → c

Remark

Solutions have been provided by [YASM00]. They show that confluence of R follows from confluence of Rse if any of the two following conditions is satisfied:

See [YASM00] for definitions of these properties.

References

[YASM00]
Toshiyuki Yamada, Jürgen Avenhaus, Carlos Loría Sáenz, and Aart Middeldorp. Logicality of conditional rewrite systems. Theoretical Computer Science, 236(1–2):209–232, April 2000.

[Submit a comment] [RTALooP home] [Index] [Previous] [Next] [Postscript] [PDF] [BibTeX Source] [LaTeX Source]