一句话:将基于递减图的合流性判据推广为可组合形式,并给出消去无关重写规则的约简方法。
本文研究项重写系统中合流性判据的组合问题。作者把基于递减图(decreasing diagrams)的合流性判据推广为可与其他判据组合的形式,使不同判据可以在同一证明中协同使用。为展示该框架,他们将正交性、规则标记(rule labeling)和临界对系统(critical pair systems)这三类经典判据改写为可组合形式;并说明如何利用这种判据设计约简方法,删除对合流性分析不必要的重写规则。此外,作者证明基于并行临界对的 Toyama 并行封闭性结果蕴含其几乎并行封闭性定理。
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.