3

Warren 的抽象机器中的练习 2.2 ：教程重构

要求对术语 f(X, g(X, a)) 和 f(b, Y) 进行表示，然后对这些术语的地址进行统一（分别表示为 a1 和 a2）。

我已经为这些术语构建了堆表示，它们如下：

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

现在我被要求跟踪统一（a1，a2），但是按照第 20 页的算法，我得到：

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

我的错误在哪里？

4

1 回答 1

2

我自己找到了解决方案。这是我的更正：

每个术语都应该有自己的函子定义（即第二项中的 f 函子不应该只链接到第一项中的第一个 f 函子，而是应该有自己的）和指向项的指针（a1 和a2) 应该指向最外层的函子。

这意味着在以下布局中 a1 = 6 和 a2 = 12

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
于 2013-10-19T00:31:32.177 回答