ABSTRACT. Unital theories are characterized by the property of some function symbols having (left and right) unit elements. We address three problems related to unital anti-unification (AU).
First, we prove that when the term signature contains at least two unital functions, anti-unification is of type zero (nullary) by showing that there exists an AU problem, which does not have a minimal complete set of generalizations. Next, we consider two special cases: the linear variant (computed generalizations are linear) and one-unital fragment (the problems are formulated over a language with one unital symbol) and design AU algorithms for them. The algorithms are terminating, sound, complete and return tree grammars from which set of generalizations can be constructed. For the linear variant, the language of generalizations generated by the grammar is finite. In the one-unital fragment, the language might be infinite, but it contains a finite minimal complete set of generalizations. It means that both linear and one-unital AU are finitary. We also design an AU algorithm for the unrestricted case. It terminates and returns a tree grammar which produces an infinite set of generalizations.
This nullarity proof can be extended to other equational theories such as associative-unital, commutative-unital, and their combination, when multiple function symbols may have these properties. However, our argument fails for idempotent-unital theories. We end with a list of open questions derived from this as well as earlier work.