Unification (2018)

Summary

In logic and computer science, unification is a process of automatically solving equations between symbolic terms. Unification has several interesting applications, notably in logic programming and type inference. In this post I want to present the basic unification algorithm with a complete implementation. Let's start with some terminology. We'll be using terms built from constants, variables and function applications: Pattern matching Unification can be seen as a generalization of pattern matching, so let's start with that first. We're given a constant term and a pattern term. The pattern term has variables. Pattern matching is the problem of finding a variable assignment that will make the two terms match. For example: Constant term: f(a, b, bar(t)) Pattern term: f(a, V, X) Trivially, the assignment V=b and X=bar(t) works here. Another name to call such an assignment is a substitution, which maps variables to their assigned values. In a less trivial case, variables can appear multiple times in a pattern: Constant term: f(top(a), a, g(top(a)), t) Pattern term: f(V, a, g(V), t) Here the right substitution is V=top(a). Sometimes, no valid substitutions exist. If we change the constant term in the latest example to f(top(b), a, g(top(a)), t), then there is no valid substitution becase V would have to match top(b) and top(a) simultaneously, which is not possible. Unification Unification is just like pattern matching, except that both terms can contain variables. So we can no longer say one is the pattern term and the other the constant term. For example: First term: f(a, V, bar(D)) Second term f(D, k, bar(a)) Given two such terms, finding a variable substitution that will make them equivalent is called unification. In this case the substitution is {D=a, V=k}. Note that there is an infinite number of possible unifiers for some solvable unification problem. For example, given: First term: f(X, Y) Second term: f(Z, g(X)) We have the substitution {X=Z, Y=g(X)} but also so...