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?
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