Interest in anti-unification, the dual problem of unification, is on the rise due to applications within the field of software analysis and related areas. For example, anti-unification-based techniques have found uses within clone detection and automatic program repair methods. While syntactic forms of anti-unification are enough for many applications, some aspects of software analysis methods are more appropriately modeled by reasoning modulo an equational theory. Thus, extending existing anti-unification methods to deal with important equational theories is the natural step forward. This paper considers anti-unification modulo pure absorption theories, i.e., some operators are associated with a special constant satisfying the axiom $f(x,\varepsilon_f) \approx f(\varepsilon_f,x) \approx \varepsilon_f$. We provide a sound and complete rule-based algorithm for such theories. Furthermore, we show that anti-unification modulo absorption is infinitary. Despite this, our algorithm terminates and produces a finitary algorithmic representation of the minimal complete set of solutions. We also show that the linear variant is finitary.

翻译：反统一（unification的对偶问题）因在软件分析及相关领域的应用而日益受到关注。例如，基于反统一的技术已被应用于克隆检测和自动程序修复方法中。虽然句法形式的反统一足以应对许多应用场景，但软件分析方法中的某些方面更适合通过模方程理论进行推理建模。因此，将现有反统一方法扩展以处理重要方程理论是自然的进步方向。本文研究了纯吸收理论模下的反统一问题，即某些算子关联一个满足公理$f(x,\varepsilon_f) \approx f(\varepsilon_f,x) \approx \varepsilon_f$的特殊常数。我们为此类理论提供了完备且可靠的基于规则算法。此外，我们证明吸收理论模反统一是无穷的。尽管存在这一特性，我们的算法仍能终止，并生成最小完备解集的有限算法表示。我们还证明线性变体是有限的。