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.
@InProceedings{baumgartner_et_al:LIPIcs.RTA.2015.57, author = {Baumgartner, Alexander and Kutsia, Temur and Levy, Jordi and Villaret, Mateu}, title = {{Nominal Anti-Unification}}, booktitle = {26th International Conference on Rewriting Techniques and Applications (RTA 2015)}, pages = {57--73}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-85-9}, ISSN = {1868-8969}, year = {2015}, volume = {36}, editor = {Fern\'{a}ndez, Maribel}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.57}, URN = {urn:nbn:de:0030-drops-51895}, doi = {10.4230/LIPIcs.RTA.2015.57}, annote = {Keywords: Nominal Anti-Unification, Term-in-context, Equivariance} }
Feedback for Dagstuhl Publishing