Higher-Order Pattern Anti-Unification in Linear Time

Baumgartner, Alexander
Kutsia, Temur
Levy, Jordi
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 α-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 ​
This document is licensed under a Creative Commons:Attribution (by) Creative Commons by3.0