Variable value not found
Closed this issue · 1 comments
flexoron commented
v2.39.2
$ tpl
?- X = [Z,1|Z],append([Z],[Z|Z],[X,Z,Z,Y|Z]),write(Y),nl.
_2 % unexpected
X = [Z,1|Z], Z = [Z,1|Z]. % Y = 1 not found
?-
Howto find Y = 1
?- X = [Z,1|Z],append([Z],[Z|Z],[X,A,A,Y|Z]),write(Y),nl.
_3
X = [Z,1|Z], Z = [Z,1|Z], A = [Z,1|Z]. % Not yet
?- X = [Z,1|Z],append([Z],[Z|Z],[X,A,B,Y|Z]),write(Y),nl.
1
X = [Z,1|Z], Z = [Z,1|Z], A = [Z,1|Z], B = [Z,1|Z], Y = 1. % Now, involving Z = A = B (= valuable scrap)
?- X = [Z,1|Z],append([Z],[Z|Z],[X,_,_,Y|Z]),write(Y),nl. % scrap scrapped
1
X = [Z,1|Z], Z = [Z,1|Z], Y = 1.
infradig commented
Simplifying
?- append([Z],[Z|Z],[[Z,1|Z],Z,Z,Y|Z]).
Z = [Z,1|Z].
Then changing the definition of
append([], R, R).
append([X|L], R, [X|S]) :- append(L, R, S).
to
append([], R, R).
append([X1|L], R, [X2|S]) :- append(L, R, S), X1 = X2.
gives
?- append([Z],[Z|Z],[[Z,1|Z],Z,Z,Y|Z]).
Z = [Z,1|Z], Y = 1.
So something in unification involving, you guessed it, cyclic terms it seems.