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.
@InProceedings{baumgartner_et_al:LIPIcs.RTA.2013.113, author = {Baumgartner, Alexander and Kutsia, Temur and Levy, Jordi and Villaret, Mateu}, title = {{A Variant of Higher-Order Anti-Unification}}, booktitle = {24th International Conference on Rewriting Techniques and Applications (RTA 2013)}, pages = {113--127}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-53-8}, ISSN = {1868-8969}, year = {2013}, volume = {21}, editor = {van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.113}, URN = {urn:nbn:de:0030-drops-40579}, doi = {10.4230/LIPIcs.RTA.2013.113}, annote = {Keywords: higher-order anti-unification, higher-order patterns} }
Feedback for Dagstuhl Publishing