Unification algorithm example in WAM (Warren's Abstract Machine)

Question

Exercise 2.2 in Warren's Abstract Machine: A Tutorial Reconstruction

asks for representations for the terms f(X, g(X, a)) and f(b, Y) and then to perform unification on the address of these terms (denoted a1 and a2 respectively).

I've constructed the heap representations for the terms, and they are as follows:

f(X, g(X, a)):
0   STR     1
1           a/0
2   STR     3
3           g/2
4   REF     4
5   STR     1
6   STR     7
7           f/2
8   REF     4
9   STR     3

f(b, Y):
10  STR     11
11          b/0
12  STR     7
13  STR     11
14  REF     14

and I am now asked to trace unify(a1, a2), but following the algorithm on page 20 in 1 I get:

d1 = deref(a1) = deref(10) = 10
d2 = deref(a2) = deref(0) = 0

0 != 10 so we continue

<t1, v1> = STORE(d1) = STORE(10) = <STR, 11>
<t2, v2> = STORE(d2) = STORE(0) = <STR, 1>

t1 != REF and t2 != REF so we continue

f1 / n1 = STORE(v1) = STORE(11) = b / 0
f2 / n2 = STORE(v2) = STORE(1) = a / 0

and now b != a so the algorithm terminated with fail = true,
and thus unification failed, but obviously there exists
a solution with X = b and Y = g(b, a).

Where is my mistake?

score 2 · Accepted Answer · answered Oct 19 '13 at 00:31

I found the solution myself. Here's my corrections:

Each term should have their own definitions of the functors (ie. the f-functor in the second term should not just link to the first f-functor in the first term, but should have its own) and pointers to the terms (a1 and a2) should point to the outermost term functor.

This means that a1 = 6 and a2 = 12 in the following layout

f(X, g(X, a)):
0   STR     1
1           a/0
2   STR     3
3           g/2
4   REF     4
5   STR     1
6   STR     7
7           f/2
8   REF     4
9   STR     3

f(b, Y):
10  STR     11
11          b/0
12  STR     13
13          f/2
14  REF     11
15  REF     15

Unification algorithm example in WAM (Warren's Abstract Machine)

1 Answers1