如果直接插入，为什么 Prolog 会将变量与失败的结果匹配? [英] Why would Prolog match a variable to a result that fails if plugged in directly?

问题描述

我正在制作一个 Prolog 程序来查找一组列表的子集.这个子集必须匹配一些特定的条件，其中一个方面是子集的列表不能相同.令我困惑的是，当我尝试为变量 X 找到匹配项时，如果我将它们插入查询中而不是 X，它会生成返回 false 的结果.例如:

?- containsSet(2, [[3],[7],[7]], X).X = [[3], [7]] ;X = [[3], [7]] ;X = [[7], [7]] ;错误的.?- containsSet(2, [[3],[7],[7]], [[7],[7]]).错误的.

如果直接插入返回false，X怎么可能匹配到[[7], [7]]?

containsSet 的想法是找到一个长度为 N(在本例中为 2)的列表子集，该子集在匹配位置没有匹配元素(即子集中没有两个列表具有相同的第一个元素或相同的第二个元素， 等等).在上面的示例中，[7] 和 [7] 的第一个(也是唯一一个)元素匹配，因此它返回 false.

解决方案

首先，祝贺我在初学者的问题中看到的最具陈述性和合理性的观察之一！

一方面，合取在逻辑上是可交换的，这是最基本和众所周知的性质之一.另一方面，许多 Prolog 初学者没有意识到使用像 (+)/1 这样的非单调谓词几乎总是破坏这样的基本不变量.您注意到这里发生了一些非常出乎意料的事情，并且您期望 Prolog 提供更正确的行为是正确的.幸运的是，针对此类问题的声明式解决方案现在在 Prolog 系统中比以往任何时候都更广泛地传播.

首先，考虑一下如果您在程序中使用 (+)/1 很快就会出现的一些问题:

<上一页>?- X = d, + 成员(X, [a,b,c]).X = d.

然而，如果我们简单地通过合取交换性来交换目标，我们会得到不同的答案:

<上一页>?- + 成员(X, [a,b,c]), X = d.错误.

这表明 (+)/1 不是单调的:它可能导致 更一般的查询失败，尽管 更具体的查询产生解决方案:

<上一页>?- + 成员(X，[a，b，c]).错误.?- + 成员(d，[a，b，c]).是的.

因此，非单调谓词会导致各种杂质并违反声明性语义.以声明的方式，知道有解决方案，我们当然希望更一般的查询成功，但它失败.

具体来说，要指定一个术语与列表中的所有其他术语不同，请使用约束 dif/2.dif/2 适用于所有方向，如果它的参数是变量，也会产生正确的答案.例如:

not_member(X, Ls) :- maplist(dif(X), Ls).

这个定义保留了合取的交换性，正如我们对纯逻辑关系的深切渴望和事实上所期望的那样:

<上一页>?- not_member(X, [a,b,c]), X = d.X = d.?- X = d, not_member(X, [a,b,c]).X = d.

由于 not_member/2 仅使用纯谓词，因此您已确保 —已经在建设中了——它只给出声明性正确的答案.

为了对您的代码进行声明式推理(我对您的方法表示赞赏)，我建议您留在 Prolog 的纯单调子集中.请参阅 logical-purity 和 prolog-dif 了解更多信息.p>

I'm making a Prolog program that finds a subset of a set of lists. This subset must match some specific conditions, an aspect of which is that the subset's lists cannot be identical. What's confusing me is that when I try to find a match for a variable, X, it generates results that return false if I plug them into the query in place of X. For example:

?- containsSet(2, [[3],[7],[7]], X).
X = [[3], [7]] ;
X = [[3], [7]] ;
X = [[7], [7]] ;
false.

?- containsSet(2, [[3],[7],[7]], [[7],[7]]).
false.

How could it possibly match X to [[7], [7]] if, when plugged in directly, it returns false?

The idea of containsSet is to find a length-N (in this case 2) subset of lists that has no matching elements in matching positions (i.e. no two lists in the subset have the same first element, or the same second element, etc). In the example above, the first (and only) elements of [7] and [7] match, so it returns false.

解决方案

First, congratulations for one of the most declarative and justified observations I have seen in questions by beginners!

On the one hand, it is one of the most basic and well-known properties that conjunction is commutative in logic. On the other hand, many Prolog beginners fail to realize that using one of the non-monotonic predicates like (+)/1 almost invariably destroys such basic invariants. You noticed that something very unexpected is going on here, and you are right to expect more correct behaviour from Prolog. Luckily, declarative solutions for such problems are now more widely spread than ever before among Prolog systems.

First, consider some problems that soon arise if you use (+)/1 in your programs:

?- X = d, + member(X, [a,b,c]).
X = d.

yet, if we simply exchange the goals by commutativity of conjunction, we get the different answer:

?-  + member(X, [a,b,c]), X = d.
false.

This shows that (+)/1 is not monotonic: It can cause a more general query to fail although a more specific query yields solutions:

?-  + member(X, [a,b,c]).
false.

?- + member(d, [a,b,c]).
true.

Thus, non-monotonic predicates cause all kinds of impurities and violate declarative semantics. Declaratively, knowing that there are solutions, we certainly expect the more general query to succeed, but it fails.

In this concrete, to specify that a term is different from all other terms in a list, use the constraint dif/2. dif/2 works in all directions, and yields correct answers also if its arguments are variables. For example:

not_member(X, Ls) :- maplist(dif(X), Ls).

This definition preserves commutativity of conjunction, as we deeply desire and in fact expect from pure logical relations:

?- not_member(X, [a,b,c]), X = d.
X = d.

?- X = d, not_member(X, [a,b,c]).
X = d.

Since not_member/2 uses only pure predicates, you have ensured — already by construction — that it gives only declaratively correct answers.

For reasoning declaratively about your code, which I applaud in your approach, I recommend you stay in the pure monotonic subset of Prolog. See logical-purity and prolog-dif for more information.

这篇关于如果直接插入，为什么 Prolog 会将变量与失败的结果匹配?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！