| Research Abstract |
Church-Rosser (CR) is an important property of term rewriting systems (TRS). Many sufficient conditions for this property have been obtained under the assumption that TRS's are linear or finite-terminating. On the other hand, for nonlinear and nonterminating TRS's, few results on the CR property have been obtained. Recently, we proposed two new approaches called the E-graph and conditional linearization ones, and obtained some new sufficient conditions for CR of nonlinear and nonterminating TRS's.
The purpose of this research is to develop our previous researches further. We have first shown that both non-E-overlapping and non-omega-overlapping are decidable and sufficient conditions for CR of right-ground TRS's. Next, we have shown that non-E-overlapping is also a sufficient condition for CR of simple-right-linear TRS's which properly include the class of right-ground TRS's. Moreover, we have considered the CR property of E-over-lapping TRS's and succeeded in obtaining some sufficient conditions for CR based on the analysis of the E-critical pairs.
In this research we have also succeeded in unifying the two different approached, i.e., the E-graph and conditional linearization ones by introducing the notion of sequence-normalizability. Using this unified approach we have obtained some sufficient conditions for CR which are a generalization of the previous ones. Furthermore, we have considered the CR property of non-simple-right-linear TRS's and showed that non-E-overlapping is a sufficient condition for CR of the class of strongly depth-preserving TRS's.
By the above results obtained by this research, our proposed plan for the CR property of TRS's has completely been achieved. This research project has also made a basic research in the reduction strategy of TRS's and an efficient implementation of functional programs, and obtained some new results.
|
