Applying program transformation to type inference for a logic language

This paper presents a type inference algorithm for a logic language, LHS. T he algorithm uses a program transformation, SPS, to given programs as a typ e inference. This method is theoretically clear, because applying it to giv en pro grams is equal to executing it partially. No other additional framew ork 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, w hich was initially developed for functional languages. Therefore, the meani ngs of the algorithms are theoretically unclear in the domain of logic lang uages. Our type inference is flexible. Users of the type inference system c an specify the types of objects abstractly (weakly) if the types are not ex actly known, or they can specify them particularly (strongly) if the types are exactly known. Both kinds of programs are inferred for types. Tn contra st, many type inference systems accept purely untyped programs. Thus, with these two features, our method is simple and flexible.