# Equational Anti-unification: Algorithms and Types

David M. Cerna

► To cite this version:

David M. Cerna. Equational Anti-unification: Algorithms and Types. UNIF 2025 - 39th International Workshop on Unification, Jul 2025, Birmingham, United Kingdom. hal-05148578

HAL Id: hal-05148578

https://hal.science/hal-05148578v1

Submitted on 7 Jul 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>
Equational Anti-unification: Algorithms and
Types

David M. Cerna

Dynatrace Research, Linz, Austria
Czech Academy of Sciences, Institute of Computer Science,
Prague, Czechia

June 26, 2025

Anti-unification (AU), also known as *generalization*, is a fundamental operation used for inductive inference [6]. It is abstractly defined as a process deriving from a set of symbolic expressions a new symbolic expression possessing certain commonalities shared between its members. While there exists applications of syntactic anti-unification and its variants [7], more often than not, anti-unification is applied to expressions interpreted over an equational theory [1, 3]. J. Burghardt presented a general procedure for equational generalization for equational theories whose congruence classes are computable using regular tree grammars [2]. While this algorithm is complete, it does not guarantee that the resulting set of generalizations is minimal. As shown in [5], even simple theories fitting Burghardt criteria are *nullary*. Further, while *idempotent* anti-unification is not *nullary* [4], a grammar construction similar to what is described in Burghardt’s work shows that anti-unification is *infinitary* even in the linear case. For *finite* theories, Burghardt’s procedure will give us a minimizable set of generalizations. In this talk, we discuss the above and related recent results and possible criteria for distinguishing type-wise well-behaved theories.

References

[1] Adam D. Barwell et al. Finding parallel functional pearls: Automatic parallel recursion scheme detection in haskell functions via anti-unification. *Future Gener. Comput. Syst.*, 79:669–686, 2018.

[2] Jochen Burghardt. E-generalization using grammars. *Artif. Intell.*, 165(1):1–35, 2005.

[3] David Cao, Rose Kunkel, Chandrakana Nandi, Max Willsey, Zachary Tatlock, and Nadia Polikarpova. babble: Learning better abstractions with e-graphs and anti-unification. *Proc. ACM Program. Lang.*, 7(POPL), January 2023.

[4] David M. Cerna and Temur Kutsia. Idempotent anti-unification. *ACM Trans. Comput. Log.*, 21(2):10:1–10:32, 2020.
[5] David M. Cerna and Temur Kutsia. Unital anti-unification: Type and algorithms. In *FSCD*, LIPIcs, 2020.

[6] David M. Cerna and Temur Kutsia. Anti-unification and generalization: a survey. In *Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence*, IJCAI '23, 2023.

[7] Brigitte Pientka. Higher-order term indexing using substitution trees. *ACM Trans. Comput. Log.*, 11(1):6:1–6:40, 2009.