The Marriage of Effects and Rewrites

In the research on computational effects, defined algebraically, effect symbols are often expected to obey certain equations. If we orient these equations, we get a rewrite system, which may be an effective way of transforming or optimizing the effects in a program. In order to do so, we need to establish strong normalization, or termination, of the rewrite system. Here we define a framework for carrying out such proofs, and extend the well-known Recursive Path Ordering of Dershowitz to show termination of some effect systems.