Suppose two code changes look different but may follow the same edit pattern. Anti-unification helps expose the pattern: it takes two specific tree-shaped terms and finds their most specific shared generalization. Where unification fills holes to make terms equal, anti-unification keeps what already matches and makes the differences into holes. section 10.0 section 1.0
Keep every shared detail
Compare Mult(Add(1,2), Div(Add(1,2),5)) with Mult(6, Div(6,5)). Their best generalization is Mult(A, Div(A,5)). Replacing A with Add(1,2) reconstructs the first term; replacing it with 6 reconstructs the second. The repeated A matters: both inputs use the same left operand in the multiplication and division. Mult(X, Div(Y,Z)) could also reconstruct them, but it unnecessarily loses that equality and the shared 5. section 10.4 section 10.5
A recursive algorithm builds the generalization and two substitutions together:
- If the terms are equal, return that term without introducing a hole. section 10.5
- If both roots are symbols with the same name, retain the symbol and recursively compare their corresponding children. section 10.5
- For a difference with no existing hole, create one and record what it stands for in each input. section 10.5
- If that same pair of differing terms appears again, reuse its hole. Generate hole names that do not collide with holes already in the inputs. section 10.5
The result must reconstruct each input under its respective substitution, but reconstruction alone is not enough: needless holes discard similarities. This first-order binary-term algorithm does not generalize symbol names. A naïve implementation can take quadratic time in the worst case; memoization can make it linear. The resulting patterns are useful in program analysis, particularly variations of clone detection. section 10.4 section 10.7
result: Mult(A, Div(A, 5)) sub1: A→Add(1,2) sub2: A→6
The result and its two substitutions make the shared structure and repeated hole visible side by side. section 10.5
