论文部分内容阅读
We define here the concept of head boundedness,head normal form and head confluence of termrewriting systems that allow infinite derivations.Head confluence is weaker than confluence,but suffi-cient to guarantee the correctness of lazy implementations of equational logic programming languages.Then we prove several results.First,if a left-linear system is locally confluent and head-bounded,then itis head-confluent.Second,head-confluent and head-bounded systems have the head Church-Rosser proper-ty.Last,if an orthogonal system is head-terminating,then it is bead-bounded.These results can be ap-plied to generalize equational logic programming languages.
We define here the concept of head boundedness, head normal form and head confluence of termrewriting systems that allow infinite derivations.Head confluence is weaker than confluence, but suffi-cient to guarantee the correctness of lazy implementations of equational logic programming languages.Then we prove several results.First, if a left-linear system is locally confluent and head-bounded, then itis head-confluent.Second, head-confluent and head-bounded systems have the head Church-Rosser proper-ty.Last, if an orthogonal system is head-terminating, then it is bead-bounded. These results can be ap-plied to generalize equational logic programming languages.