Conditional Linearization of Non-Duplicating Term Rewriting Systems

概要

論文の詳細を見る
We propose a new conditional linearization based on left-right separated conditional 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. Applying this result to conditional linearization, we next show sufficient conditions for the unique normal form property and the Church-Rosser property of non-duplicating(unconditional)term rewriting systems even if they are non-left-linear or overlapping.
社団法人電子情報通信学会の論文
2001-04-01