Church-Rosser Property and Unique Normal Form Property of Non-Duplicating Term Rewriting Systems(Theory of Rewriting Systems and Its Applications)
Yoshihito Toyama, Michio Oyamaguchi · Institutional Repositories DataBase (IRDB) · 1995
We propose a new type of conditional term rewriting systems: lefl-z2 $gh\mathrm{f}$ separated condi- tional term rewriting systems, in which the left-hand side and the right-hand side of a rewrite rule have separate variables.By developing a concept of weight decreasing joinability we first present a sufficient condition for the Church-Rosser property of left-right separated conditional term rewriting systems which may have overlapping rewrite rules.We next apply this result to show sufficient conditions for the unique normal form property and the Church-Rosser prop- erty of unconditional term rewriting systems which are non-duplicating, non-left-linear, and overlapping.