Generalization Problems with Atom-Variables in Languages with Binders and Equational Theories
Daniele Nantes-Sobrinho, Manfred Schmidt-Schauss, Alexander Baumgartner, Temur Kutsia
TL;DR
The paper tackles anti-unification in nominal languages with binders under equational theories $A$, $C$, $AC$, where standard generalization can generate many redundant solutions. It extends a semantic atom-variable framework to compute unique LGGs and presents NAU_E, a sound, weakly complete algorithm that produces finite weak minimal LGG sets while handling equivariance via semantic tests. A key challenge is the interaction between renaming and equational reasoning, requiring semantical checks during equivariance branching. Although $A$, $C$, $AC$ can cause exponential LGG sets due to subexpression permutations, the work points to restricted theory fragments where LGGs are unitary and computable in polynomial time, offering practical benefits for symbolic computation and automated reasoning.
Abstract
Generalization problems in languages with binders involve computing the most common structure between expressions while respecting bound variable renaming and freshness constraints. These problems often lack a least general solution. However, leveraging nominal techniques, we previously demonstrated that a semantic approach with atom-variables enables the elimination of redundant solutions and allows for computing unique least general generalizations (LGGs). In this work, we extend this approach to handle associative (A), commutative (C), and associative-commutative (AC) equational theories. We present a sound and weak complete algorithm for solving equational generalization problems, which generates finite weak minimal complete sets of LGGs for each theory. A key challenge arises from solving equivariance problems while taking into account these equational theories, as identifying redundant generalizations requires recognizing when one expression (with binders) is a renaming of another while possibly considering permutations of sub-expressions. This unexpected interaction between renaming and equational reasoning made this particularly difficult, necessitating semantic tests within the equivariance algorithm. Given that these equational theories naturally induce exponentially large LGG sets due to subexpression permutations, future work could explore restricted theory fragments where the generalization problem remains unitary. In these fragments, LGGs can be computed efficiently in polynomial time, offering practical benefits for symbolic computation and automated reasoning tasks.