Sonic Partial Deduction

Abstract

The current state of the art for ensuring finite unfolding of logic programs consists of a number of online techniques where unfolding decisions are made at specialisation time. Introduction of a static termination analysis phase into a partial deduction algorithm permits unfolding decisions to be made offline, before the actual specialisation phase itself. This separation improves specialisation time and facilitates the automatic construction of compilers and compiler generators. The main contribution of this paper is how this separation may be achieved in the context of logic programming, while providing non-trivial support for partially static datastructures.

The paper establishes a solid link between the fields of static termination analysis and partial deduction enabling existing termination analyses to be used to ensure finiteness of the unfolding process. This is the first offline technique which allows arbitrarily partially instantiated goals to be sufficiently unfolded to achieve good specialisation results. Furthermore, it is demonstrated that an offline technique such as this one can be implemented very efficiently and, surprisingly, yield even better specialisation than a (pure) online technique. It is also, to our knowledge, the first offline approach which passes the KMP test (i.e., obtaining an efficient Knuth-Morris-Pratt pattern matcher by specialising a naive one).