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适当地包含了右地TRS的类别。此外，我们考虑了e -重叠TRS的CR性质，并通过对e -临界对的分析，成功地获得了CR的一些充分条件。在本研究中，我们还通过引入序列归一化的概念，成功地统一了两种不同的方法，即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.