Skip to main content

Ensuring Global Termination of Partial Deduction while Allowing Flexible Polyvariance

Bern Martens, John Gallagher, Ensuring Global Termination of Partial Deduction while Allowing Flexible Polyvariance. CSTR-94-016, Department of Computer Science, University of Bristol. December 1994. PDF, 234 Kbytes.


The control of polyvariance is a key issue in partial deduction of logic programs. Certainly, only finitely many specialised versions of any procedure should be generated, while, on the other hand, overly severe limitations should not be imposed. In this paper, well-founded orderings serve as a starting point for tackling this so-called ``global termination'' problem. Polyvariance is determined by the set of distinct ``partially deduced'' atoms generated during partial deduction. Avoiding ad-hoc techniques, we formulate a quite general framework where this set is represented as a tree structure. Associating weights with nodes, we define a well-founded order among such structures, thus obtaining a foundation for certified global termination of partial deduction. We include an algorithm template, concrete instances of which can be used in actual implementations, prove termination and correctness, and report on the results of some experiments. Finally, we conjecture that the proposed framework can support further advances towards (fully automatic) optimal program specialisation.

Bibtex entry.

Publication Admin