A framework for the analysis of syntactic replacement restrictions

Author

Salvador Lucas

Abstract

We formalize the notion of syntactic replacement restriction, which is useful for modeling reduction-based systems which compute with terms and impose restrictions on the possible computations (typically by means of strategies). We emphasize the syntactic flavour of our approach: the restrictions are associated to components of terms and (in principle) they do not depend on either a particular Term Rewriting System or a computational mechanism (like rewriting, narrowing, residuation, etc.). The replacement restrictions can be used to improve the computational behavior of the unrestricted mechanism. We give a general descriptive and algebraic framework to deal with replacement restrictions. For the descriptive part, we introduce and motivate properties which characterize classes of replacement restrictions. For the algebraic side, the set of replacement restrictions is presented as a complete Boolean algebra. The algebraic operations (and others which we also define) can be used to combine replacement restrictions. We use the ordering on the lattice of the Boolean algebra to approximate replacement restrictions by using small subsets of particular restrictions. The computational properties (termination, completeness, ...) of the restricted computations can be analyzed analyzed within this framework.

Keywords

declarative programming, reduction-based systems, replacement restrictions, term rewriting.