I've got here a small script, that converts list of elements into a set. For example list [1,1,2,3] -> set [1,2,3]. Can somebody explain to me, step by step, whats happening inside those procedures? Can you please use my [1,1,2,3] -> [1,2,3] example?
list_to_set([],[]).
list_to_set([A|X],[A|Y]):-
list_to_set(X,Y),
\+member(A,Y).
list_to_set([A|X],Y):-
list_to_set(X,Y),
member(A,Y).
The procedural counterpart of a prolog program is called SLDNF. Query:
list_to_set([1,1,2,3], Result)
Now SLDNF tries to match [1,1,2,3] with [A|X] through a procedure called unification. In a few words, it checks whether variable can be instantiated. [A|X] is a shortcut, it means (loosely): "A is the first element and X is the rest". This can be done if A= 1 and X = [1,2,3] and Result = [1 |Y]. If the unification succeeds then we use the same substitution in the body of the rule (what appears after :-). You may wonder why are we using the second clause but not the third or the first? Prolog actually tries all of them, tryign to emulate a nondeterministic choice. procedurally though it tries them in order. The first clause can't be unified (A = ?, there's nothing in the list). The third clause will be checked later if our first attempt fails. Let's call it "choice point 1", because Prolog has this open path that leaves unexplored and that can use if the paths that have been chosen so far fail.
Now SLDNF has reduced your initial query to:
list_to_set([1,2,3], Y2), \+ member(1, Y2) {Result = [1 | Y2]}
(Variables can be renamed, and we do it to avoid confusion with the program) This is where the magic happens. SLDNF now does the same thing as before but with a slightly different input [1,2,3]. Recursion at its best. So it tries to unify it with the first clause but it fails again. It succeeds with the second, and similarly you'll get that instead of the first element of the query (called literal) we have again the body, with the variable substitution X = [2, 3], A = 1, Y2 = [1 | Y].
Now we have
list_to_set([2,3], Y), \+ member (1,Y), \+ member(1, [1 | Y]) {Result = [1 | [1 | Y]]}
I'm not continuing until the end. Eventually we'll end up checking + member(1, [1 | Y]), which means "1 is not member of a list with head 1 and tail Y". This is a build in predicate and will fail, because 1 is in that list (it's the head). Prolog will go back to a choice point end eventually arrive at "choice point 1". Here the last condition in the clause is "A is member of Y". You can check yourself that this path will succeed eventually.
Sorry for the lengthy hurried answer, I hope it helps.