2026-07-24T21:22:25Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5189 2024-03-06T10:36:01Z ddc:004 open_access

Nominal Anti-Unification Baumgartner, Alexander Kutsia, Temur Levy, Jordi Villaret, Mateu Nominal Anti-Unification Term-in-context Equivariance 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Alexander Baumgartner and Temur Kutsia and Jordi Levy and Mateu Villaret 2015 Is Part Of LIPIcs, Volume 36, 26th International Conference on Rewriting Techniques and Applications (RTA 2015) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.RTA.2015.57 urn:nbn:de:0030-drops-51895 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.57 eng https://creativecommons.org/licenses/by/3.0/legalcode