[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |
Originator: Vincent van Oostrom
Date: June 1993
Summary: Is the union of two left-linear, confluent combinatory reduction systems over the same alphabet, where the rules of the first system do not overlap the rules of the second, confluent?
Let R and S be two left-linear, confluent combinatory reduction systems with the same alphabet. Suppose the rules of R do not overlap the rules of S. Is R ∪ S confluent? This is true for the restricted case when R is a term-rewriting system (an easy generalization of a result by F. Müller [Mül92]), or if neither system has critical pairs. (The restriction to the same alphabet is essential, since confluence is in general not preserved under the addition of function symbols, not even for left-linear systems.)
The answer is yes (Thm. 3.1 of [vOvR94]).
[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |