问题标签 [logical-purity]

有没有办法在 prolog 中执行 if，例如，如果变量为 0，则执行一些操作（将文本写入终端）。甚至不需要 else，但我找不到任何有关 if 的文档。

如果我想确保两个变量不会实例化为同一个术语，那么首选的方法是什么？

假设我需要在图中找到有向边，并且节点不能对自身有边：

（这里的边是 a -> c，b -> a，但不是c -> c）

以下作品：

这也有效[swi-prolog]：

这显然不起作用（因为 A 和 B 都没有被实例化？）：

我想我对第一个解决方案的问题是，对于更复杂的谓词，在失败node之前可能会发生许多不必要的统一。另一方面，在一个库中，这表明它不适合在如此简单的情况下使用（尽管它具有我似乎正在寻找的确切功能）edge。dif

编写好的 Prolog 必须掌握哪些设计启发式方法？我听说一个有经验的程序员需要大约两年的时间才能精通 Prolog。有效地使用递归是其中的一部分，但这似乎是一个相对较小的障碍。到底是什么给程序员带来了这么多麻烦？我应该在示例代码中寻找什么来判断它的质量？

老实说，我是 Prolog 新手，所以请原谅我的无知。

我有一个简单的谓词来计算列表中原子的出现次数，如下所示：

以下查询返回正确的结果：

但是，如果我试图找到所有可能的解决方案，它只会给出一个。

我如何得到它来提供所有的解决方案？我虽然它可能与 cut 运算符有关，但删除它似乎也不起作用。

我知道var/1，nonvar/1并且!/0是不纯的原语，但是它们的使用是否会使每个使用它们的程序不纯？

我写了下面的谓词plus/3，它的行为就好像它是纯的，或者至少是我所声称的。谓词是说明性的，并非旨在高效。

我有两个问题：

1. 上面的谓词plus/3真的是纯的吗？
2. 一般来说，你如何证明一个特定的关系具有逻辑纯度？

这个问题在关于这个答案的讨论之后。

问题

我有一个与逻辑纯度有关的问题。

这个程序是纯的吗？

关于上下文的一些[ir]相关细节

我正在尝试编写具有良好终止属性的纯谓词。例如，我想编写一个谓词list_length/2来描述列表与其长度之间的关系。我想实现与内置谓词相同的终止行为length/2。

我的问题旨在确定以下谓词是否是纯的：

我可以用clpfd实现我的目标......

...或者我可以使用var/1, nonvar/1and !/0, 但是很难证明谓词是纯的。

问题

一旦列表的长度已知/固定，是否可以安排目标执行，或者正如@false 在评论中指出的那样，给定的参数变成 [proper] 列表？沿着这条线的东西：

何时条件可以使用?=/2, nonvar/1, ground/1, ,/2, and ;/2only 来构造，并且在查看整个列表时它们似乎不是很有用。

作为进一步的细节，如果可能的话，我正在寻找一种呈现逻辑纯度的解决方案。

动机

我认为当人们想要使用谓词p(L)来检查 list 的属性L但不以生成方式使用它时，此条件可能很有用。

例如，[出于效率或终止原因]如果具有固定长度（即是一个列表），则可能会更喜欢p1(L), p2(L)按此顺序执行以下连词，否则以相反的顺序执行（如果是部分列表）。LLp2(L), p1(L)L

这可能是这样实现的：

更新

我确实实施了一个解决方案，但它缺乏纯度。

我想为 这个论坛中的其他一些最近的问题提供一个逻辑上纯粹的解决方案。

首先，我实现了一个具体化的变体append/3并将其命名为appendR/4. 它基于谓词if_/3并由(=)/3AUBUC 的Prolog union 中的 @false 实现：

该实现基本上可以工作，如以下查询所示：

到目前为止，一切都很好......这是棘手的部分：

我想得到前两个答案，但不是最后两个。请帮忙！

虽然从声明的角度来看，这个定义使用member/2andnon_member/2几乎是¹完美的，但它为某些查询产生了冗余的解决方案，并在周围留下了选择点。

什么是在此基础上改进的定义（以纯粹的方式可能使用if_/3and (=)/3）使得完全相同的一组解决方案被描述different/2但至少对于地面查询是确定的（因此不会留下任何无用的选择点）并省略（如果可能）任何多余的答案？

¹ _{其实，different([a|nonlist],[]), different([],[b|nonlist])成功了。它同样可能失败。因此，两者都失败的解决方案很好（甚至更好）。}

“逻辑纯度”是什么意思（在 Prolog 编程的上下文中）？逻辑纯度标签信息说“仅使用 Horn 子句的程序”，但是，如何if_/3使用限定的谓词，尽可能多地使用它，以及各种元逻辑（什么是正确的术语？var/1等等）谓词，即低级的东西。

我知道它达到了一些“纯粹”的效果，但这究竟意味着什么？

有关更具体的说明，请解释在使用中例如在此答案中if_/3看到的逻辑纯的资格？