Section outline

    • Alex Baumgartner: A Variant of Higher-Order Anti-Unification

    The anti-unification problem of two terms t1 and t2 is concerned with finding their generalization, a term t such that both t1 and t2 are instances of t under some substitutions. Interesting generalizations are the least general ones. The purpose of anti- unification algorithms is to compute such least general generalizations. For higher-order terms, in general, there is no unique least general higher-order generalization. Therefore, special classes have been considered for which the uniqueness is guaranteed. One of such classes is formed by higher-order patterns. These are lambda-terms where the arguments of free variables are distinct bound variables. A rule-based anti-unification algorithm in simply-typed lambda- calculus which computes a least general higher-order pattern generalization will be presented. The algorithm computes it in cubic time within linear space and it has been implemented.