Regular Trees as an Abstract Domain for Program Specialisation

On-line partial evaluation algorithms include a generalisation step, which is needed to ensure termination. In partial evaluation of logic and functional programs, the usual generalisation operation is the most specific generalisation (\it msg) of expressions. This can cause loss of information, which is especially serious in programs whose computations first build some internal data structure, which is then used to control a subsequent phase of execution - a common pattern of computation. If the size of the intermediate data is unbounded at partial evaluation time then the \it msg will lose almost all information about its structure. Hence subsequent phases of computation cannot be effectively specialised. In this paper the problem is tackled by introducing regular trees into a partial evaluation algorithm. Regular trees are recursive descriptions of term structure closely related to tree automata. In the algorithm, regular approximations of computation states encountered during partial evaluation are constructed. The critical point is that when generalisation is performed, the upper bound on regular trees can be combined with the \it msg, thus preserving structural information including recursively defined structure. It also allows the specialisation of programs with respect to goals whose arguments range over sets described by regular trees. The algorithm is presented as an instance of Leuschel's scheme for abstract specialisation of logic programs. This provides a generic algorithm parameterised by an abstract domain - regular trees in this case. The correctness requirements from his scheme are established. The extension of the algorithm to propagate regular approximations of answers as well as calls is also presented, increasing the amount of specialisation that can be obtained. Finally a technique for increasing precision based on ``wrapper functions" is introduced.