Approximating Constraint Logic Programs Using Polymorphic Types and Regular DescriptionsHuseyin Saglam, John P. Gallagher, Approximating Constraint Logic Programs Using Polymorphic Types and Regular Descriptions. CSTR-95-017, Department of Computer Science, University of Bristol. July 1995. PDF, 235 Kbytes.
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. % as well as typed logic programming languages like Goedel. Even in strongly typed languages we may 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: first 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 artificial 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.