Computational Properties of Term Rewriting with Replacement Restrictions.
Salvador Lucas · APPIA-GULP-PRODE · 1997
\'Ve give a general formulation of the notion of replacement restriction, a concepl which induces a restricted rewrite relation on a term rewriting system. Being a very general concept, we imroduce and motivate properties which can be used to characterize some important families of replacement rest rictions. We show how to approximate the lattice of replacement restrictions by the fini te lattice of contextsensitive replacement restrictions . This allows us to eventually lift existing results on computational properties (termination , completeness, ... ) of context-sensitive rewriting to non-trivial approximations of different classes of restricted rewriting. We also give useful results on confluence for restricted rewriting as an easy generalization of well-known results for unrestTicted term rewriting.