통합 알고리즘 예

Question

운동 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 

과 지금의 Unify를 추적하도록 요청하고 (A1, A2), 그러나 20 페이지의 알고리즘에서 다음 1 내가 얻을 :

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

내 실수는 어디에 있습니까?

Answer 1

해결책을 직접 찾았습니다.

각 용어는 펑터에 대한 자체 정의가 있어야합니다 (즉, 두 번째 용어의 f- 펑터는 첫 번째 용어에서 첫 번째 펑터와 연결해서는 안되며 자체적으로 사용해야합니다) 용어 (a1과 a2)에 대한 포인터는 최 외측 용어 펑터를 가리켜 야합니다.

이는 그 다음 배치의 A1 및 A2 = 6 = 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