Unbound variable unification in Prolog

In a logical language like Prolog, the statement X = Y doesn't mean that the value of Y is assigned to X, it means that both variables are now aliases to the same value.

X = Y

That means that after

X = Y

X = 5

?Y

will yield 5, and alternatively, that after

X = Y

Y = 2

?X

will yield 2.

But this post is not about Prolog. It's just about that feature of Prolog, and how it works, internally.

I will start with an example that shows the problem, proceed with an algorithm, and end with some caveats.

An example

Let's make A and B aliases, and C and D as well. Then assign 3 to D, and end by making B and C aliases.

A = B

C = D

D = 3

B = C

?A

All 4 variables are then aliases and will yield the same value: 3.

How does that work? 

The algorithm

The following algorithm is a stripped down version of unification, that focuses on variable unification. I asked ChatGPT to come up with an algorithm, as I could not find a simple algorithm via Google Search.

unify(X, Y):
    X = deref(X)
    Y = deref(Y)

    if X == Y:
        succeed

    else if X is unbound variable:
        Heap[X] = Y
        succeed

    else if Y is unbound variable:
        Heap[Y] = X
        succeed

    else if both are integers:
        succeed if equal, else fail

    else:
        fail

In this algorithm Heap is the location where variables are stored, and deref (dereference) follows a chain of variables to the end. = here is just assignment.

The value of a variable may be another variable, and this is the basis of the algorithm.

A free variable is represented as a variable that has itself as a value (for example: X: X). 

Deref example: if F has value G and G has value H and H has value 13, the deref of F yields 13

Thus the algorithm starts by replacing X and Y by their dereferenced values. If they match, unification succeeds. If one variable is still free, after dereferencing, it takes the other variable as its value. If both variables are free, only one is bound to the other.

Example - continued

Let's go through the example:

initially: A: A, B: B, C: C and D: D (all variables are free)

A = B

now A: B, and B: B

C = D

now C: D and D: D (and A: B, and B: B)

D = 3

now C: D and D: 3 (and A: B, and B: B)

B = C

now A: B, and B: C and C: D and D: 3

?A

dereferencing A yields B → C → D → 3

Caveats

• The algorithm does not take into account the "occurs check" for A = f(A); many systems don't do this check, but it's good to be aware of it.