Fundamental properties of rewriting systems and evaluation strategy of functional programs

Church-Rosser（CR）是项重写系统（TRS）的一个重要性质。在TRS是线性的或有限终止的假设下，已经得到了许多充分条件。另一方面，对于非线性和非终止TRS的，很少有结果的CR性质已经得到。最近，我们提出了两种新的方法，即E图方法和条件线性化方法，并得到了非线性和非终止TRS的CR的一些新的充分条件。我们首先证明了非E-重叠和非Ω-重叠都是右接地TRS的CR的可判定的充分条件。其次，我们证明了非E-重叠也是简单右线性TRS的CR的一个充分条件，它适当地包括了右接地TRS的类。此外，我们还考虑了E-重叠TRS的CR性质，并在对E-临界对分析的基础上，成功地得到了CR的一些充分条件。通过引入序列可正规化的概念，将E-图和条件线性化的E-图进行了推广。利用这种统一的方法，我们得到了CR的一些充分条件，这些条件是以前条件的推广。此外，我们还研究了非简单右线性TRS的CR性质，证明了非E-重叠是强保深TRS类CR的充分条件，从而完全实现了我们所提出的TRS的CR性质。本课题还对TRS的约简策略和功能程序的有效实现进行了基础性研究，取得了一些新的成果。

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.