Introduction

A most general unifier, usually abbreviated MGU, is the least specific substitution that makes two terms equal. In practice, the classic algorithmic answers are Robinson's unification algorithm and the more rewrite-oriented Martelli-Montanari formulation, with efficient implementations adding data-structure optimizations rather than changing the core logical idea.

What "Most General" Means

Suppose you want to unify f(x, a) with f(b, y). One valid substitution is x = b, y = a, which makes both terms f(b, a).

That substitution is a unifier. It is also most general because it does not commit to anything more specific than necessary. Any more specific unifier would be an instance of it.

This matters because logic programming, theorem proving, and type inference want a reusable answer, not just any arbitrary matching.

Robinson's Core Algorithm

Robinson's algorithm works by repeatedly simplifying a set of equations between terms.

The core cases are:

• if two symbols are identical constants, continue
• if one side is a variable, bind it if safe
• if both sides are compound terms with the same functor and arity, decompose their arguments into more equations
• otherwise, fail

The "safe" part is the occurs check: a variable cannot be bound to a term that already contains that variable.

For example, x = f(x) must fail, or you create an infinite term.

A Small Runnable Python Implementation

Here is a minimal unifier for symbolic terms represented as tuples such as ("f", "x", "a").

1from collections import deque
2
3
4def is_variable(term):
5    return isinstance(term, str) and term.startswith("?")
6
7
8def apply(subst, term):
9    if is_variable(term):
10        while is_variable(term) and term in subst:
11            term = subst[term]
12        return term
13    if isinstance(term, tuple):
14        return tuple(apply(subst, part) for part in term)
15    return term
16
17
18def occurs(var, term, subst):
19    term = apply(subst, term)
20    if var == term:
21        return True
22    if isinstance(term, tuple):
23        return any(occurs(var, part, subst) for part in term)
24    return False
25
26
27def unify(t1, t2):
28    equations = deque([(t1, t2)])
29    subst = {}
30
31    while equations:
32        left, right = equations.popleft()
33        left = apply(subst, left)
34        right = apply(subst, right)
35
36        if left == right:
37            continue
38
39        if is_variable(left):
40            if occurs(left, right, subst):
41                raise ValueError("occurs check failed")
42            subst[left] = right
43            continue
44
45        if is_variable(right):
46            if occurs(right, left, subst):
47                raise ValueError("occurs check failed")
48            subst[right] = left
49            continue
50
51        if isinstance(left, tuple) and isinstance(right, tuple):
52            if len(left) != len(right) or left[0] != right[0]:
53                raise ValueError("functor mismatch")
54            equations.extend(zip(left[1:], right[1:]))
55            continue
56
57        raise ValueError("cannot unify")
58
59    return {k: apply(subst, v) for k, v in subst.items()}
60
61print(unify(("f", "?x", "a"), ("f", "b", "?y")))

This prints:

{'?x': 'b', '?y': 'a'}

That is the MGU for the example.

Why The Occurs Check Matters

It is tempting to skip the occurs check for speed, and some practical systems do under restricted assumptions. But algorithmically, the full unification problem includes it.

Without the occurs check, unifying ?x with ("f", "?x") would succeed incorrectly and create cyclic structure. In pure first-order unification, that is not allowed.

So if the question is about the correct general algorithm, the occurs check is part of the answer.

Martelli-Montanari As A Standard Presentation

When people ask for the "optimal" MGU algorithm, the more precise answer is often Martelli-Montanari. It expresses unification as a sequence of rewrite rules on an equation set:

• delete identical equations
• orient variable equations to the left
• eliminate by substitution
• decompose compound terms
• fail on conflicts or occurs-check violations

This is not a completely different idea from Robinson. It is a cleaner algorithmic formulation that is easier to analyze and implement efficiently.

What "Optimal" Usually Means Here

There is no single magical answer that is optimal in every implementation setting. Practical performance depends on:

• how terms are represented
• whether substitutions are applied eagerly or lazily
• whether a union-find style structure is used
• whether the occurs check is full, partial, or omitted under domain assumptions

So the right expert answer is usually:

• conceptually: Robinson unification computes MGUs
• algorithmically: Martelli-Montanari is a standard efficient formulation
• implementation-wise: optimized term and substitution data structures dominate performance

Where MGUs Are Used

MGUs show up in several places:

• Prolog and logic programming
• type inference for polymorphic languages
• automated theorem provers
• symbolic algebra systems

The reason the MGU matters is compositionality. Once you have the most general solution, other compatible solutions can be obtained by specializing it.

Common Pitfalls

• Calling any successful substitution an MGU without checking whether it is unnecessarily specific.
• Ignoring the occurs check and then claiming full first-order unification correctness.
• Treating functor mismatch as something a substitution can repair when the heads and arities already disagree.
• Confusing pattern matching with full unification; pattern matching is one-sided and simpler.
• Asking for one "optimal" implementation without specifying the term representation and performance model.

Summary

• An MGU is the least specific substitution that makes two terms equal.
• Robinson's unification algorithm is the classic foundation.
• Martelli-Montanari is a standard efficient rewrite-based formulation.
• The occurs check is required for fully correct first-order unification.
• Real performance depends as much on representation choices as on the abstract algorithm name.