Prolog：为什么这是一个“坏”的程序？答案

【问题标题】：Prolog: why is this a "bad" program?Prolog：为什么这是一个“坏”的程序？
【发布时间】：2020-02-24 06:34:40
【问题描述】：

max(M,N,M):-M >= N,!.
max(M,N,N).

我正在阅读一本教科书，上面说声明性和程序性含义不同...我不明白。

有人能指出我正确的方向吗？

【问题讨论】：

max(4,3,3) 成功。

标签： prolog

【解决方案1】：

tl;dr：这不是关系。

里面有一个非绿色的切口。其实是红切。要看到这一点，请移除切口，您会注意到您得到了两种不同的解决方案

?- max(1,0,N). % without the cut
   N = 1
;  N = 0.

它将是绿色切割，如果第二个子句是：

max(M,N,N) :- M < N.

切割发生的确切条件是什么？它不是M >= N，而是暗示了一个更进一步的条件，即A1 = A3, ... 这不是直接可见的，因为它仅通过变量的重复出现来显示：

max(M,N,M):-M >= N,!.
        ^
        |
        + hidden equality

通过利用隐藏的相等性，我们可以轻松构建一个不一致的示例：取M 和N 这样M > N 并将N 放在第三个参数中（尽管我们知道这是错误的）。

?- max(1, 0, 0).   % the original version
true.              % very wrong!
?- max(1, non_number, non_number).
true.              % even wronger!
?- max(an-other, non_number, non_number).
true.              % wrongest!!

为了解决这个问题，我们必须在剪辑之后延迟统一。

max(M,N,R):- M >= N,!, R = M.
max(M,N,N).

现在一切都解决了吗？可惜不是……

结果如何？是数字吗？

?- max(1+0,0, R).
   R = 1+0.

并非总是如此。也许宁愿作为定义：

max(M,N,R):- M >= N,!, R is M.
max(M,N,R) :- R is N.

怎么样

?- max(0,N,1).
ERROR: Arguments are not sufficiently instantiated

但是....只有一个解决方案！即N = 1

很复杂，不是吗？好吧，原来，Prolog 根本不做算术。它后来被修补了。当前制定该关系的最佳方法是使用当前的library(clpz)（@SICStus，@Scryer）或其不再维护的因此不太可靠的前身library(clpfd)（@SWI）。

:- op(150, fx, #).   % only needed on SWI
max(M, N, Max) :-
   max(#M,#N) #= #Max.

现在这确实定义了整数的最大关系（但不是浮点数...）。

【讨论】：

【解决方案2】：

我将留给其他人来解释在存在削减的情况下头部参数输出统一的危险。相反，让我们看看谓词未能将第三个参数与前两个参数中的最大值统一起来的情况。我们可以定义max/3谓词应该满足的以下属性：

property(M,N,Max) :-
    (   max(M,N,Max) ->
        Max >= M, Max >= N
    ;   nonvar(Max)
    ).

即如果max/3 成功，则Max 必须等于或大于前两个参数。如果max/3 失败，那一定是由于绑定的第三个参数未能与两个输入参数中的最大值统一。

让我们使用 Logtalk 的 lgtunit 实现快速检查它（您可以在大多数 Prolog 系统上运行；这里我将使用 SWI-Prolog）：

$ swilgt
...

?- {lgtunit(loader)}.
...
% (0 warnings)
true.

?- [user].
|: max(M,N,M):-M >= N,!.
|: max(M,N,N).

Warning: user://1:102:
Warning:    Singleton variables: [M]
|: property(M,N,Max) :-
|:     (   max(M,N,Max) ->
|:         Max >= M, Max >= N
|:     ;   nonvar(Max)
|:     ).
|: ^D% user://1 compiled 0.01 sec, 3 clauses
true.

请注意，我们要生成随机测试，其中前两个参数是整数，但第三个参数可以是变量或整数：

?- lgtunit::quick_check(property(+integer, +integer, ?integer), [n(20000)]).
*     quick check test failure (at test 5484 after 9 shrinks):
*       property(1,0,0)
false.

正如您在报告的失败中看到的那样，当调用绑定所有参数时，您对 max/3 谓词的定义可能会失败。目标max(1,0,0) 与第一个子句的开头不一致。因此，使用第二个子句会导致预期失败的成功目标。

我们可以通过将带有输出参数的统一移动到在剪切之后来纠正错误（由 QuickCheck 暴露）：

max(M,N,Max):- M >= N,!, Max = M.
max(_,N,N).

但是这个定义正确吗？对上述案例的快速测试表明该错误已修复：

?- max(1,0,0).
false.

让我们也快速检查一下（使用相同的属性）：

?- lgtunit::quick_check(property(+integer, +integer, ?integer), [n(20000)]).
% 20000 random tests passed
true.

看起来不错，但请记住：QuickCheck 可以暴露错误但不能证明它们不存在。事实上，如果我们使用默认的测试次数（100），我们可能会错过这个错误。在某些情况下，它有助于使用狭窄的参数进行测试。例如，使用 max/3 的原始、错误的定义：

?- lgtunit::quick_check(
       property(
           +between(integer,-2,2),
           +between(integer,-2,2),
           ?between(integer,-2,2)
       )
   ).
*     quick check test failure (at test 23 after 0 shrinks):
*       property(1,-1,-1)
false.

【讨论】：