Termination of Algebraic Rewriting with Inhibitors

Abstract

We proceed with the study of termination properties in the double pushout approach to algebraic rewriting, and show a concrete termination criterion for rewriting systems with inhibitors. Inhibitors prevent elements in an algebra to participate in rule matches, so that termination depends only on whether new possibilities for matches are created. The notion of inhibitor can be extended to considering different levels of inhibition, by which the ability of an element to participate in a match is progressively reduced. We illustrate the approach by considering some application contexts in model transformation.