PhD Information (Michael Leuschel)


This file contains more detailed information about the PhD of Michael Leuschel.

General Information

Title: Advanced Techniques for Logic Program Specialisation

Author: Michael Leuschel

Language of Presentation: English

Promotors: Prof. Dr. Danny De Schreye, Prof. Dr. Walter Van Assche

Date of defence: May 27, 1997

Institution granting degree: University of Leuven, Belgium


Program specialisation, also called partial evaluation or partial deduction, is an automatic technique for program optimisation. The central idea is to specialise a given source program for a particular application domain. Program specialisation encompasses traditional compiler optimisation techniques, but uses more aggressive transformations, yielding both much greater speedups and more difficulty in controlling the transformation process.

Because of their clear (and often simple) semantical foundations, declarative languages offer significant advantages for the design of semantics based program analysers, transformers and optimisers. This thesis exploits these advantages in the context of logic programming and develops advanced techniques for program specialisation, striving to produce tangible practical benefits within the larger objective of turning declarative languages and program specialisation into valuable tools for constructing reliable, maintainable and efficient programs.

This thesis contains contributions within that context around several themes. New, powerful methods for the control problem within partial deduction, based on characteristic trees, are developed. A method for automatic compiler generation, which does not have to resort to self-applicable specialisers, is presented. A practical and very successful application in the area of integrity checking in deductive databases is worked out. Finally, an integration of "unfold/fold" transformations with partial deduction, as well as a further integration with abstract interpretation, are developed.

More precisely, part of the thesis attends to the control of polyvariance problem and illustrates the advantages of characteristic trees over a purely syntactic approach. Thereafter the thesis proceeds to solve the intricate problems - in terms of precision, termination and ad-hoc depth bounds - that have ridden existing approaches based on characteristic trees. A framework, called ecological partial deduction, is developed, whose correctness, in the context of normal logic programs, is formally proven. Based on this framework, the thesis presents concrete algorithms, whose correctness and termination are established. An implementation is used to conduct extensive experiments and validate the practical usefulness of the approach.

Another part of the thesis concentrates on the issue of self-application, an elegant concept allowing e.g. to automatically build compilers and compiler generators from interpreters. Despite its promises however, self-application has up to now not been very successful for logic programming languages. This thesis overcomes that situation by using the so called "cogen approach". In that way one gets the benefits of self-application without having to devise a self-applicable specialiser.

The thesis also develops a practical application of program specialisation, based on the idea of optimising integrity checking upon updates in deductive databases. To that end the integrity checking procedure is written as a meta-program, which is then specialised for certain transaction patterns. An approach is presented whereby one can automatically obtain very efficient specialised update procedures, executing substantially faster than other integrity checking procedures proposed in the literature.

Partial deduction was heretofore incapable of performing certain useful unfold/fold transformations, like tupling or deforestation. To remedy this situation, the thesis develops the framework of conjunctive partial deduction which, by specialising conjunctions instead of individual atoms, is able to accommodate these optimisations. This makes it possible to consolidate partial deduction with unfold/fold program transformation, incorporating the power of the latter while keeping the automatic control and efficiency considerations of the former. An implementation is used to perform extensive experiments on a challenging set of benchmarks. Although some control problems remain, the experiments demonstrate the practical viability and potential of conjunctive partial deduction.

The last part of the thesis attends to integrating abstract interpretation with partial deduction. It is shown that both these program manipulation methods have limitations on their own and that a combination of these techniques might therefore be extremely useful in practice. This claim is instantiated by developing a fine-grained algorithm, which interleaves top-down (conjunctive) partial deduction steps with bottom-up abstract interpretation steps, and by showing that the algorithm is able to obtain specialisation and analysis outside the reach of either method alone.


Table of Contents and Selective Download

Still under construction.


PART I:Technical Background 9 PART II: On-line Control of Partial Deduction: Controlling Polyvariance 47 PART III: Off-line Control of Partial Deduction: Achieving Self-Application 141 PART IV: Optimising Integrity Checking by Program Specialisation 171 PART V: Conjunctive Partial Deduction 219 PART VI: Combining Abstract Interpretation and Partial Deduction 293 APPENDIX BIBLIOGRAPHY 359


SAMENVATTING (Dutch summary)

Michael Leuschel / K.U. Leuven /