10 Unification of binary terms
This chapter covers
- Using “unification” to find values that solve equations
- Solving first-order problems with Robinson’s algorithm
- Applying the algorithm to type inference and logic problems
“Unification” is an intimidating jargon word for a straightforward concept: Given two things that contain “holes”, find stuff to put in the holes that makes the two things equal. Like in high school algebra:
We’ve got two things – an expression on one side and zero on the other – that we’d like to be equal. What can we substitute for the “hole” labeled X 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. Why do we care about solving equations on data structures? Because if you can solve the unification problem on data structures such as stacks or binary trees, then you can also solve arbitrary logic problems! There are applications to type inference in compilers and many other domains.
We’ll start by unifying two stacks to get some insights; that will lead us to unification of binary terms. Along the way we’ll illustrate how easy it is to get this algorithm wrong by forgetting about some of the tricky cases.