I have some doubt about how work the following implementation of BubbleSort algorithm in Prolog.
I have very clear how BubbleSort algorithm work so my doubt is only related to the Prolog first order logic and declarative interpretation.
This is my code:
bubbleSort(List, SortedList) :- swap(List, List1),
!,
bubbleSort(List1, SortedList).
bubbleSort(SortedList, SortedList).
/* swap predicate swap the two element if X come after Y in lexicographical order */
swap([X,Y|Tail], [Y,X|Tail]) :- X @> Y.
/* If it is not true that X come after Y in lexicographical order let the head in its
original position and call the swap predicate on the sublist */
swap([Z|Tail], [Z|Tail1]) :- swap(Tail, Tail1).
So I have some doubt about declarative interpretation of this program:
The core of the program is the bubbleSort/2 predicate that perform the scansion of List in which are performed eventual swap of adjacent elements.
So swap/2 predicate work like a procedural if:
1) IF the first element in the sublist (X) follow the second element in the sublist (Y) in the lexicographical order it is not good, so perform the swap.
2) Otherwise X and Y are in the right order and try to execute te swap on the sublist Tail
So for example if I perform the following query:
[trace] ?- bubbleSort([3,2,1], Sorted).
I obtain:
Call: (7) bubbleSort([3, 2, 1], _G399) ? creep
Call: (8) swap([3, 2, 1], _G478) ? creep
Call: (9) 3@>2 ? creep
Exit: (9) 3@>2 ? creep
Exit: (8) swap([3, 2, 1], [2, 3, 1]) ? creep
Call: (8) bubbleSort([2, 3, 1], _G399) ? creep
Here call the first version of bubbleSort/2 on the original list. To be TRUE call the first version of swap/2 predicate that check if the first two elements of the list are not in lexicographical order each other, this fact is TRUE so swap these elements. Now that swap/2 predicate is verified, come back by backtracking and (to satisfy bubbleSort/2) call again bubbleSort2 saying now that the original list to order is the list after the swap (the list in which the first and the second element are swapped)
So call again bubbleSort and happen:
Call: (8) bubbleSort([2, 3, 1], _G399) ? creep
Call: (9) swap([2, 3, 1], _G484) ? creep
Call: (10) 2@>3 ? creep
Fail: (10) 2@>3 ? creep
Redo: (9) swap([2, 3, 1], _G484) ? creep
Call: (10) swap([3, 1], _G480) ? creep
Call: (11) 3@>1 ? creep
Exit: (11) 3@>1 ? creep
Exit: (10) swap([3, 1], [1, 3]) ? creep
Exit: (9) swap([2, 3, 1], [2, 1, 3]) ? creep
So now it try to satisfy swap/2 on the list [2,3,1] but now this is not true that the first two elements are not in lexicographical order each other, so the first version of swap/2 predicate fail, so it use the second version that simply call swap/2 on the sublist **[3,1] where it is true that 3 don't follow 1, so swap it and I obtain the [1,3] list.
Here I have the first doubt: after this swap on this sublist (from [3,1] to [1,3]) I obtain the list: [2, 1, 3] in this line:
Exit: (9) swap([2, 3, 1], [2, 1, 3]) ? creep
why? is this because after have satisfied swap(Tail, Tail1) predicate:
swap([Z|Tail], [Z|Tail1]) :- swap(Tail, Tail1).
I have that Tail1 is [1,3] so Z was the old head 2 and [Z|Tail1] is [2,1,3] ?
However, now it is end the first scansion of the bubble sort algorithm that have take the "bigger" element at the end of the list
The execution continues in the same way but I have a doubt about the end of the program execution that is:
Redo: (10) bubbleSort([1, 2, 3], _G399) ? creep
Exit: (10) bubbleSort([1, 2, 3], [1, 2, 3]) ? creep
Exit: (9) bubbleSort([2, 1, 3], [1, 2, 3]) ? creep
Exit: (8) bubbleSort([2, 3, 1], [1, 2, 3]) ? creep
Exit: (7) bubbleSort([3, 2, 1], [1, 2, 3]) ? creep
Sorted = [1, 2, 3].
So at the end call the bubbleSort/2 predicate on an ordered List by:
Redo: (10) bubbleSort([1, 2, 3], _G399) ? creep
where [1,2,3] is List1.
Now I am in the second version of bubbleSort/2 predicate, this one:
bubbleSort(SortedList, SortedList).
where the list to sort and the sorted list is the same (so it means that the original list is totatly sorted).
So what is this? the base case that, once verified, say that the program execution have to end?
So execute backtracking to say that all the previous bubbleSort/2 are verified, untill reach the first bubbleSort/2 call and say that this is vierified and unify Sorted with [1,2,3] list
Is my reasoning correct? Are there a more declarative interpretation of this?