Higher Order Generalization

摘要

Generalization is a fundamental operation of inductive inference. While first order syntactic generalization (anti-unification) is well understood, its various extensions are needed in applications. This paper discusses syntactic higher order generalization in a higher order language #lambda#2[1]. Based on the application ordering, we proved the least general generlaization exists and is unique up to renarming. An algorithm to compute the least general generalization is presented.