Approximating Constraint Logic Programs Using . . .

Approximate descriptions of the success set of a program have many uses in program development and optimisation. For untyped logic programming languages, regular approximation is a practical and useful tool. In this paper we consider the problem of approximating the meaning of programs in which some #polymorphic# type information is given. This situation can arise in constraint logic programming languages. In untyped languages the user could impose types on selected symbols. Even in strongly typed languages wemay be able to derive more precise descriptions of the meaning, or to consider restricted uses of polymorphic typed predicates. We propose a practical two-stage method: #rst the original program is transformed by replacing typed arguments by corresponding polymorphic type terms. For well-typed programs the resulting program is an abstraction of the original. Second, an established algorithm for regular approximation is applied to the transformed program. The algorithm is guaranteed to terminate without using arti#cial techniques such as depth-k bounds on #type# terms. The derived description combines polymorphic type terms, including union types, with regular descriptions of untyped terms. The method allows goal-dependent analysis as well as goal-independent analysis of a complete program. We show some experimental results demonstrating the speed and precision of the method and show that it scales up well when applied to larger programs