Nominal anti-unification
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 -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 were generalization of first-order terms is needed (inductive learning, clone detection, etc.), but bindings are involved.
Cite
@article{arxiv.2504.21097,
title = {Nominal anti-unification},
author = {Alexander Baumgartner and Temur Kutsia and Jordi Levy and Mateu Villaret},
journal= {arXiv preprint arXiv:2504.21097},
year = {2025}
}