In L. Fribourg and F. Turini, editors, Logic Program Synthesis and Transformation - Meta Programming in Logic. Proceedings of LOPSTR'94 and META'94, Lecture Notes in Computer Science 883, pages 122-137, Pisa, Italy, 1994. Springer Verlag.
In this paper we present a partial evaluation scheme for a ``real life'' subset of Prolog. This subset contains first-order built-in's, simple side-effects and the operational predicate if-then-else. We outline a denotational semantics for this subset of Prolog and show how partial deduction can be extended to specialise programs of this kind. We point out some of the problems not occurring in partial deduction and show how they can be solved in our setting. Finally we provide some results based on an implementation of the above.
Available: Postscript BibTeX
Technical Report CW 199, December 1994
Keywords: Logic Programming, Partial Deduction, Constraints
A partial deduction strategy for logic programs usually uses an abstraction operator to guarantee the finiteness of the set of goals for which partial deductions are produced. Finding an abstraction operator which guarantees finiteness and still does not loose relevant information (with respect to the partial deduction) is a difficult problem. In [1] and [2] Gallagher and Bruynooghe proposed to base the abstraction operator on characteristic paths and trees. A characteristic tree captures the structure of the generated partial SLDNF-tree for a given goal, i.e. it captures the relevant information for partial deduction. The generation of more general atoms having the same characteristic tree would lead to an almost perfect abstraction operator. Unfortunately the abstraction operators proposed in [1] and [2] do not always produce more general atoms and do not always preserve the characteristic trees. In this paper we propose to solve this problem through the use of constraints in the partial deduction process. We show that satisfiability of these constraints is decidable and that they do not introduce a termination problem of their own. We will thus present a partial deduction strategy which
In Proceedings of PEPM'95, the ACM Sigplan Symposium on Partial Evaluation and Semantics-Based Program Manipulation, pages 253-263, June 23-25 La Jolla, California. ACM Press.
In [1] we presented a partial evaluation scheme for a ``real life'' subset of Prolog, containing first-order built-in's, simple side-effects and the operational predicate if-then-else. In this paper we apply this scheme to specialise integrity checking in deductive databases. We present an interpreter which can be used to check the integrity constraints in hierarchical deductive databases. This interpreter incorporates the knowledge that the integrity constraints were not violated prior to a given update and uses a technique to lift the ground representation to the non-ground one for resolution. By partially evaluating this meta-interpreter for certain transaction patterns we are able to obtain very efficient specialised update procedures, executing substantially faster than the original meta-interpreter. The partial evaluation scheme presented in [1] seems to be capable of automatically generating highly specialised update procedures for deductive databases.
Technical Report CW 210, April 1995 (revised August 1995).
Abridged version in: J. Lloyd, editor, Proceedings of ILPS'95, the International Logic Programming Symposium, pages 495-509, Portland, USA, December 1995. MIT Press.
Integrity constraints are very useful in many contexts, such as, for example, deductive databases, abductive and inductive logic programming. However, fully testing the integrity constraints after each update or modification can be very expensive and methods have been developed which simplify the integrity constraints. In this paper, we pursue the goal of writing this simplification procedure as a meta-program in logic programming and then using partial deduction to obtain pre-compiled integrity checks for certain update patterns. We argue that the ground representation has to be used to write this meta-program declaratively. We however also show that, contrary to what one might expect, current partial deduction techniques are then unable to specialise this meta-interpreter in an interesting way and no pre-compilation of integrity checks can be obtained. In fact, we show that partial deduction (alone) is not able to perform any (sophisticated) specialisation at the object-level for meta-interpreters written in the ground representation. We present a solution which uses a novel implementation of the ground representation and an improved partial deduction strategy. With this we are able to overcome the difficulties and produce highly specialised and efficient pre-compiled integrity checks through partial deduction of meta-interpreters.
Keywords: Meta-Programming, Ground Representation, Partial Deduction, Integrity Checking, Declarative Programming
Available: Postscript BibTeX
In H. Decker, U. Geske, T. Kakas, C. Sakama, D. Seipel and T. Urpi, editors, Proceedings of the ICLP'95 Joint Workshop on Deductive Databases and Logic Programming and Abduction in Deductive Databases and Knowledge Based Systems, pages 81-95, June 1995, Kanagawa, Japan. GMD-Studien Nr.266.
Integrity constraints are very useful in many contexts, such as, for example, deductive databases, abductive and inductive logic programming. However, fully testing the integrity constraints after each update or modification can be very expensive and methods have been developed which simplify the integrity constraints. In this paper, we pursue the goal of writing this simplification procedure as a meta-program in logic programming and then using partial deduction to obtain specialised update procedures for certain update patterns. We argue that the ground representation has to be used to write this meta-program declaratively. However, contrary to what one might expect, current partial deduction techniques are then unable to specialise this meta-interpreter in an interesting way and no specialised update procedures can be obtained. We present a solution which uses a novel implementation of the ground representation and an improved partial deduction strategy. With this we are able to overcome the difficulties and produce highly specialised and efficient update procedures through partial deduction of meta-interpreters.
Available: Postscript BibTeX
Technical Report CW 215, October 1995. Revised Version (CW 250) accepted for Publication in New Generation Computing (tentatively scheduled for Vol.16, No.3, May'98).
A partial deduction strategy for logic programs usually uses an abstraction operation to guarantee the finiteness of the set of goals for which partial deductions are produced. Finding an abstraction operation which guarantees finiteness and does not loose relevant information is a difficult problem. In earlier work Gallagher and Bruynooghe proposed to base the abstraction operator on characteristic paths and trees. A characteristic tree captures the structure of the generated partial SLDNF-tree for a given goal.
In this paper we distinguish between the concepts of global and local precision and show why it is a good idea to base abstraction operations on characteristic tree because they capture exactly the local precision aspects. The generation of more general atoms having the same characteristic tree would lead to an almost perfect abstraction operation which provides just enough global precision to avoid any loss of local precision. Unfortunately the abstraction operators proposed by Gallagher and Bruynooghe in earlier work do not always produce more general atoms and do not always preserve the characteristic trees. We show in this paper that this can lead to non-termination and to precision losses. We present an elaborate solution to this problem based on introducing constraints into the partial deduction process. We show that satisfiability of these constraints is decidable and that they do not introduce a termination problem of their own. We will thus present a partial deduction strategy which has no loss of local precision due to the abstraction and always terminates while ensuring correctness.
Keywords: Logic Programming, Program Specialisation, Partial Deduction, Constraints
Available: Postscript BibTeX (you might want to download the more recent CW 250 instead)
In Maurizio Proietti, editor, Proceedings of LOPSTR'95, the 5th International Workshop on Logic Program Synthesis and Transformation, Utrecht, Netherlands, September 1995, Lecture Notes in Computer Science 1048, pages 1-16, Springer Verlag.
Also as Technical Report CW 216, October 1995.
A partial deduction strategy for logic programs usually uses an abstraction operation to guarantee the finiteness of the set of atoms for which partial deductions are produced. Finding an abstraction operation which guarantees finiteness and does not loose relevant information is a difficult problem. In earlier work Gallagher and Bruynooghe proposed to base the abstraction operation on characteristic paths and trees. A characteristic tree captures the relevant structure of the generated partial SLDNF-tree for a given goal. Unfortunately the abstraction operations proposed in the earlier work do not always produce more general atoms and do not always preserve the characteristic trees. This problem has been solved for purely determinate unfolding rules and definite programs in earlier work by Leuschel and De Schreye by using constraints inside the partial deduction process. In this paper we propose an alternate solution which achieves the preservation of characteristic trees for any unfolding rule, normal logic programs (it can even handle some extra-logical built-in's if so desired) and without adding constraints to the partial deduction process (making the re-use of proven unfolding techniques very simple). We thus provide a powerful, generally applicable and elegant abstraction operation for partial deduction providing a fine-grained and terminating control of polyvariance.
Available: Postscript BibTeX
Abstract in: J. Lloyd, editor, Proceedings of ILPS'95, the International Logic Programming Symposium, pages 615-616, Portland, USA, December 1995.
We give a broad and general introduction to program specialisation, including motivating examples for partial deduction, partial evaluation of Prolog and other forms of specialisation. We then provide some insight into the foundations of partial deduction, including correctness and completeness conditions, and illustrate ways in which they can be ensured. We further elaborate the issues related to the control of partial deduction. We briefly discuss off-line control. For on-line control, we motivate and illustrate the distinction between local and global control in partial deduction algorithms, point out some trade-offs and briefly sketch a generic approach based on well- founded orderings and an approach based on characteristic trees. We then discuss some specific problems related to specialisation of meta-programs and indicate some solutions. We further point out relations between partial deduction and program termination, abstract interpretation, unfold/fold transformation and compile-time optimisation. We give a brief overview of existing systems and successful applications. We end with the presentation of some open problems.
In O.Danvy, R.Glück, P.Thiemann, editors, Proceedings of the 1996 Dagstuhl Seminar on Partial Evaluation, Lecture Notes in Computer Science 1110, pages 263-283, Schloss Dagstuhl, Germany, February 1996, Springer Verlag.
Also as Technical Report CW 220, December 1995.
Recently, considerable advances have been made in the (on-line) control of logic program specialisation. A clear conceptual distinction has been established between local and global control and on both levels concrete strategies as well as general frameworks have been proposed. For global control in particular, recent work has developed concrete techniques based on the preservation of characteristic trees (limited, however, by a given, arbitrary depth bound) to obtain a very precise control of polyvariance. On the other hand, the concept of an m-tree has been introduced as a refined way to trace "relationships" of partially deduced atoms, thus serving as the basis for a general framework within which global termination of partial deduction can be ensured in a non ad hoc way. Blending both, formerly separate, contributions, in this paper, we present an elegant and sophisticated technique to globally control partial deduction of normal logic programs. Leaving unspecified the specific local control one may wish to plug in, we develop a concrete global control strategy combining the use of characteristic atoms and trees with global (m-)trees. We thus obtain partial deduction that always terminates in an elegant, non ad hoc way, while providing excellent specialisation as well as fine-grained (but reasonable) polyvariance. We conjecture that a similar approach may contribute to improve upon current (on-line) control strategies for functional program transformation methods such as (positive) supercompilation.
Available: Postscript BibTeX
In O.Danvy, R.Glück, P.Thiemann, editors, Proceedings of the 1996 Dagstuhl Seminar on Partial Evaluation, Lecture Notes in Computer Science 1110, pages 238-262, Schloss Dagstuhl, Germany, February 1996, Springer Verlag.
Also as Technical Report CW 221, February 1996.
A new, revised and much extended version is available as technical report DSSE-TR-99-6.
The so called "cogen approach" to program specialisation, writing a compiler generator instead of a specialiser, has been used with considerable success in partial evaluation of both functional and imperative languages. This paper demonstrates that this approach is also applicable to partial evaluation of logic programming languages, also called partial deduction. Self-application has not been as much in focus in partial deduction as in partial evaluation of functional and imperative languages, and the attempts to self-apply partial deduction systems have, of yet, not been altogether that successful. So especially for partial deduction, the cogen approach could prove to have a considerable importance when it comes to practical applications. It is demonstrated that using the cogen approach one gets very efficient compiler generators which generate very efficient generating extensions which in turn yield (for some examples at least) very good and non-trivial specialisation.
Available: Postscript BibTeX
In M.Maher, editor, Proceedings of JICSLP'96, the Joint International Conference and Symposium on Logic Programming, pages 319-332, Bonn, Germany, September 1996. MIT Press.
Also as Technical Report CW 225, February 1996.
The relation between partial deduction and the unfold/fold approach has been a matter of intense discussion. In this paper we consolidate the advantages of the two approaches and provide an extended partial deduction framework in which most of the tupling and deforestation transformations of the fold/unfold approach, as well the current partial deduction transformations, can be achieved. Moreover, most of the advantages of partial deduction, e.g. lower complexity and a more detailed understanding of control issues, are preserved. We build on well-defined concepts in partial deduction and present a conceptual embedding of folding into partial deduction, called conjunctive partial deduction. Two minimal extensions to partial deduction are proposed: using conjunctions of atoms instead of atoms as the principle specialisation entity and also renaming conjunctions of atoms instead of individual atoms. Correctness results for the extended framework (with respect to computed answer semantics and finite failure semantics) are given. Experiments with a prototype implementation are presented, showing that, somewhat to our surprise, conjunctive partial deduction not only handles the removal of unnecessary variables, but also leads to substantial improvements in specialisation for standard partial deduction examples.
Keywords: Program Specialisation, Program Transformation, Partial Deduction, Unfold/Fold Transformations
Available: Postscript BibTeX
In H.Kuchen and S.D. Swierstra, editors, Proceedings of PLILP'96, the 8th International Symposium on Programming Languages, Implementations, Logics, and Programs, pages 137-151, Aachen, Germany, September 1996. LNCS 1140, Springer Verlag.
Extended version as Technical Report CW 232, May 1996.
Standard partial deduction suffers from several drawbacks when compared to top-down abstract interpretation schemes. Conjunctive partial deduction, an extension of standard partial deduction, remedies one of those, namely the lack of side-ways information passing. But two other problems remain: the lack of success-propagation as well as the lack of inference of global success-information. We illustrate these drawbacks and show how they can be remedied by combining conjunctive partial deduction with an abstract interpretation technique known as more specific program construction. We present a simple, as well as a more refined integration of these methods. Finally we illustrate the practical relevance of this approach for some advanced applications, like proving functionality or specialising certain meta-programs written in the ground representation, where it surpasses the precision of current abstract interpretation techniques.
Keywords: Program Analysis and Transformation, Partial Deduction, Partial Evaluation, Abstract Interpretation, Deforestation, Meta-Programming
Available: Postscript BibTeX
In J. Gallagher, editor, Proceedings of the International Workshop on Logic Program Synthesis and Transformation (LOPSTR'96), pages 59-82, Stockholm, Sweden, August 1996. LNCS 1207, Springer Verlag.
Extended Version as Technical Report CW 242, October 1996.
Recently, partial deduction of logic programs has been extended to conceptually embed folding. To this end, partial deductions are no longer computed of single atoms, but rather of entire conjunctions; Hence the term "conjunctive partial deduction".
Conjunctive partial deduction aims at achieving unfold/fold-like program transformations such as tupling and deforestation within fully automated partial deduction. However, its merits greatly surpass that limited context: Also other major efficiency improvements are obtained through considerably improved side-ways information propagation. In this extended abstract, we investigate conjunctive partial deduction in practice. We describe the concrete options used in the implementation(s), look at abstraction in a practical Prolog context, include and discuss an extensive set of benchmark results. From these, we can conclude that conjunctive partial deduction indeed pays off in practice, thoroughly beating its conventional precursor on a wide range of small to medium size programs. However, controlling it in a perfect way proves far from obvious, and a range of challenging open problems remain as topics for further research.
Available: Postscript BibTeX
In J. Gallagher, editor, Proceedings of the International Workshop on Logic Program Synthesis and Transformation (LOPSTR'96), pages 83-103, Stockholm, Sweden, August 1996. LNCS 1207, Springer Verlag.
Extended Version as Technical Report CW 243, October 1996.
This paper is concerned with the problem of removing, from a given logic program, {\em redundant arguments}. These are arguments which can be removed without affecting correctness. Most program specialisation techniques, even though they perform argument filtering and redundant clause removal, fail to remove a substantial number of redundant arguments, yielding in some cases rather inefficient residual programs. We formalise the notion of a redundant argument and show that one cannot decide effectively whether a given argument is redundant. We then give a safe, effective approximation of the notion of a redundant argument and describe several simple and efficient algorithms calculating based on the approximative notion. We conduct extensive experiments with our algorithms on mechanically generated programs illustrating the practical benefits of our approach.
Keywords: Logic Programming, Partial Deduction, Program Transformation, Unfold/Fold, Slicing.
Available: Postscript BibTeX
Technical Report CW 237, July 1996. Revised version in The Journal of Logic Programming 36(2), pages 149-193. August 1998.
Integrity constraints are useful for the specification of deductive databases, as well as for inductive and abductive logic programs. Verifying integrity constraints upon updates is a major efficiency bottleneck and specialised methods have been developed to speedup this task. They can however still incur a considerable overhead. In this paper we propose a solution to this problem by using partial evaluation to pre-compile the integrity checking for certain update patterns. The idea being, that a lot of the integrity checking can already be performed given an update pattern without knowing the actual, concrete update.
In order to achieve the pre-compilation, we write the specialised integrity checking as a meta-interpreter in logic programming. This meta-interpreter incorporates the knowledge that the integrity constraints were not violated prior to a given update and uses a technique to lift the ground representation to the non-ground one for resolution. By partially evaluating this meta-interpreter for certain transaction patterns, using a sophisticated partial evaluation technique presented in earlier work, we are able to automatically obtain very efficient specialised update procedures, executing, for instance, substantially faster than the original meta-interpreter.
Keywords: Logic Programming, Program Specialisation, Partial Evaluation, Partial Deduction, Deductive Databases, Integrity Constraints.
Available: Postscript BibTeX
Technical Report CW 248, February 1997. Revised version in ACM Transactions on Programming Languages and Systems (Toplas), volume 20(1), pages 208-258.
Given a program and some input data, partial deduction computes a specialised program handling any remaining input more efficiently. However, controlling the process well is a rather difficult problem. In this paper, we elaborate global control for partial deduction: For which atoms, among possibly infinitely many, should specialised relations be produced, meanwhile guaranteeing correctness as well as termination\/? Our work is based on two ingredients. First, we use the concept of a characteristic tree, encapsulating specialisation behaviour rather than syntactic structure, to guide generalisation and polyvariance, and show how this can be done in a correct and elegant way. Secondly, we structure combinations of atoms and associated characteristic trees in global trees registering ``causal'' relationships among such pairs. This allows us to spot looming non-termination and perform proper generalisation in order to avert the danger, without having to impose a depth bound on characteristic trees. The practical relevance and benefits of the work are illustrated through extensive experiments. Finally, a similar approach may improve upon current (on-line) control strategies for program transformation in general such as (positive) supercompilation of functional programs. It also seems valuable in the context of abstract interpretation to handle infinite domains of infinite height with more precision.
Keywords: Flow Analysis, Partial Deduction, Partial Evaluation, Program Transformation, Supercompilation.
Available: BibTeX
PhD Thesis, K.U. Leuven, May 1997. 396 pages.
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.
Available: Postscript (Full Text, 829 kB compressed) DVI version of the Full Text (673 kB compressed) BibTeX More Information and Selective Download
In N. Fuchs, editor, Logic Program Synthesis and Transformation. Proceedings of LOPSTR'97, pages 189-205, Leuven, Belgium, July, 1997. LNCS 1463, Springer-Verlag.
We provide a first investigation of the specialisation and transformation of tabled logic programs through unfolding. We show that - surprisingly - unfolding, even determinate, can worsen the termination behaviour in the context of tabling. We therefore establish two criteria which ensure that such mishaps are avoided. We also briefly discuss the influence of some other transformation techniques on the termination and efficiency of tabled logic programs.
Available: BibTeX
In N. Fuchs, editor, Logic Program Synthesis and Transformation. Proceedings of LOPSTR'97, pages 111-127, Leuven, Belgium, July, 1997. LNCS 1463, Springer-Verlag.
This work has been motivated by an initial study on how to adapt advanced program specialisation techniques, originally developed for standard logic programming, to the context of tabled logic programming. In a companion paper, we describe how left-propagation of bindings in a program executed under SLG-resolution using a fixed left-to-right selection rule (as SLG is usually implemented in practical systems such as XSB) can seriously endanger the termination characteristics of that program.
In the companion paper, preconditions for safe (i.e. termination preserving) program specialisation through unfolding are proposed. In the present paper we study the termination of tabled programs, executed under SLG using a fixed left-to-right selection rule, in its own right. We adapt existing results on acceptability of programs with respect to sets of atoms. We show how this provides a natural necessary and sufficient condition for the termination of tabled logic programs. We also briefly discuss automatic verification of the proposed termination conditions, and present a non-trivial example.
Available: BibTeX
Technical Report CW 250, June 1997. Revised version in New Generation Computing Vol.16 No.3, 1998, pages 283-342.
Revised Version of CW 215.
Partial deduction strategies for logic programs often use an abstraction operator to guarantee the finiteness of the set of goals for which partial deductions are produced. Finding an abstraction operator which guarantees finiteness and does not lose relevant information is a difficult problem. In earlier work Gallagher and Bruynooghe proposed to base the abstraction operator on characteristic paths and trees, which capture the structure of the generated incomplete SLDNF-tree for a given goal.
In this paper we exhibit the advantages of characteristic trees over purely syntactical measures: if characteristic trees can be preserved upon generalisation, then we obtain an almost perfect abstraction operator, providing just enough polyvariance to avoid any loss of local specialisation. Unfortunately, the abstraction operators proposed in earlier work do not always preserve the characteristic trees upon generalisation. We show that this can lead to important specialisation losses as well as to non-termination of the partial deduction algorithm. Furthermore, this problem cannot be adequately solved in the ordinary partial deduction setting.
We therefore extend the expressivity and precision of the Lloyd and Shepherdson partial deduction framework by integrating constraints. We provide formal correctness results for the so obtained generic framework of constrained partial deduction. Within this new framework we are, among others, able to overcome the above mentioned problems by introducing an alternative abstraction operator, based on so called pruning constraints. We thus present a terminating partial deduction strategy which, for purely determinate unfolding rules, induces no loss of local specialisation due to the abstraction while ensuring correctness of the specialised programs.
Keywords: Logic Programming, Program Specialisation, Partial Deduction, Constraints
Available: Postscript Dvi BibTeX
In F. Bry, B. Freitag and D. Seipel, editors, Proceedings of the 12th Workshop Logische Programmierung (WLP'97), pages 116-126, Munich, Germany, September 1997.
Summary of CW 250.
Partial deduction based upon the Lloyd and Shepherdson framework generates a specialised program given a set of atoms. Each such atom represents all its instances. This can severely limit the specialisation potential of partial deduction. We therefore extend the precision the Lloyd and Shepherdson approach by integrating ideas from constraint logic programming. We formally prove correctness of this new framework of constrained partial deduction and illustrate its potential on some examples.
Keywords: Logic Programming, Program Specialisation, Partial Deduction, Constraints
Available: Postscript Dvi BibTeX
In G. Puebla, editor, Proceedings of the ILPS'97 Workshop on Tools and Environments for (Constraint) Logic Programming, Port Jefferson, USA, October 1997.
We present the fully automatic partial deduction system ECCE, which can be used to specialise and optimise logic programs. We describe the underlying principles of ECCE and illustrate some of the potential application areas. Interesting possibilites of cross-fertilisation with other fields such as reachability analysis of concurrent systems and inductive theorem proving are highlighted and substantiated.
Available: Postscript (gzipped) BibTeX
Technical Report CW 252, June 1997 (revised August 1997). Abridged version in F. Bry, B. Freitag and D. Seipel, editors, Proceedings of the 12th Workshop Logische Programmierung (WLP'97), pages 92-103, Munich, Germany, September 1997.
This technical report is superseded by the technical report DSSE-TR-98-11.
Recently well-quasi orders in general, and homeomorphic embedding in particular, have gained popularity to ensure the termination of program analysis, specialisation and transformation techniques. However, as we illustrate in the paper, the homeomorphic embedding relation as it is usually defined suffers from several inadequacies which make it less suitable in a logic programming context. We present several increasingly refined ways to remedy this problem by providing more sophisticated treatments of variables and present a new, extended homeomorphic embedding relation.
Keywords: Termination, Well-quasi orders, Logic Programming, Program Transformation, Program Analysis, Partial Deduction
Available: Postscript Dvi BibTeX
Technical Report CW 259, May 1998. Abridged version in J. Jaffar, editor, Proceedings of JICSLP'98, the Joint International Conference and Symposium on Logic Programming, pages 2220-234, Manchester, UK, June 1998. MIT Press.
We clarify the relationship between abstract interpretation and program specialisation in the context of logic programming. We present a generic top-down abstract specialisation framework, along with a generic correctness result, into which a lot of the existing specialisation techniques can be cast. The framework also shows how these techniques can be further improved by moving to more refined abstract domains. It, however, also highlights inherent limitations shared by all these approaches. In order to overcome them, and to fully unify program specialisation with abstract interpretation, we also develop a generic combined bottom-up/top-down framework, which allows specialisation and analysis outside the reach of existing techniques.
Available: Postscript (gzipped) BibTeX
Technical Report DSSE-TR-98-11, October 1998.
Extended and revised version of On the power of homeomorphic embedding for online termination. In G. Levi, editor, Static Analysis, Proceedings of SAS'98, pages 230-245, Pisa, Italy, September 1998. LNCS 1503, Springer-Verlag.
It also contains the material in Improving homeomorphic embedding for online termination. In P. Flener, editor, Proceedings of LOPSTR'98, pages 199-218, Manchester, UK, June 1998. LNCS 1559, Springer-Verlag.
Recently well-quasi orders in general, and homeomorphic embedding in particular, have gained popularity to ensure the termination of program analysis, specialisation and transformation techniques. In this paper we investigate and clarify for the first time, both intuitively and formally, the advantages of such an approach over one using well-founded orders. Notably we show that the homeomorphic embedding relation is strictly more powerful than a large class of involved well-founded approaches. We, however, also illustrate that the homeomorphic embedding relation suffers from several inadequacies which are unsatisfactory in contexts, such as logic or functional & logic programming, where logical variables arise. We therefore also present new, extended homeomorphic embedding relations to remedy this problem.
Keywords: Termination, Well-quasi orders, Program Analysis, Specialisation and Transformation, Logic Programming, Functional & Logic Programming
Available: Postscript (gzipped) Dvi BibTeX
Technical Report DSSE-TR-99-3, February 1999.
In Third International Conference Perspectives of System Informatics, Novosibirsk, Russia, July 1999. LNCS 1755, pages 101-112, Springer-Verlag.
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).
Keywords: Partial evaluation, mixed computation, and abstract interpretation, Program transformation and specialisation, Logic programming, Partial deduction, Termination
Available: Postscript (gzipped) Dvi BibTeX
In Third International Conference Perspectives of System Informatics, Novosibirsk, Russia, July 1999. LNCS 1755, pages 93-100, Springer-Verlag.
We present an approach to software verification by program inversion, exploiting recent progress in the field of automatic program transformation, partial deduction and abstract interpretation. Abstraction-based partial deduction can work on infinite state spaces and produce finite representations of infinite solution sets. We illustrate the potential of this approach for infinite model checking of safety properties.
In G.-J. Kruijff and R.T. Oehrle, editors, Proceedings of Formal Grammar 99, pages 93-101, Utrecht, The Netherlands, August 1999.
We present a framework, along with formal correctness results, for analysing context-free and context-sensitive grammars by using abstract interpretation. We also hint at a possible instance (and implementation) of the approach using regular expressions and the homeomorphic embedding relation to ensure termination. We hope that our approach will prove to be useful for analysing difficult properties of formal grammars and for providing compact approximations of them.
Technical Report DSSE-TR-99-6, September 1999.
Submitted.
This is a much extended and improved version of the conference paper Efficiently Generating Efficient Generating Extensions in Prolog.
The so called ``cogen approach'' to program specialisation, writing a compiler generator instead of a specialiser, has been used with considerable success in partial evaluation of both functional and imperative languages. This paper demonstrates that this approach is also applicable to partial evaluation of logic programming languages, also called partial deduction. Self-application has not been as much in focus in logic programming as for functional and imperative languages, and the attempts to self-apply partial deduction systems have, of yet, not been altogether that successful. So, especially for partial deduction, the cogen approach should prove to have a considerable importance when it comes to practical applications. This paper first develops a generic offline partial deduction technique for pure logic programs, notably supporting partially instantiated datastructures via binding types. From this a very efficient cogen is derived, which generates very efficient generating extensions (executing up to several orders of magnitude faster than current online systems) which in turn perform very good and non-trivial specialisation, even rivalling existing online systems. All this is supported by extensive benchmarks. Finally, it is shown how the cogen can be extended to directly support a large part of Prolog's declarative and non-declarative features and how semi-online specialisation can be efficiently integrated.
Available: Postscript (gzipped) Dvi BibTeX
Proceedings of LOPSTR'99, LNCS 1817, pages 63-82.
Preliminary version in Pre-proceedings of LOPSTR'99, pages 137-144, Venice, Italy, September 1999.
We illustrate the use of logic programming techniques for finite model checking of CTL formulaes. We present a technique for infinite state model checking of safety properties based upon logic program specialisation and analysis techniques. The power of the approach is illustrated on several examples. We discuss how this approach has to be extended to handle more complicated infinite state systems and to handle arbitrary CTL formulae.
Available: Postscript
Proceedings of PPDP'2000, ACM Press.
In recent work it has been shown that infinite state model checking can be performed by a combination of partial deduction of logic programs and abstract interpretation. This paper focuses on one particular class of problem--coverability for (infinite state) Petri nets--and shows how existing techniques and tools for declarative programs can be successfully applied. In particular, we show that a restricted form of partial deduction is already powerful enough to decide all coverability properties of Petri Nets. We also prove that two particular instances of partial deduction exactly compute the Karp-Miller tree as well as Finkel's minimal coverability set. We thus establish an interesting link between algorithms for Petri nets and logic program specialisation.
Available: Postscript
The Journal of Logic Programming 41, pages 231-277. November 1999.
Partial deduction in the Lloyd-Shepherdson framework cannot achieve certain optimisations which are possible by unfold/fold transformations. We introduce conjunctive partial deduction, an extension of partial deduction accommodating such optimisations, e.g., tupling and deforestation. We first present a framework for conjunctive partial deduction, extending the Lloyd-Shepherdson framework by considering conjunctions of atoms (instead of individual atoms) for specialisation and renaming. Correctness results are given for the framework with respect to computed answer semantics, least Herbrand model semantics, and finite failure semantics. Maintaining the well-known distinction between local and global control, we describe a basic algorithm for conjunctive partial deduction, and refine it into a {\em concrete algorithm} for which we prove termination. The problem of finding suitable renamings which remove redundant arguments turns out to be important, so we give an independent technique for this. A fully automatic implementation has been undertaken, which always terminates. Differences between the abstract semantics and Prolog's left-to-right execution motivate deviations from the abstract technique in the actual implementation, which we discuss. The implementation has been tested on an extensive set of benchmarks which demonstrate that conjunctive partial deduction indeed pays off, surpassing conventional partial deduction on a range of small to medium-size programs, while remaining manageable in an automatic and terminating system.
Keywords: Program Specialisation and Transformation, Partial Evaluation, Partial Deduction, Unfold/fold, Supercompilation, Logic Programming, Well-quasi orders.
As Elsevier mixed up the numbering of the references, you can download a corrected version of the paper!
Available: Postscript Dvi
Proceedings of CL'2000, LNAI 1861, pages 101-115, Springer-Verlag.
In recent work it has been shown that infinite state model checking can be performed by a combination of partial deduction of logic programs and abstract interpretation. It has also been shown that partial deduction is powerful enough to mimic certain algorithms to decide coverability properties of Petri nets. These algorithms are forward algorithms and hard to scale up to deal with more complicated systems. Recently, it has been proposed to use a backward algorithm scheme instead. This scheme is applicable to so-called well-structured transition systems and was successfully used, e.g., to solve coverability problems for reset Petri nets. In this paper, we discuss how partial deduction can mimic many of these backward algorithms as well. We prove this link in particular for reset Petri nets and Petri nets with transfer and doubling arcs. We thus establish a surprising link between algorithms in Petri net theory and program specialisation, and also shed light on the power of using logic program specialisation for infinite state model checking.
Available: Postscript
Proceedings of LPAR'2000, LNAI 1955, pages 451-468, Springer-Verlag.
We develop an abstract partial deduction method capable of solving planning problems in the Fluent Calculus. To this end, we extend "classical" partial deduction to accommodate both, equational theories and regular type information. We show that our new method is actually complete for conjunctive planning problems in the propositional Fluent Calculus. Furthermore, we believe that our approach can also be used for more complex systems, e.g., in cases where completeness can not be guaranteed due to general undecidability.
Available: Postscript