Directional Type Checking for Logic Programs: Beyond Discriminative Types

Directional types form a type system for logic programs which is based on the view of a predicate as a {\em directional procedure\/} which, when applied to a tuple of input terms, generates a tuple of output terms. It is known that directional-type checking wrt.\ arbitrary types is undecidable; several authors proved decidability of the problem wrt.\ discriminative regular types. In this paper, using techniques based on tree automata, we show that directional-type checking for logic programs wrt.\ general regular types is \dexptime-complete and fixed-parameter linear. The letter result shows that despite the exponential lower bound, the type system might be usable in practice