A Variant of Higher-Order Anti-Unification

Authors Alexander Baumgartner, Temur Kutsia, Jordi Levy, Mateu Villaret

Thumbnail PDF


  • Filesize: 489 kB
  • 15 pages

Document Identifiers

Author Details

Alexander Baumgartner
Temur Kutsia
Jordi Levy
Mateu Villaret

Cite AsGet BibTex

Alexander Baumgartner, Temur Kutsia, Jordi Levy, and Mateu Villaret. A Variant of Higher-Order Anti-Unification. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 113-127, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)


We present a rule-based Huet's style anti-unification algorithm for simply-typed lambda-terms in eta-long beta-normal form, 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. The algorithm computes it in cubic time within linear space. It has been implemented and the code is freely available.
  • higher-order anti-unification
  • higher-order patterns


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail