正/负条件项重写系统的句法合流准则
Syntactic Confluence Criteria for Positive/Negative-Conditional Term Rewriting Systems
摘要：
我们研究了以下已知的用于将无条件或条件项重写系统的汇合显示为条件系统的实际上更有用的汇合标准的想法的组合：我们的构造符和非构造符的语法分离，Huet的介绍和Toyama对非Noether无条件系统的平行闭性的推广，使用浅汇合来证明诺特条件系统和非诺特条件系统的汇合，可以假设某些类型的有限汇合来检查条件临界对的条件的满足性或不可行性的想法，以及（当给出终止时）仅必须考虑素叠加并且可以对满足条件临界对的条件的替换应用某些归一化限制的思想。除了结合和改进已知的方法，我们提出了以下新的想法和结果：我们加强了覆盖可连接的诺特系统的标准，并且，通过使用我们的句法分离为构造器和非构造器符号的表达力，我们可以提出水平汇流的标准，而不是实际上的浅汇流标准，也可以削弱严格的正态性要求（加强左线性）的Noether和非Noether条件系统的浅汇合准则的拟正规性容易满足的要求。最后，本文也给出了一个实用的概述的语法手段，显示合流的条件项重写系统。
英文摘要：
We study the combination of the following already known ideas for showing confluence of unconditional or conditional term rewriting systems into practically more useful confluence criteria for conditional systems: Our syntactical separation into constructor and non-constructor symbols, Huet's introduction and Toyama's generalization of parallel closedness for non-noetherian unconditional systems, the use of shallow confluence for proving confluence of noetherian and non-noetherian conditional systems, the idea that certain kinds of limited confluence can be assumed for checking the fulfilledness or infeasibility of the conditions of conditional critical pairs, and the idea that (when termination is given) only prime superpositions have to be considered and certain normalization restrictions can be applied for the substitutions fulfilling the conditions of conditional critical pairs. Besides combining and improving already known methods, we present the following new ideas and results: We strengthen the criterion for overlay joinable noetherian systems, and, by using the expressiveness of our syntactical separation into constructor and non-constructor symbols, we are able to present criteria for level confluence that are not criteria for shallow confluence actually and also able to weaken the severe requirement of normality (stiffened with left-linearity) in the criteria for shallow confluence of noetherian and non-noetherian conditional systems to the easily satisfied requirement of quasi-normality. Finally, the whole paper may also give a practically useful overview of the syntactical means for showing confluence of conditional term rewriting systems.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
