11 Anti-unification of binary terms
This chapter covers
- Using “anti-unification” to find generalizations
- A sketch of a real-world developer assistance tool
In Chapter 10 we learned that “unification” starts with two binary terms that may contain named “holes” and finds a “substitution” – a set of values that go in those hole – such that applying the substitution to both terms produces the same result. What on Earth could anti-unification be?
I like to think of unification as moving from the general to the specific: we start with holes that could contain anything, and we find a specific substitution that satisfies an equation. Anti-unification moves from the specific to the general: we start with two unequal things and identify the parts they have in common; everything else becomes a hole. Unification fills holes; anti-unification makes holes.
Unification is useful because it allows us to find solutions to equations on terms, which is a necessary step in type inference and other forms of automated logical deduction. Anti-unification is useful in situations where we need to find similarities between different things; we’ll see how it is applicable to a variety of code analysis problems, including my personal favorite, deducing bug fixing patterns from examples.