list - 可逆合并

Question

我们可以按如下方式合并两个排序列表

merge_([A|T], [], [A|T]).
merge_([], [A|T], [A|T]).
merge_([A|T], [B|U], [A|V]) :- A @< B, merge_(T, [B|U], V).
merge_([A|T], [B|U], [B|V]) :- A @>= B, merge_([A|T], U, V).

在一个方向上工作正常。不适用于此定义的是如下查询 merge_(A, [a, b, c], [a, b, c, d]). ，尽管有独特且非常明显的解决方案 A = [d]. .甚至迭代 merge_(A, B, [a, b, c]).应该产生相当简单的结果集: A被排序 [a, b, c] 的子集和 B = [a, b, c] \ A .

如何更改 merge_ 的定义让它在各个方向都发挥作用？

Answer 1

谓词 (@<)/2和 (@>=)/2是 不单调 ，因此不会表现出正确描述“合并”一般含义所必需的属性。使用此类谓词的程序可能在特定情况下工作，但通常通常会产生不正确的结果。

为了向您展示问题的本质，这些谓词违反了以下重要的声明性属性:

Adding a goal can at most reduce, never extend, the set of solutions.

这些属性打破了这种单调性，例如:

?- Y @< X。
错误的。

不存在解决方案 ， 是的？特别是肯定 X=1 , Y=0是 不是 一个解决方案，对吧？走着瞧:

?- X=1, Y=0, Y @< X。
X = 1,
Y = 0。

什么？我们只是被告知没有任何解决方案!

换句话说，在处理这些谓词时，我们甚至无法应用最基本的逻辑推理。因此，在我看来，如果您想最大程度地享受逻辑编程的好处，最好避免使用此类谓词。

约束 提供摆脱这种困惑的方法。约束在所有实例化模式中都能正常工作，并允许在所有方向上工作的更通用的程序。

这是一个描述 列表合并的程序整数 , 使用 中电(FD) 约束:

合并_([A|T], [], [A|T])。
合并_([], [A|T], [A|T])。
merge_([A|T], [B|U], [A|V]) :- A #< B, merge_(T, [B|U], V).
merge_([A|T], [B|U], [B|V]) :- A #>= B, merge_([A|T], U, V)。

您引用的示例的整数类比:

?- 合并_(A, [1,2,3], [1,2,3,4])。
A = [4]。

因此，这完全按预期工作。唯一的缺点:它要求我们将想要推理的实体映射到整数。实际上，很多程序在任何情况下都会对整数进行推理，因此这通常是可以接受的。

对于其他领域，类似的概括也是可能的。但是，整数是最常用的域之一，因此所有广泛使用的 Prolog 系统都附带 CLP(FD) 约束，我建议将其作为此类问题的有用起点甚至解决方案。

顺便说一句，如果您仅使用 CLP(FD) 约束，您引用的另一个示例也完全按预期工作:

?- 合并_(A, B, [1,2,3])。
A = [1, 2, 3],
B = [] ;
A = [],
B = [1, 2, 3] ;
A = [1]，
B = [2, 3] ;
A = [1, 2],
B = [3] ;
等等。