Prolog中冒泡排序算法的声明式解释

Question

我对 Prolog 中的 BubbleSort 算法的以下实现如何工作有一些疑问。

我非常清楚 BubbleSort 算法是如何工作的，所以我的疑问只与 Prolog 一阶逻辑和声明式解释有关。

这是我的代码：

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).

所以我对这个程序的声明式解释有些怀疑：

程序的核心是 bubbleSort/2 谓词，它执行 List 的扫描，并在其中执行相邻元素的最终交换。

所以 swap/2 谓词就像一个程序 if：

1) 如果子列表 (X) 中的第一个元素按字典顺序跟随子列表 (Y) 中的第二个元素，则不好，因此执行交换。

2) 否则 X 和 Y 的顺序正确，并尝试在子列表 Tail

上执行 te swap

例如，如果我执行以下查询：

[trace]  ?- bubbleSort([3,2,1], Sorted).

我得到：

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

这里调用原始列表中的bubbleSort/2的第一个版本。为 TRUE 调用第一个版本的 swap/2 谓词检查列表的前两个元素是否彼此不按字典顺序，这个事实是 TRUE 所以交换这些元素。现在验证了 swap/2 谓词，通过回溯返回并（为了满足 bubbleSort/2）再次调用 bubbleSort2，现在说原来的list to order 是交换后的列表（第一个和第二个元素交换的列表）

所以再次调用bubbleSort并发生：

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 

所以现在它试图满足列表 [2,3,1] 上的 swap/2 但现在这不是真的，前两个元素彼此不按字典顺序，所以swap/2 谓词的第一个版本失败，因此它使用在子列表 **[3,1] 上简单调用 swap/2 的第二个版本，这是真的3 不跟随 1，所以交换它，我得到 [1,3] 列表。

这里我有第一个疑问：在此子列表上交换之后（从 [3,1] 到 [1,3]），我在这一行中获得了列表：[2,1,3]：

Exit: (9) swap([2, 3, 1], [2, 1, 3]) ? creep 

为什么？这是因为在满足 swap(Tail, Tail1) 谓词之后：

swap([Z|Tail], [Z|Tail1]) :- swap(Tail, Tail1).

我知道 Tail1 是 [1,3] 所以 Z 是旧的头 2 而 [Z|Tail1] 是 [2,1,3] ？

但是，现在结束了冒泡排序算法的第一次扫描，它在列表末尾采用了“更大”的元素

执行以相同的方式继续，但我对程序执行的结束有疑问：

   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].

所以最后在有序列表上调用 bubbleSort/2 谓词：

 Redo: (10) bubbleSort([1, 2, 3], _G399) ? creep

其中 [1,2,3] 是 List1。

现在我处于 bubbleSort/2 谓词的第二版，这个：

bubbleSort(SortedList, SortedList).

其中要排序的列表和排序后的列表是相同的（所以这意味着原始列表是完全排序的）。

那么这是什么？基本情况，一旦验证，程序执行必须结束？

所以执行回溯说所有之前的 bubbleSort/2 都经过验证，直到到达第一个 bubbleSort/2 调用并说这是经过验证并统一排序的[1,2,3] 列表

我的推理正确吗？对此是否有更具声明性的解释？

Answer 1

我认为理解这个算法的关键是当列表排序时 swap/2 失败 - 空列表上没有匹配项。

从这里第二个bubbleSort/2规则的必要性。