10 Unification and anti-unification
This chapter covers
- Using “unification” to find values that solve equations
- Solving first-order problems with Robinson’s algorithm
- Applying unification to type inference and logic problems
- Using “anti-unification” to find generalizations
- A sketch of a real-world code analysis tool
“Unification” is an intimidating jargon word for a straightforward concept: Given two things that might contain “holes”, find stuff to put in the holes that makes the two things equal. Like in high school algebra:
What can we substitute for “hole” A that makes the equation true? We could put either 2 or 3 into that hole, and then both sides would be “unified”.
In this chapter we’re not going to look at the unification problem on mathematical equations, but rather on data structures. If you can solve the unification problem on data structures on binary trees, then you can also solve arbitrary logic problems. Early work in artificial intelligence made heavy use of this concept, and there are applications to type inference in compilers and many other domains today.