TY - GEN
T1 - A variant of higher-order anti-unification
AU - Baumgartner, Alexander
AU - Kutsia, Temur
AU - Levy, Jordi
AU - Villaret, Mateu
PY - 2013
Y1 - 2013
N2 - We present a rule-based Huet's style anti-unification algorithm for simply-typed lambda-terms in η-long -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 α-equivalence and variable renaming. The algorithm computes it in cubic time within linear space. It has been implemented and the code is freely available.
AB - We present a rule-based Huet's style anti-unification algorithm for simply-typed lambda-terms in η-long -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 α-equivalence and variable renaming. The algorithm computes it in cubic time within linear space. It has been implemented and the code is freely available.
KW - Higher-order anti-unification
KW - Higher-order patterns
UR - https://www.scopus.com/pages/publications/84889595348
U2 - 10.4230/LIPIcs.RTA.2013.113
DO - 10.4230/LIPIcs.RTA.2013.113
M3 - Conference proceeding
AN - SCOPUS:84889595348
SN - 9783939897538
T3 - Leibniz International Proceedings in Informatics, LIPIcs
SP - 113
EP - 127
BT - 24th International Conference on Rewriting Techniques and Applications, RTA 2013
A2 - van Raamsdonk, Femke
PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
T2 - 24th International Conference on Rewriting Techniques and Applications, RTA 2013
Y2 - 24 June 2013 through 26 June 2013
ER -