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
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, as in high-school algebra:
A 2 + 6 = 5 × A
What can we substitute for hole A to make the equation true? We could put 2 or 3 in that hole, and both sides would be unified.
In this chapter, we’re going to look at the unification problem not on mathematical equations but on data structures. If you can solve the unification problem on data structures—specifically on binary trees—you can also solve arbitrary logic problems. Early work in artificial intelligence made heavy use of this concept, and it has applications to type inference in compilers and many other domains today.