Type dependencies for logic programs using ACI-unification

This paper presents a new notion of typing for logic programs which general izes the notion of directional types. The generation of tl pe dependencies for a logic program is fully automatic with respect to a given domain of ty pes. The analysis method is based on a novel combination of program abstrac tion and ACI-unification which is shown to be correct and optimal. Type dep endencies are obtained by abstracting programs, replacing concrete terms by their types, and evaluating the meaning of the abstract programs using a s tandard semantics for logic programs enhanced by ACI-unification. This appr oach is generic and can be used with any standard semantics. The method is both theoretically clean and easy to implement using general purpose tools. The proposed domain of types is condensing which means that analyses can b e carried out in both top-down or bottom-up frameworks with no loss of prec ision for goal-independent analyses. The proposed method has been fully imp lemented within a bottom-up approach and the experimental results are promi sing. (C) 2000 Elsevier Science B.V. All rights reserved.