The Marriage of Effects and Rewrites

TL;DR

This paper introduces a framework for proving the termination of rewrite systems in computational effects, extending Recursive Path Ordering to ensure effect system normalization.

Contribution

It develops a new method for establishing strong normalization of effect rewrite systems by extending Recursive Path Ordering.

Findings

Extended Recursive Path Ordering to effect systems

Proved termination for certain effect rewrite systems

Framework facilitates effect optimization in programming languages

Abstract

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.