Applying program transformation to type inference for a logic language

This paper presents a type inference algorithm for a logic language, LHS. The algorithm uses a program transformation, SPS, to given programs as a type inference. This method is theoretically clear, because applying it to given pro grams is equal to executing it partially. No other additional framework is needed for our approach. In contrast, many studies on type inference for logic languages are based on Mycroft and O'Keefe's famous algorithm, which was initially developed for functional languages. Therefore, the meanings of the algorithms are theoretically unclear in the domain of logic languages. Our type inference is flexible. Users of the type inference system can specify the types of objects abstractly (weakly) if the types are not exactly known, or they can specify them particularly (strongly) if the types are exactly known. Both kinds of programs are inferred for types. Tn contrast, many type inference systems accept purely untyped programs. Thus, with these two features, our method is simple and flexible.