A precise type analysis of logic programs

Abstract

This paper presents a new type analysis for logic programs. The type information in a set of substitutions is described by a disjunction of variable typings each of which maps a variable to a non-deterministic regular type. The use of non-deterministic regular types, set union and intersection operators, and disjunctions of variable typings makes the new type analysis more precise than those found in the literature. Experimental results on the performance of the new analysis are given together with comparable results from an existing type analysis. The fundamental problem of checking the emptiness of non-deterministic regular types is more complex in the new analysis. The experimental results, however, show that careful use of tabling reduces the effect to an average of 15% of execution time on a set of benchmarks.