ISO/IEC JTC1 SC22 WG17
Comparison of implementations of dif/2

ISO Prolog works.

# Query Answer dif_si/2 IV SICStus ECLiPSe IF YAP B SWI Scryer Trealla
# Query, quads answer description
dif_si/2 IV SICStus ECLiPSe IF YAP B SWI Scryer Trealla
introduced Œdipe 0.6 Sepia <2.10 V5.0 <6.4 5.5.3
date 1972-05 1987 <1989-04 <1996-05 <2000 <2003 2004-03 2019-02 2021-04
conforming extension via 5.5.9 and 5.5.11 yes yes yes yes yes yes yes yes yes yes
strictly conforming extension5.1 e built-in built-in library
prolog_extras 		library
const_delay 		neither built-in default
dif 		library
dif 		library
dif new
e1 ?- asserta(dif(1,1)), dif(1,2).% in 5.1 efalse. p._e.(m.,st.,_) p._e.(m.,st.,_) OK OK true p._e.(m.,st.,_) OK OK OK
e2 ?- dif(1,2).% in 5.1 eexistence_error(procedure,dif/2). true true OK OK true true true OK OK new
consistency n/a full full full weak full full full full full
term-termination n/a yes yes yes yes yes yes partial yes yes
tree-termination n/a yes yes no no yes no partial yes yes
display of constraints i._e no 2 yes yes no 3 yes no 1 yes yes yes
call_residue_vars/2 no yes call_residue/2 no yes no yes yes yes
redundant constraints ? no yes ? no ?no no no new no new
1 ?- dif(1,2). true. OK OK OK OK OK OK OK OK OK OK
2 ?- dif(1,Y), Y=1. false. OKR OK OK OK OK OK OK OK OK OK
3 ?- dif(1,Y), Y=2. Y=2. OKR OK OK OK OK OK OK OK OK OK
4 ?- dif(X,-Y), X= -Y. false. OKR OK OK OK OK OK OK OK OK OK
5 ?- dif(X,Y), X=Y. false. OKR OK OK OK true OK OK OK OK OK
6 ?- dif(X,Y), X=Y, X=1. false. OKR OK OK OK OK OK OK OK OK OK
7 ?- dif(-X,-Y), X=Y. false. OKR OK OK OK true OK OK OK OK OK
8 ?- dif(-X,-Y), X=Y, X=1. false. OKR OK OK OK OK OK OK OK OK OK
9 ?- dif(-X,X). trueo2 | maybet7. sto OK2 OK OK true OK true OK OK OK
10 ?- dif(-X,Y), X=Y. trueo2 | maybet7. stoR OK2 OK OK true OK true OK OK OK
11 ?- X=Y, dif(X-Y,1-2). X=Y. OK OK OK OK OK X=X OK OK OK OK
12 ?- dif(X-Y,1-2), X=Y. X=Y. OKR OK OK ,X-X~=1-2 3 X=X OK OK OK new OK new
13 ?- X=Y, Y=1, dif(X-Y,1-2). X=1, Y=1. OK OK OK OK OK OK OK OK OK OK
14 ?- dif(X-Y,1-2), X=Y, Y=1. X=1, Y=1. OKR OK OK OK OK OK OK OK OK OK
15 ?- dif(X-Y,1-2), X=Y, X=2. X=2, Y=2. OKR OK OK OK OK OK OK OK OK OK
16 ?- dif(A-C,B-D), C-D=z-z, A-B=1-2. A=1, C=z, B=2, D=z. OKR OK OK OK OK OK OK OK OK OK
17 ?- A-B=1-2, C-D=z-z, dif(A-C,B-D). A=1, B=2, C=z, D=z. OK OK OK OK OK OK OK OK OK OK
18 ?- dif(A,[C|B]), A=[[]|_], A=[B]. A=[[]], B=[], dif([[]],[C]). i._e ..., dif(C,[]).2 OK OK A=[[]], B=[] OK A=[[]], B=[] OK OK OK
19 ?- dif([E],[/]), E=1. E=1. OKR OK OK OK OK OK OK OK OK OK
20 ?- dif([a],B), B=[_|_], B=[b]. B=[b]. OKR OK OK OK OK OK OK OK OK OK
21 ?- dif([],A), A = [_]. A = [_A]. OKR OK OK OK OK OK OK OK OK new OK new
22 ?- A = [_], dif([],A). A = [_A]. OK OK OK OK OK OK OK OK OK OK
23 ?- dif(X,a), copy_term(X,a). maybe | false. i._e maybe maybe maybe maybe aborts maybe false false false
24 ?- findall(X,dif(X,a),[a]). true | false. i._e true true false true true true false false false
25 ?- setof(t,dif(X,a),_), X = a. X = a | false. i._e X=a X=a false X=a X=a X=a false false X=a
26 ?- setof(t,(dif(X,a);dif(X,b)),_), X = a. X = a. i._e X=a X=a false X=a X=a X=a false false X=a
Rational tree unification
t1 ?- \+ \+ -X=X. sto, true. OK OK OK OK OK OK OK OK OK
t2 ?- -X=X, -Y=Y, X\=Y. sto, false. OK OK loops OK OK loops OK OK OK
t3 ?- -X=X, dif(X,1). sto, X = -X. OK OK OK OK OK OK OK OK OK OK
t4 ?- -X=X, -Y=Y, dif(X,Y). sto, false. OK OK OK loops OK OK loops OK OK OK
t5 ?- dif(X,Y), -X=X, -Y=Y. sto, false. OKR OK OK loops loops OK loops OK OK OK
t6 ?- A=[[]|A],dif(A,B),B=[[]|A]. sto, false. OKR OK OK OK loops OK loops OK OK OK
t7 ?- dif(-X,X),-Y=Y,X=Y. sto, false. OKR OK OK OK OK OK loops OK OK OK
t8 ?- -X=X, dif(X,Y),X=Y. sto, false. OKR OK OK OK loops OK loops OK OK OK
Occurs-check unification
o1 ?- -X=X. sto, false. OK OK OK
o2 ?- dif(-X,X). true. OK OK OK OK
o3 ?- dif(-X,Y), X=Y. Y = X. OKR OK OK new OK new

Notes

– The following reference implementation is used. Either directly (OK) or after reordering goals (OKR). An instantiation error is an indication for pending constraints. 
dif_si(X, Y) :-
   X \== Y,
   (  X \= Y -> true
   ;  throw(error(instantiation_error,_Imp_def))
   ).
1 B Prolog worked in 7.1b5.1, no display in 7.3 up to 8.1
2 Prolog IV has an internal mechanism to obtain the constraints attached to specific variables, but no way to obtain such variables. 
?- dif(X-Y,1-2),X=Y,symbolic_cstrbis([X,Y], V1,V2,V3,V4,V5,V6).
   A ex
      V6 = true, V5 = true, V4 = true, V3 = true, V2 = true, V1 = [A,A], X = Y, Y ~ tree, A ~ tree.
?- dif(X-Y,1-2), symbolic_cstrbis([X,Y], V1,V2,V3,V4,V5,V6).
   A ex B ex 
      V6 = true, V5 = true, V4 = true, V3 = true,
      V2 = difrat([B,A],[1,2]),
      V1 = [B,A], Y ~ tree, X ~ tree, A ~ tree, B ~ tree.
?- symbolic_cstrbis([X,Y], V1,V2,V3,V4,V5,V6).
   V6 = true, V5 = true, V4 = true, V3 = true, V2 = true, V1 ~ [tree,tree], Y ~ tree, X ~ tree.
3 IF/Prolog has is_constraint/1 to test for the presence of constraints.
Relevant clauses: 7.3 Unification,

Excluded: means to enable dif/2 similar to Prolog prologue.

Open: Interaction with subsumes_term/2

Version Control, Validated HTML