左线性重写系统的合流性

The Confluence of Left--linear Term Rewriting System

讨论左线性的项重写系统的合流性,通过引入重写系统的局部归约序,可证明对于具有局部归约序的左线性重写系统R,R具有合流性,当且仅当,对于任意M→R P和M→R Q,P和Q在M下相对局部归约序子连通。

This paper concerns the confluence of term rewriting system. By introducing the local reduction ordering of term rewriting system, a new sufficient condition for confluence of term rewriting system is given as follows: If R is a left-linear term rewriting system with local reduction ordering, then R is confluent iff for any M→P ang M→Q, P and Q are sub-connected under M w. r. t. the local reduction ordering.