Datensatz

Zusammenfassung

We follow the set-based approach to directional types proposed by Aiken and Lakshman$\:$\cite{AikenL:sas94}. Their type \emph{checking} algorithm works via set constraint solving and is sound and complete for given discriminative types. We characterize directional types in model-theoretic terms. We present an algorithm for \emph{inferring} directional types. The directional type that we derive from a logic program~$\P$ is uniformly at least as precise as any discriminative directional type of~$\P$, i.e., any directional type out of the class for which the type {\em checking\/} algorithm of Aiken and Lakshman is sound and complete. We improve their algorithm as well as their lower bound and thereby settle the complexity (D{\footnotesize EXPTIME}-complete) of the corresponding problem.