LIPIcs.RTA.2015.57.pdf
- Filesize: 0.52 MB
- 17 pages
Document
Nominal Anti-Unification
Authors
-
Part of:
Volume:
26th International Conference on Rewriting Techniques and Applications (RTA 2015)
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: 2015-06-18
Cite AsGet BibTex
Alexander Baumgartner, Temur Kutsia, Jordi Levy, and Mateu Villaret. Nominal Anti-Unification. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 57-73, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/LIPIcs.RTA.2015.57
https://doi.org/10.4230/LIPIcs.RTA.2015.57
Abstract
We study nominal anti-unification, which is concerned with computing
least general generalizations for given terms-in-context. In general, the problem does not have a least general solution, but if the set of atoms permitted in generalizations is finite, then there exists a least general generalization which is unique modulo variable renaming and alpha-equivalence. We present an algorithm that computes it. The algorithm relies on a subalgorithm that constructively decides equivariance between two terms-in-context. We prove soundness and completeness properties of both algorithms and analyze their complexity. Nominal anti-unification can be applied to problems where generalization of first-order terms is needed (inductive learning, clone detection, etc.), but bindings are involved.
Keywords
- Nominal Anti-Unification
- Term-in-context
- Equivariance
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads