Re: Prologs with Occurs Check constantly on?

Jan Burse <janburse@xxxxxxxxxxx> writes:
Jan Wielemaker schrieb:
As Ulrich pointed out, the world of unification with occurs-check
combines poorly with the world of cyclic terms. This was the main
conclusion from a debate whether A=f(A), unify_with_occurs_check(A,_)
should succeed or fail.

But in the meantime since 2011-04 or so SWI has a very nice and new
definition failing only for "new cycles". There are some cases still
awaiting perfection, but its seems really the best way to go.

....

I probably don't need to give you examples,
but here is one:

?- X=f(X), Y=f(Y), X=Y.

I guess it will hang in 75% of the Prolog
systems, or is it 95%?

Lets look at X=f(X), Y=f(Y), X\=Y. instead, to avoid
issues with printing the answer.

IF, SWI, YAP, SICStus, Ciao, Eclipse all fail finitely

B, GNU, XSB loop
.

Relevant Pages

  • Re: CLP(FD) team for the ASP solver competition
    ... are identical should fail. ... This fails in SWI. ... When looking at a system with non-terminating constraint propagation, ... Any appropriate simple predefined goal or conjunction of such goals such ...
    (comp.lang.prolog)
  • Re: 3 steps to syntax harmony
    ... SWI gives ... while SICStus gives ... B-Prolog ... ...
    (comp.lang.prolog)