Deletion of Redundant Unary Type Predicates from Logic Programs

Abstract

In this paper, program transformation is proposed as a way of handling type information efficiently. A typed program is translated to an untyped program, with regular unary predicates replacing the types, and then an attempt is made to eliminate as many of the unary type literals as possible. The method is as follows: first a query-answer transformation of the program with a given goal is made. This gives a specification of the calls to each literal in the program arising in the computation of the goal. The set of calls defines the context of the literal in the computation. Any literal can be eliminated if its answers are implied by its context. We define a procedure for eliminating literals defined by regular programs, a class which includes the type literals. A regular approximation of the query-answer program is made, and then decidable properties of regular programs are used to check for the elimination of the literal. The method can be compared with type-checking, since the elimination procedure also shows whether some type literal fails, indicating a “badly-typed” clause. Our aim however is not to construct a type system, but rather to show that simple types can be handled using a general framework of program analysis and transformation.

Work supported by ESPRIT Project PRINCE (P5246)