3

我有两个表达式来使用 Prolog 列出所有位列表：

bit(0).
bit(1).

bitlist1([]).
bitlist1([B|Bs]) :-
    bit(B),
    bitlist1(Bs).

bitlist2([]).
bitlist2([B|Bs]) :-
    bitlist2(Bs),
    bit(B).

我不太清楚它们在逻辑上是否等效，即使它们都确实列出了所有位列表。

当我使用 SWI-Prolog 时，我得到了以下输出：

?- bitlist1(Bs).
Bs = [] ;
Bs = [0] ;
Bs = [0, 0] ;
Bs = [0, 0, 0] ;
Bs = [0, 0, 0, 0] ;
Bs = [0, 0, 0, 0, 0] ;
Bs = [0, 0, 0, 0, 0, 0] ;
Bs = [0, 0, 0, 0, 0, 0, 0] ;
Bs = [0, 0, 0, 0, 0, 0, 0, 0] ;
Bs = [0, 0, 0, 0, 0, 0, 0, 0, 0] ;
Bs = [0, 0, 0, 0, 0, 0, 0, 0, 0|...] ;
...

?- bitlist2(Bs).
Bs = [] ;
Bs = [0] ;
Bs = [1] ;
Bs = [0, 0] ;
Bs = [1, 0] ;
Bs = [0, 1] ;
Bs = [1, 1] ;
Bs = [0, 0, 0] ;
Bs = [1, 0, 0] ;
Bs = [0, 1, 0] ;
Bs = [1, 1, 0] ;
Bs = [0, 0, 1] ;
Bs = [1, 0, 1] ;
Bs = [0, 1, 1] ;
Bs = [1, 1, 1] ;
Bs = [0, 0, 0, 0] ;
...

bitlist1开始列出仅包含零的所有位列表，然后开始列出所有其他位列表，但这实际上不能被视为 Prolog 列出了仅包含零的位列表的无尽流。

bitlist20列出每个长度的和的所有组合，1然后继续使用长度更高的位列表。

因此它们在 imo 逻辑上是等效的，只是位列表的输出顺序不同。

也许任何人都可以证实我的猜测或解释为什么这两个表达式在逻辑上不等价？会很好。

4

4 回答 4

1

引用范诺德

两个表达式在逻辑上是否等价的问题对于任何“有趣的”逻辑都是不可判定的。

然后，由于 Prolog 搜索的不完整，您应该在一定程度上限制您的证明标准。我会说等价源于这样一个事实：

对于任何给定的 N，不可能找到失败的长度（L，N）、bitlist1（L）、bitlist2（L）。的确

2 ?- length(L,N), bitlist1(L), bitlist2(L).
L = [],
N = 0 ;
L = [0],
N = 1 ;
L = [1],
N = 1 ;
L = [0, 0],
N = 2 ;
L = [0, 1],
N = 2 ;
L = [1, 0],
N = 2 ;
L = [1, 1],
...
于 2013-05-23T07:00:26.607 回答
1

在逻辑层面上，两个谓词是等价的，因为规则中的“，”被解释为可交换的逻辑合取（检查这一点的最简单方法是查看 A & B -> C 和 B & A 的真值表-> C，但也可以使用后续微积分或其他一些证明微积分来完成这项工作）。

对于纯 prolog 程序，逻辑等价谓词的答案集是相同的。由于 prolog 使用深度优先搜索作为搜索策略，因此一个预测可能不会终止，以防其他预测终止：

?- bitlist1([a|Xs]).
false.

?- bitlist2([a|Xs]).
^CAction (h for help) ? abort
% Execution Aborted

原因是prolog试图一个接一个地证明目标。在 bitlist1 的情况下，第一个目标是 bit(B)，prolog 可以立即决定 bit(a) 不成立。在 bitlist2 的情况下，prolog 首先尝试证明 bitlist2(Bs) 并递归地对 Bs 列表的尾部执行此操作，从而导致无限递归。因此，即使两个谓词在逻辑上是等价的，它们的行为也会不同。

对于查看解决方案的问题，您可以尝试以增加长度的方式枚举列表：

?- length(X,_), bitlist1(X).
X = [] ;
X = [0] ;
X = [1] ;
X = [0, 0] ;
X = [0, 1] ;
X = [1, 0] ;
X = [1, 1] ;
X = [0, 0, 0] ;
X = [0, 0, 1] ;
X = [0, 1, 0] .

?- length(X,_), bitlist2(X).
X = [] ;
X = [0] ;
X = [1] ;
X = [0, 0] ;
X = [1, 0] ;
X = [0, 1] ;
X = [1, 1] ;
X = [0, 0, 0] ;
X = [1, 0, 0] ;
X = [0, 1, 0] .

长度谓词给出列表与其长度之间的关系。我们现在依靠 length(X,_) 生成长度增加的自由变量列表这一事实。然后目标 bitlist(1/2) 将在一个固定大小的列表上调用，prolog 将在回溯并尝试下一个更大的列表之前找到该大小的所有解决方案。

请注意，此技巧仅重新排序解决方案，但通常不会更改终止：

?- X=[a|Xs], length(X,_), bitlist2(X).
^CAction (h for help) ? abort
% Execution Aborted

这仍然失败，因为 prolog 需要检查所有列表 X 不以 a 开头，但检查仅在递归目标之后完成。

于 2013-05-24T10:10:52.247 回答
0

在纯逻辑中，操作顺序无关紧要，因为一切都是幂等函数。因此，只要您没有削减或副作用，A, B并且B, A是等效的。

于 2013-05-23T00:39:52.450 回答
0

我不确定您是否应该讨论谓词的纯逻辑含义，然后用实际的 Prolog 程序演示它。

例如，您的第一个谓词实际上永远不会用完 0。没有“后记”，或者搜索树中的“后记”肯定永远不会被访问。当然，如果您使用它来生成答案；使用它进行验证不会表现出这种行为。

于 2013-05-23T05:14:08.990 回答