Decreasing Diagrams for Confluence and Commutation

摘要

Like termination, confluence is a central property of rewrite systems. Unlikefor termination, however, there exists no known complexity hierarchy forconfluence. In this paper we investigate whether the decreasing diagramstechnique can be used to obtain such a hierarchy. The decreasing diagramstechnique is one of the strongest and most versatile methods for provingconfluence of abstract rewrite systems. It is complete for countable systems,and it has many well-known confluence criteria as corollaries. So what makes decreasing diagrams so powerful? In contrast to otherconfluence techniques, decreasing diagrams employ a labelling of the steps withlabels from a well-founded order in order to conclude confluence of theunderlying unlabelled relation. Hence it is natural to ask how the size of thelabel set influences the strength of the technique. In particular, what classof abstract rewrite systems can be proven confluent using decreasing diagramsrestricted to 1 label, 2 labels, 3 labels, and so on? Surprisingly, we findthat two labels suffice for proving confluence for every abstract rewritesystem having the cofinality property, thus in particular for every confluent,countable system. Secondly, we show that this result stands in sharp contrast to the situationfor commutation of rewrite relations, where the hierarchy does not collapse. Thirdly, investigating the possibility of a confluence hierarchy, wedetermine the first-order (non-)definability of the notion of confluence andrelated properties, using techniques from finite model theory. We find that inparticular Hanf's theorem is fruitful for elegant proofs of undefinability ofproperties of abstract rewrite systems.