Higher order generalization

Abstract

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 λ2[1]. Based on the application ordering, we proved the least general generalization exists and is unique up to renaming. An algorithm to compute the least general generalization is presented.