/* To determine whether Prolog does the "occur-check".
** In the following program it is clear that "test" is not a logical 
** consequence of "p(X,f(X))." and "test :- p(Y,Y)." since p(Y,Y) can
** never be unified with "p(X, f(X)", sinc ethe "occur-check" is not
** satisfied. Once the substitution {Y/X} has been done, the next
** disagreement set is {Y, f(Y)}. However since Y occurs in f(Y) a
** substitution such as {f(Y)/Y} can never lead to a unification of
** p(Y, Y) with p(Y, f(Y)). However sinc ethis occur check is not 
** performed and the resulting unification is not verified in any 
** other way, Prolog returns the answer "yes" even though "test" is
** not a logical consequence

*/

p(X,f(X)).
test :- p(Y,Y).

/* Here is the XSB Prolog session.
xsb
[xsb_configuration loaded]
[sysinitrc loaded]
[packaging loaded]

XSB Version 2.4 (Bavaria) of July 13, 2001
[i686-pc-linux-gnu; mode: optimal; engine: chat; gc: copy; scheduling: local]

| ?- [occurcheck].
[Compiling ./occurcheck]
[occurcheck compiled, cpu time used: 0.0590 seconds]
[occurcheck loaded]

yes
| ?- test.

yes
| ?- 


*/

/* The following example shows that if Prolog does the occur check
** then it could easily return the answer "no" for the following.
*/

test2 :- q(X, X).
q(Y, f(Y)) :- q(Y, Y).

/* However Prolog goes off into an infinite loop in the trying to unify,
** because it does not perform the "occur-check"
*/

/* 
		      Difference lists in Prolog
		    ------------------------------
** A difference list is a Prolog structure consisting of two lists, (with 
** possibly uninstantiated components such that the second list is or can be
** a suffix of the first one.
*/


/* With difference lists the append function can sometimes be done in constant
** time, since Prolog uses the uninstantiated variable as endmarker of the 
** difference list
*/

append_dl(X\Y, Y\Z, X\Z).

/* Look at the following execution
| ?- append_dl([1,2,3|X]\X, [4,5]\[], Y).

X = [4,5]
Y = [1,2,3,4,5] \ []

*/

/* Now consider the following

** An implementation without "occur check would allow us to conclude
** that concat([], [], [a]) holds true

*/


test3 :- concat(U\U, V\V, [a|W]\W).
concat(X\Y, Y\Z, X\Z).

/* as indeed it does!

| ?- test3.

yes
| ?- 

*/