Equational Anti-Unification over Absorption Theories

TL;DR

This paper develops a sound and complete algorithm for anti-unification modulo absorption theories, addressing the infinitary nature of the problem and providing finitary solutions, with applications in software analysis.

Contribution

It introduces the first rule-based algorithm for anti-unification over absorption theories, handling infinitary cases and ensuring finitary representations.

Findings

Algorithm is sound and complete for absorption theories.

Anti-unification modulo absorption is inherently infinitary.

The linear variant of the algorithm is finitary.

Abstract

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.