2026-07-26T00:33:31Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:4057 2024-03-06T10:34:45Z ddc:004 open_access

A Variant of Higher-Order Anti-Unification Baumgartner, Alexander Kutsia, Temur Levy, Jordi Villaret, Mateu higher-order anti-unification higher-order patterns 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Alexander Baumgartner and Temur Kutsia and Jordi Levy and Mateu Villaret 2013 Is Part Of LIPIcs, Volume 21, 24th International Conference on Rewriting Techniques and Applications (RTA 2013) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.RTA.2013.113 urn:nbn:de:0030-drops-40579 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.113 eng https://creativecommons.org/licenses/by/3.0/legalcode