POLYMORPHIC TYPE ANALYSIS IN LOGIC PROGRAMS BY ABSTRACT INTERPRETATION

In this paper, we first introduce a notion of polymorphic abstract int erpretation that formalises a polymorphic analysis as a generalisation of possibly infinitely many monomorphic analyses in the sense that th e results of the monomorphic analyses can be obtained as instances of that of the polymorphic analysis. We then present a polymorphic type a nalysis of logic programs in terms of an abstract domain for polymorph ic descriptions of type information and two operators on the abstract domain, namely the least upper bound operator and the abstract unifica tion operator. The abstract domain captures type information more prec isely than other abstract domains for similar purposes. The abstract u nification operator for the polymorphic type analysis is designed by l ifting the abstract unification operator for a monomorphic type analys is in logic programs, which simplifies the proof of the safeness of th e polymorphic type analysis. Some experimental results with a prototyp e implementation of the polymorphic type analysis are also presented. (C) 1998 Elsevier Science Inc. All rights reserved.