**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

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.

- Postscript of the Full Text (+/- 680 kB g'zipped)
- Postscript of the Full Text (+/- 2 MB uncompressed)
- PDF of the Full Text (+/- 2 MB uncompressed; thanks to Brian Peterson)
- DVI version of the Full Text (+/- 500 kB g'zipped)
- BibTeX

**INTRODUCTION**

- 1 Introduction 1
- 1.1 Logic programming and program specialisation 1
- 1.2 Overview of the thesis 3

- 2 Logic and Logic Programming 11
- 2.1 First-order logic and syntax of logic programs 11
- 2.2 Semantics of logic programs 15
- 2.3 Proof theory of logic programs 19

- 3 Partial Evaluation and Partial Deduction 29
- 3.1 Partial evaluation 29
- 3.2 Partial deduction 32
- 3.3 Control of partial deduction 36

- 4 Characteristic Trees 49
- 4.1 Structure and abstraction 49
- 4.2 Characteristic paths and trees 51
- 4.3 An abstraction operator using characteristic trees 55
- 4.4 Characteristic trees in the literature 61
- 4.5 Extensions of characteristic trees 63

- 5 Ecological Partial Deduction 65
- 5.1 Partial deduction based on characteristic atoms 65
- 5.2 Correctness results 71
- 5.3 A set based algorithm and its termination 86
- 5.4 Some further discussions 90

- 6 Removing Depth Bounds by Adding Global Trees 95
- 6.1 The depth bound problem 95
- 6.2 Partial deduction using global trees 99
- 6.3 Post-processing and other improvements 120
- 6.4 Experimental results and discussion 125
- 6.5 Conclusion and future work 135

- 7 Efficiently Generating Efficient Generating Extensions in Prolog 143
- 7.1 Introduction 143
- 7.2 Off-line partial deduction 148
- 7.3 The cogen approach for logic programming languages 154
- 7.4 Examples and results 159
- 7.5 Discussion and future work 165

- 8 Integrity Checking and Meta-Programming 173
- 8.1 Introduction and motivation 173
- 8.2 Deductive databases and specialised integrity checking 174
- 8.3 Meta-interpreters and pre-compilation 182
- 8.4 Some issues in meta-programming 184

- 9 Pre-Compiling Integrity Checks via Partial Evaluation of Meta-Interpreters 193
- 9.1 A meta-interpreter for integrity checking in hierarchical databases 193
- 9.2 Partial evaluation of ITE-Prolog 196
- 9.3 Experiments and results 202
- 9.4 Moving to recursive databases 213
- 9.5 Conclusion and future directions 214

- 10 Foundations of Conjunctive Partial Deduction 221
- 10.1 Partial deduction vs. unfold/fold 221
- 10.2 Conjunctive partial deduction 224
- 10.3 Correctness results 231
- 10.4 Discussion and conclusion 241

- 11 Redundant Argument Filtering 245
- 11.1 Introduction 245
- 11.2 Correct erasures 247
- 11.3 Computing correct erasures 250
- 11.4 Applications and benchmarks 255
- 11.5 Polyvariance and negation 259
- 11.6 Reverse filtering (FAR) 262
- 11.7 Related work and conclusion 266

- 12 Conjunctive Partial Deduction in Practice 269
- 12.1 Controlling conjunctive partial deduction for pure Prolog 269
- 12.2 The system and its methods 276
- 12.3 Benchmarks and conclusion 278

- 13Logic Program Specialisation: How to Be More Specific 295
- 13.1 Partial deduction vs. abstract interpretation 295
- 13.2 Introducing more specific programs 298
- 13.3 Some motivating examples 303
- 13.4 A more refined algorithm 308
- 13.5 Specialising the ground representation 313
- 13.6 Discussion 315

- 14 Conclusion and Outlook 319

- A Notations for Some Basic Mathematical Constructs 323
- A.1Sets and relations 323
- A.2Sequences 324
- A.3Graphs and trees 324

- B Counterexample 325
- C Benchmark Programs 327
- D Extending the Cogen 333
- E A Prolog Cogen: Source Code 335
- F A Prolog Cogen: Some Examples 339
- F.1 The parser example 339
- F.2 The solve example 341
- F.3 The regular expression example 344

- G Meta-Interpreters and Databases for Integrity Checking 347
- G.1 The
*ic-solve*meta-interpreter 347 - G.2 The
*ic-lst*meta-interpreter 351 - G.3 A more sophisticated database 353

- G.1 The
- H Explicit Unification Algorithms 355
- H.1 A unification algorithm with accumulators 355
- H.2 A unification algorithm without accumulators 357

**INDEX** 387

**SAMENVATTING** (Dutch summary)

Michael Leuschel / K.U. Leuven / michael@cs.kuleuven.ac.be