非表示:
キーワード:
-
要旨:
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.
