A transformation system for definite programs based on termination analysis

Abstract

We present a goal replacement rule whose main applicability condition is based on termination properties of the resulting transformed program. The goal replacement rule together with a multi-step unfolding rule forms a powerful and elegant transformation system for definite programs. It also sheds new light on the relationship between folding and goal replacement, and between different folding rules. Our explicit termination condition contrasts with other transformation systems in the literature, which contain conditions on folding and goal replacement, often rather complex, in order to avoid “introducing a loop” into a program. We prove that the goal replacement rule preserves the success set of a definite program. We define an extended version of goal replacement that also preserves the finite failure set. A powerful folding rule can be constructed as a special case of goal replacement, allowing folding with recursive rules, with no distinction between old and new predicates. A proof that Seki's transformation system preserves recurrence, an important termination property, is outlined.