Logic programs as types for logic programs

Abstract

Optimistic type systems for logic programs are considered. In such systems types are conservative approximations to the success set of the program predicates. The use of logic programs to describe types is proposed. It is argued that this approach unifies the denotational and operational approaches to descriptive type systems and is simpler and more natural than previous approaches. The focus is on the use of unary-predicate programs to describe the types. A proper class of unary-predicate programs is identified, and it is shown that it is expensive enough to express several notions of types. An analogy with two-way automata and a correspondence with alternating algorithms are used to obtain a complexity characterization of type inference and type checking. This characterization is facilitated by the use of logic programs to represent types.<>