Python · Course navigation

First-order unification

Find the substitution that makes two logical terms identical, including the occurs check.

On this page

Before you start

Recursion, dictionaries, and tuples.

Find the substitution that makes two logical terms identical, including the occurs check.
Predict the sample output and explain the state changes.
Complete the practice task and check the boundary cases.

The concept

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.

Code example

Python

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()))

Output

[('x', 'Mary'), ('y', 'John')]
None
None
[('x', 'y'), ('y', 'Z')]

Example details

Follow the code

Open the walkthrough to inspect the example one step at a time.

Show guided walkthrough

Guided walkthroughReady

1def is_variable(term):

2 return isinstance(term, str) and term[:1].islower()

5def occurs(var, term, theta):

6 if var == term:

7 return True

8 if is_variable(term) and term in theta:

9 return occurs(var, theta[term], theta)

10 if isinstance(term, tuple):

11 return any(occurs(var, item, theta) for item in term)

12 return False

15def unify_var(var, term, theta):

16 if var in theta:

17 return unify(theta[var], term, theta)

18 if is_variable(term) and term in theta:

19 return unify(var, theta[term], theta)

20 if occurs(var, term, theta):

21 return None

22 return {**theta, var: term}

25def unify(x, y, theta):

26 if theta is None:

27 return None

28 if x == y:

29 return theta

30 if is_variable(x):

31 return unify_var(x, y, theta)

32 if is_variable(y):

33 return unify_var(y, x, theta)

34 if isinstance(x, tuple) and isinstance(y, tuple) and len(x) == len(y):

35 for a, b in zip(x, y):

36 theta = unify(a, b, theta)

37 return theta

38 return None

41print(sorted(unify(("Knows", "John", "x"), ("Knows", "y", "Mary"), {}).items()))

42print(unify(("P", "x"), ("P", ("F", "x")), {}))

43print(unify(("Knows", "John"), ("Likes", "John"), {}))

44print(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

Prepared trace of the published program. Some rows group repeated iterations.
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')]

Behind the scenes

How Python processes this code

Python runs this source through its interpreter. It creates objects for values and resolves names as each statement runs.

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.