Rewriting modulo a rewrite system
We introduce rewriting with two sets of rules, the first interpreted
equationally and the second not. A
semantic view considers equational rules as defining an equational theory
and reduction rules as defining
a rewrite relation modulo this theory. An operational view considers both
sets of rules as similar. We
introduce sufficient properties for these two views to be equivalent (up to
different notions of
equivalence). The paper ends with a collection of example showing the
effectiveness of this approach.