Higher-Order Pattern Anti-Unification in Linear Time
Alexander Baumgärtner, Temur Kutsia, Jordi Levy, Mateu Villaret · Journal of Automated Reasoning · 2016
We present a rule-based Huet’s style anti-unification algorithm for simply typed lambda-terms, which computes a least general higher-order pattern generalization. For a pair of arbitrary terms of the same type, such a generalization always exists and is unique modulo $$\alpha $$ α -equivalence and variable renaming. With a minor modification, the algorithm works for untyped lambda-terms as well. The time complexity of both algorithms is linear.