LIPIcs.RTA.2013.113.pdf
- Filesize: 489 kB
- 15 pages
Document
A Variant of Higher-Order Anti-Unification
Authors
-
Part of:
Volume:
24th International Conference on Rewriting Techniques and Applications (RTA 2013)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Rewriting Techniques and Applications (RTA) - License:
Creative Commons Attribution 3.0 Unported license
- Publication date: 2013-06-24
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)
https://doi.org/10.4230/LIPIcs.RTA.2013.113
https://doi.org/10.4230/LIPIcs.RTA.2013.113
Abstract
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.
Keywords
- higher-order anti-unification
- higher-order patterns
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads