We show how confluence criteria based on decreasing diagrams are generalized to ones composable with other criteria. For demonstration of the method, the confluence criteria of orthogonality, rule labeling, and critical pair systems for term rewriting are recast into composable forms. We also show how such a criterion can be used for a reduction method that removes rewrite rules unnecessary for confluence analysis. In addition to them, we prove that Toyama's parallel closedness result based on parallel critical pairs subsumes his almost parallel closedness theorem.
翻译:我们展示了如何基于递减图的合流准则被推广为可与其他准则组合的形式。为演示该方法,我们将术语重写中的正交性、规则标记和临界对系统的合流准则重构为可组合形式。我们还展示了此类准则如何用于一种归约方法,该方法可移除对合流分析不必要的重写规则。此外,我们证明了基于平行临界对的Toyama平行封闭性结果蕴含了他的近乎平行封闭性定理。