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 generalization under ≥ nor the structure-preserving generalization. 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 least generalization under ≥ of any pair of second-order terms, whereas pfg computes the generalization equivalent to lg under ≥. Nevertheless, neither ifg nor pfg preserves the structural information. Hence, we also introduce the algorithm spg and show that it computes a structure-preserving generalization. Finally, we show that the algorithms lg, pfg and spg are associative, while the algorithm ifg is not.
['Kouichi Hirata', 'Takeshi Ogawa', 'Masateru Harao']
Generalization Algorithms for Second-Order Terms