Generation of equivalent transformation rules from a set of definite clauses by using meat-rules

摘要

In the "equivalent transformation (ET)" model, computation is regarded as equivalent transformation of declarative descriptions (e.g., a set of definite clauses) by a number of equivalent transformation rules. This paper proposes a method for generating ET rules that can transform a set of definite clauses equivalently. A new concept of meta-descriptions, each of which represents infinite descriptions by instantiation, is introduced. Meta descriptions are transformed equivalently by means of meta-rules to generate ET rules. An ET rule is obtained from each pair of meta-descriptions that are equivalent. One of the most important characteristics of the proposed method is modularity. A meta-rule is modular in the sense that its correctness can be judged independently of other meta-rules. Meta-rules can be applied in any order, while the folding rule in logic programming cannot.