On the Open Problems Concerning Church-Rosser of Left-Linear Term Rewriting Systems(<Special Section>Foundations of Computer Science)
スポンサーリンク
概要
- 論文の詳細を見る
G. Huet (1980) showed that a left-linear term-rewriting system (TRS) is Church-Rosser (CR) if P 〓 Q for every critical pair <P, Q> where P 〓 Q is a parallel reduction from P to Q. But, it remains open whether it is CR when Q 〓 P for every critical pair <P, Q>. In this paper, we give a partial solution to this problem, that is, a left-linear TRS is CR if Q 〓^^W P for every critical pair <P, Q> where Q 〓^^W P is a parallel reduction with the set W of redex occurrences satisfying that if the critical pair is generated from two rules overlapping at an occurrence u, then the length |w| ≤ |u| for every w ∈ W. We also show that a left-linear TRS is CR if Q →^^<≯u>__= P for every critical pair <P, Q> generated from two rules overlapping at an occurrence u. Here, Q →^^<≯u>__= P is either Q = P or a reduction whose redex occurrence is not greater than u. This condition is incomparable with the previous one and a partial solution to the open problem of ascertaining whether it is CR when Q →__= P for every critical pair <P, Q>.
- 社団法人電子情報通信学会の論文
- 2004-02-01
著者
-
Ohta Yoshikatsu
Faculty Of Engineering Mie University
-
Oyamaguchi Michio
Faculty Of Engineering Mie University
関連論文
- The Joinability and Related Decision Problems for Semi-constructor TRSs(計算理論)
- Some Results on the CR property of non-E-overlapping and depth-preserving TRS's(Theory of Rewriting Systems and Its Applications)
- On the Church-Rosser Property of Root-E-overlapping and Strogly Depth-preserving Term Rewriting Systems(Special Issue on Generation Database Technology for Internet, Multimedia and Mobile computing)
- On the Church-Rosser Property of Non-E-overlapping and Strongly Depth-preserving Term Rewriting Systems
- Church-Rosser Property and Unique Normal Form Property of Non-Duplicating Term Rewriting Systems(Theory of Rewriting Systems and Its Applications)
- The Reachability and Joinability Problems for Right-Ground Term-Rewriting Systems
- The Reachability Problem for Quasi-Ground Term Rewriting Systems
- On the Open Problems Concerning Church-Rosser of Left-Linear Term Rewriting Systems(Foundations of Computer Science)
- On the Task Scheduling with Communication Delay
- On the Church-Rosser Property of Left-Linear Term Rewriting Systems(Regular Section)
- The Joinability and Related Decision Problems for Semi-constructor TRSs
- The Joinability and Related Decision Problems for Semi-constructor TRSs