מיכאל קודיש

This paper presents an approach to specialising logic programs which is based on abstract interpretation. Program specialisation involves two stages, the construction of an abstract computation tree and a program construction stage. For the tree construction stage, abstract OLDT resolution is defined and used to construct a complete and finite tree corresponding to a given logic program and a goal. In the program construction stage, a specialised program is extracted from this tree. We focus on two logic programming languages: sequential Prolog and Flat Concurrent Prolog. Although the procedural reading of concurrent logic programs is very different from that of sequential programs, the techniques presented provide a uniform approach to the specialisation of both languages. We present the results for Prolog rigorously, and extend them less formally to Flat Concurrent Prolog. There are two main advantages of basing program specialisation on abstract interpretation. Firstly, termination can be ensured by using abstract interpretations over finite domains, while performing a complete flow analysis of the program. Secondly, correctness of the specialised program is closely related to well-defined consistency conditions on the concrete and abstract interpretations.