Anti-unification (AU) is a general approach to finding generalizations between symbolic expressions. The idea is to find a generalization which captures the common structure between a set of expressions. AU has been a problem of continuous interest since the 1970’s in Computer Science. Where anti-unification usually refers to a class of generalization problems for logical expressions of various orders and under various equational theories Library Learning (LL) refers to a practical problem of finding programming functions which capture common structure within a corpus of computer programs.
LL literature seems to frame the LL task as an abstraction problem, which means finding functions which capture the common structure within a corpus of code so a practitioner can understand or leverage a thing according to its practical dimensions for the practitioner’s current problem.
Links
- Anti-unification explained: https://everything.explained.today/Anti-unification/
- Declarative Program Analysis and Optimization: Anti-Unification and Library Learning: An Exploratory Review: https://inst.eecs.berkeley.edu/~cs294-260/sp24/projects/erawn/
- Anti-unification and generalization: a survey: https://dl.acm.org/doi/10.24963/ijcai.2023/736
- Anti-Unification: Introduction, Applications, and Recent Results: https://mayalarincon.github.io/EVENTS/DavidCernaTalk2024.pdf
- Equational Anti-unification over Absorption Theories: https://link.springer.com/chapter/10.1007/978-3-031-63501-4_17