A term rewriting system (TRS) is said to be simple-right-linear if for any rewrite rule, the right-hand-side term is linear and no variables occuring more than once in the left-hand-side occur in the right-hand-side. This paper shows that a simple-right-linear TRS is Church-ROsser (i.e., confluent) if it satisfies the following condition (called the sequence-normalizing property) : for any reduction sequence γ : M ←→ N of length n, there exists a reduction sequence δ : M ←→ N of length ≤ n such that no E-overlapping sequences occur in δ. Next, some sufficient conditions for this sequence-normalizing property are presented and shown to be a generalization of those for Church-Rosser obtained by two different approaches proposed in [Oyamaguchi, 1992] and [Toyama-Oyamaguchi, 1993].
雑誌名
Research reports of the Faculty of Engineering, Mie University
On the Church-Rosser Property of E-overlapping and Simple-Right-Linear TRS's
AA008163410200010.PDF
(1.29MB)
