Term rewriting systems and the Church-Rosser property

Our research concerns term rewriting systems having the Church-Rosser property. First, we develop modular aspects for term rewriting systems for systematic analysis of the behavior of combined term rewriting systems. The main outcome of this research is establishment of the modularity of the Church-Rosser property, which is very helpful for dealing with complex term rewriting systems. We also develop a simple method for proving the equivalence of two given term rewriting systems without the explicit use of induction, and demonstrate that the method can be effectively applied to deriving a new term rewriting system from a given one by using equivalence transformation rules. Finally, the Church-Rosser property of a new type of conditional term rewriting systems is investigated.

我们的研究涉及具有丘奇 - 罗瑟性质的项重写系统。首先，我们为项重写系统开发模块化方面的内容，以便对组合项重写系统的行为进行系统分析。这项研究的主要成果是确立了丘奇 - 罗瑟性质的模块性，这对处理复杂的项重写系统非常有帮助。我们还开发了一种简单的方法，用于在不明确使用归纳法的情况下证明两个给定项重写系统的等价性，并证明该方法可通过使用等价变换规则有效地应用于从给定的项重写系统推导出一个新的项重写系统。最后，对一种新型的条件项重写系统的丘奇 - 罗瑟性质进行了研究。