Transforming Inductive Definitions
Danny De Schreye · 1999
The main goal of this paper is to provide a common foundation to the theories of correctness of program transformations for a large variety of programming languages. We consider the notion of rule set and the notion of inductive set which is defined by a rule set. We also consider a class of transformations of rule sets, called rule replacements, which replace an old rule set by a new rule set. These replacements can be viewed as generalizations of the most commonly used transformations, such as folding and unfolding. We study two methods for proving the correctness of rule replacements, that is, for showing that the old rule set and the new rule set define the same inductive set. These methods are: (i) the Unique Fixpoint Method, based on the well-foundedness property of the new rule set, and (ii) the Improvement Method, based on the fact that the premises of the old rule set are replaced by premises which have ‘smaller’ proofs w.r.t. a suitable well-founded relation. Our Unique Fixpoint and Improvement Methods generalize many methods described in the literature which deal with transformation rules for functional and logic programming languages. Our methods have also the advantages of: (i) being parametric w.r.t. the well-founded relation which is actually used, and (ii) being applicable to rules with finite or infinite sets of premises