Compositional Confluence Criteria

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. In addition to them, we prove that Toyama’s parallel closedness result based on parallel critical pairs subsumes his almost parallel closedness theorem. 2012 ACM Subject Classification Theory of computation → Equational logic and rewriting Acknowledgements We are grateful to Jean-Pierre Jouannaud, Vincent van Oostrom, and Yoshihito Toyama for their valuable comments on preliminary results of this work. We thank the reviewers for their thorough reading and suggestions, which helped us to improve the presentation.