First-order unification
Find the substitution that makes two logical terms identical, including the occurs check.
def is_variable(term):
return isinstance(term, str) and term[:1].islower()
def occurs(var, term, theta):
if var == term:
return True
if is_variable(term) and term in theta:
return occurs(var, theta[term], theta)
if isinstance(term, tuple):
return any(occurs(var, item, theta) for item in term)
return False
def unify_var(var, term, theta):
if var in theta:
return unify(theta[var], term, theta)
if is_variable(term) and term in theta:
return unify(var, theta[term], theta)
if occurs(var, term, theta):
return None
return {**theta, var: term}
def unify(x, y, theta):
if theta is None:
return None
if x == y:
return theta
if is_variable(x):
return unify_var(x, y, theta)
if is_variable(y):
return unify_var(y, x, theta)
if isinstance(x, tuple) and isinstance(y, tuple) and len(x) == len(y):
for a, b in zip(x, y):
theta = unify(a, b, theta)
return theta
return None
print(sorted(unify(("Knows", "John", "x"), ("Knows", "y", "Mary"), {}).items()))
print(unify(("P", "x"), ("P", ("F", "x")), {}))
print(unify(("Knows", "John"), ("Likes", "John"), {}))
print(sorted(unify(("P", "x", "x"), ("P", "y", "Z"), {}).items()))[('x', 'Mary'), ('y', 'John')]
None
None
[('x', 'y'), ('y', 'Z')]Explanation
First-order logic adds objects, predicates, functions, and variables to propositional logic, so it can say, for example, that everyone who knows John likes him. To apply a rule such as Knows(John, x) to a fact such as Knows(y, Mary), an inference system must find a substitution for the variables that makes the two expressions identical. Finding it is called unification, and the substitution is a unifier. A most general unifier (MGU) is the least restrictive one; for example, x = Mary and y = John unifies the two sentences above.
The algorithm compares the two terms. Identical terms need nothing. A variable unifies with any term by binding to it, provided the variable does not occur inside that term: that is the occurs check, which stops x from unifying with F(x), since no finite term equals a term that contains itself. Compound terms unify if their function or predicate symbols match and all their arguments unify under the substitution built so far. Anything else fails.
In the code a variable is a lowercase string, a constant, predicate or function name is capitalized, and a compound term is a tuple whose first item is the symbol. The final example unifies P(x, x) with P(y, Z). The result {x: y, y: Z} is in triangular form: applying the substitution repeatedly resolves x to y and then y to Z. Unification is the core operation of resolution in first-order logic and of the execution of Prolog programs.
Explore the dry run
def is_variable(term): return isinstance(term, str) and term[:1].islower() def occurs(var, term, theta): if var == term: return True if is_variable(term) and term in theta: return occurs(var, theta[term], theta) if isinstance(term, tuple): return any(occurs(var, item, theta) for item in term) return False def unify_var(var, term, theta): if var in theta: return unify(theta[var], term, theta) if is_variable(term) and term in theta: return unify(var, theta[term], theta) if occurs(var, term, theta): return None return {**theta, var: term} def unify(x, y, theta): if theta is None: return None if x == y: return theta if is_variable(x): return unify_var(x, y, theta) if is_variable(y): return unify_var(y, x, theta) if isinstance(x, tuple) and isinstance(y, tuple) and len(x) == len(y): for a, b in zip(x, y): theta = unify(a, b, theta) return theta return None print(sorted(unify(("Knows", "John", "x"), ("Knows", "y", "Mary"), {}).items()))print(unify(("P", "x"), ("P", ("F", "x")), {}))print(unify(("Knows", "John"), ("Likes", "John"), {}))print(sorted(unify(("P", "x", "x"), ("P", "y", "Z"), {}).items()))Follow the example
Start to inspect the source, values, and output. These prepared steps explain the published sample; grouped loop steps describe multiple iterations.
View the complete dry-run table
| Step / line | What happens | State after step | Output so far |
|---|---|---|---|
| A variable can be bound to the other term, unless the occurs check or an existing binding forbids it. | — | — | |
| Occurs check: x cannot be bound to F(x) because it would require an infinite term. | — | — | |
| John matches y and x matches Mary: the unifier is {x: Mary, y: John}. | — | [('x', 'Mary'), ('y', 'John')] | |
| x would have to equal F(x), which fails the occurs check, so there is no unifier. | — | [('x', 'Mary'), ('y', 'John')]
None | |
| Different predicate symbols can never match. | — | [('x', 'Mary'), ('y', 'John')]
None
None | |
| x binds to y, then the second x forces y to unify with Z: a chain {x: y, y: Z}. | — | [('x', 'Mary'), ('y', 'John')]
None
None
[('x', 'y'), ('y', 'Z')] |
Cost and common mistakes
With the occurs check, simple implementations can take exponential time on some inputs; algorithms with shared structure (Martelli–Montanari, Paterson–Wegman) run in nearly linear time.
- Skipping the occurs check makes unification unsound in some cases. Some Prolog systems omit it for speed.
- The naming convention matters: in this code a lowercase function or predicate name would be mistaken for a variable.
- A unifier may be returned in triangular form. Apply it repeatedly, or compose it, to obtain the fully substituted terms.
Try it yourself
Do Knows(John, x) and Knows(x, Mary) unify?
Reveal answer and reasoning
No. x would have to be John from the first argument and Mary from the second, and John ≠ Mary. Standardizing apart (renaming the variables in one sentence) is what makes the earlier example unify.