prolog - 当谓词回溯到相同的解决方案时，使用切割是否有意义？

Question

我正在编写一个简单的矩阵库，我偶然发现了一个解决方案，它提供了一个了解切割目的的机会。

boolean_mult(1,1,1).
boolean_mult(1,0,0).
boolean_mult(0,1,0).
boolean_mult(0,0,0).

binary_dot_product([B1],[B2],Solution) :-
    boolean_mult(B1,B2,Solution).
binary_dot_product([1|_],[1|_],1). % computation can end here.
binary_dot_product([_|B1s],[_|B2s],Solution) :-
    binary_dot_product(B1s,B2s,Solution).

从声明性的角度来看，这个解决方案是有意义的。给定两个 1 和 0 的列表，B1 和 B2，如果它们头部的 bool 积为 1，则列表的点积为 1。否则取它们尾部的点积。单例列表的点积是两个元素的 bool 积。
我遇到的问题显示在这个查询中:

?- binary_dot_product([1,0,1],[1,1,1],X).
X = 1 ;
X = 1 ;
X = 1.

我能够回溯三次，从声明的角度来看这是没有意义的。只能有一个点积!不是3!
我可以通过使用 cut 轻松解决这个问题:

binary_dot_product([B1],[B2],Solution) :-
    boolean_mult(B1,B2,Solution).
binary_dot_product([1|_],[1|_],1) :- !. 
binary_dot_product([_|B1s],[_|B2s],Solution) :-
    binary_dot_product(B1s,B2s,Solution).

现在:

?- binary_dot_product([1,0,1],[1,1,1],X).
X = 1.

到目前为止，在我的 Prolog 职业生涯中，我已经避免了像瘟疫一样的削减，因为我已经被警告过它们的危险。在这种情况下，虽然我觉得裁员很有意义。
在上面的代码中使用 cut 会得到什么和失去什么？

Answer 1

编辑(因为 OP 坚持;-)
我在回答这个问题:

What am I gaining and losing from a use of a cut in the above code?

我不确定你得到了什么。如果您不在代码中使用剪切，您将失去提出免费获得的更一般性问题的能力。
在一般情况下，多次获得相同的正确解决方案强烈表明您的代码，无论是否有删减，要么是多余的，要么是完全错误的。这当然不是普遍正确的，但从经验来看，它经常是正确的。

你不应该“像瘟疫一样避免削减”。你应该在你需要的时候使用它们，而不是在你不需要它们的时候使用它们。
这是一个太大的话题，无法在 SO 上回答。每一本像样的 Prolog 教科书都解释了削减和讨论何时需要它们以及为什么；并使用您的判断力，这将随着您的编程而改进。
但是:如果您的程序在没有切割的情况下是不正确的，则切割不会修复它。

考虑这些问题。

给定两个 bool 向量，它们的点积是多少？

实现一个带有三个参数的谓词。前两个参数是 bool 向量，第三个参数是点积。

在 Prolog-land 中，第二个问题假设您可以提出诸如“给定一个向量和一个点积，另一个向量是什么？”之类的问题。您当前的任何一种实现都可以做到这一点吗？你会问这样的问题吗？即使你不认为你会问这样的问题，既然你能做到，你能想出它的用途吗？你明白这是怎么回事吗？

现在，您的代码。它存在问题(例如，请参阅 Isabelle Newbie 刚刚发表的评论)。
这不会给出错误的结果:

:- module(boolean, [add/3, mult/3, dot_product/3]).

add(1,1,1).
add(1,0,1).
add(0,1,1).
add(0,0,0).

mult(1,1,1).
mult(1,0,0).
mult(0,1,0).
mult(0,0,0).

dot_product(V1, V2, P) :-
    same_length(V1, V2),
    maplist(mult, V1, V2, [H|T]),
    foldl(add, T, H, P).

使用它:

?- use_module(boolean).
true.

?- dot_product([1,0,1],[1,1,1],P).
P = 1 ;
false.

?- dot_product([1, 1], [1, 0], Product).
Product = 1 ;
false.

?- dot_product([1, 1], V2, 1).
V2 = [1, 1] ;
V2 = [1, 0] ;
V2 = [0, 1] ;
false.

?- dot_product(V1, V2, 1).
V1 = V2, V2 = [1] ;
V1 = V2, V2 = [1, 1] ;
V1 = [1, 1],
V2 = [1, 0] ;
V1 = [1, 0],
V2 = [1, 1] ;
V1 = V2, V2 = [1, 0] ;
V1 = [1, 1],
V2 = [0, 1] ;
V1 = [0, 1],
V2 = [1, 1] ;
V1 = V2, V2 = [0, 1] ;
V1 = V2, V2 = [1, 1, 1] ;
V1 = [1, 1, 1],
V2 = [1, 1, 0] .

?- dot_product(V1, V2, P).
V1 = V2, V2 = [1],
P = 1 ;
V1 = [1],
V2 = [0],
P = 0 ;
V1 = [0],
V2 = [1],
P = 0 ;
V1 = V2, V2 = [0],
P = 0 ;
V1 = V2, V2 = [1, 1],
P = 1 ;
V1 = [1, 1],
V2 = [1, 0],
P = 1 ;
V1 = [1, 0],
V2 = [1, 1],
P = 1 .

EDIT2:在最后一个正确答案之后还有一个选择点。要摆脱它，您可以使用 tabling (例如，在 SWI-Prolog 中可用)。两者兼得 add/3和 mult/3表，像这样(在定义它们之前):

:- table add/3, mult/3.

没有更多的“假”:

?- dot_product([1,0,1],[1,1,1],P).
P = 1.

?- dot_product(V1, [1, 0], 0).
V1 = [0, 1] ;
V1 = [0, 0].

“相同长度”似乎足够重要；由于没有削减，您可以使用谓词来“生成和测试”。无论如何，点积只为相同长度的向量定义，不是吗？
我没有尝试优化代码。正如您在问题中所观察到的那样，如果论点成立，您可以走捷径。这将是切割(或 if-then-else)的一个很好的用途:如果参数是基础，则在任何向量中查找任何“1”；否则，使用通用算法。
要检查地面列表中的“1”，您可以使用 memberchk(1, List) .