Generalization Algorithms for Second-Order Terms

In this paper, we study the generalization algorithms for second-order terms, which are treated as first-order terms with function variables, under an instantiation order denoted by . First, we extend the least generalization algorithm lg for a pair of first-order terms under , introduced by Plotkin and Reynolds, to the one for a pair of second-order terms. The extended algorithm lg, however, is insufficient to characterize the generalization for a pair of second-order terms, because it computes neither the least nor the minimal generalization under . Since the transformation rule for second-order matching algorithm consists of an imitation and a projection, in this paper, we introduce the imitation-free generalization algorithm ifg and the projection-free generalization algorithm pfg. Then, we show that ifg computes the minimal generalization under of any pair of second-order terms, whereas pfg computes the generalization equivalent to lg under . Nevertheless, neither lg, ifg nor pf...

• Type: Conference
• Year: 2004
• Where: ILP
• Authors: Kouichi Hirata, Takeshi Ogawa, Masateru Harao
• Keywords: Algorithm, Generalization Algorithm, ILP 2004, Second-order Terms