问题标签 [logical-purity]

关于这个主题的维基百科部分是一团糟。它指出：

Pure Prolog基于一阶谓词逻辑的子集 Horn 子句，它是图灵完备的。Prolog的图灵完备性可以通过使用它来模拟图灵机来展示：

（重点补充）

然后它继续显示使用非 Horn 子句（!和once）的代码：

好的，所以 Prolog 是图灵完备的。没有人怀疑这一点。纯Prolog 呢？

如果纯 Prolog 实际上是图灵完备的，为什么我们似乎无法在其中实现列表交集（第一个列表按第二个列表中的成员资格过滤）？所有实现都至少使用以下之一：!, \+, findall,call直接或间接。

一篇关于汞的论文说：

Prolog 的大多数变体中的 if-then-else 和 negation 结构是不合逻辑且不合理的：它们会导致系统计算出与被视为逻辑理论的程序不一致的答案。一些现有的逻辑编程系统，例如NU-Prolog 和 Gödel 为这些 Prolog 结构提供了逻辑和合理的替代。不幸的是，这些系统通过运行时接地检查来强制执行安全性。这种效果可以将程序的运行时间增加任意大的倍数；如果检查基础的目标包括大项，则检查可能会非常昂贵。

NU-Prolog 和 Gödel 看起来相当死气沉沉且不自由，但我仍然想知道：

• 这些合乎逻辑且合理的if-then-else替代品是什么？
• 他们在 SWI 或 GNU Prologs 中有类似物吗？
• 它们是如何工作的？他们怎么能工作？在 Prolog 中添加逻辑否定会将其变成一般的 FOL，对吗？您基本上需要一个通用的 FOL 定理证明器来使用它？
• 它们与 不同if_/3吗？if_/3必须扩展以在新条件下使用。在 NU-Prolog 和 Gödel 中也必须这样做吗？

标签逻辑纯度提到 (=)/2 是纯的。它是“内在”纯粹还是“操作”纯粹？据我所知，它可以由这个 Horn 子句定义：

如果还不是内置的，这是 Prolog 的事实：

这意味着 (=)/2 将是“本质上”纯粹的，正如 SWI-Prolog 已经指出的那样。那么，如果有任何差异，那么与一阶相等（FOL=）有什么区别？

@false之前评论过：

是的，您可以在没有dif/2. 但是你甚至不能实现交集或类似的谓词。

假设我们用 , , 和 扩展纯 Prolog ( Horn FOL + CWA + UNA ) ,用于, 它的表达能力是否仍然存在差距,即在Scheme中定义微不足道的东西, 但要困难得多在这样扩展的（几乎是纯粹的）Prolog 中陈述？call/Ndif/2(=)/3if_/3

特别是，这样的 Prolog 是否允许像 Scheme 允许操作 Scheme 列表一样方便地操作 Prolog 列表？

编辑： 假设方案没有突变、宏、延续、惰性、流、数字、字符串、向量或字符。只是符号、布尔值和列表（树）。

我想知道是否有一个只有一条规则的纯 Prolog 元解释器。通常的 Prolog vanilla 元解释器有两个规则。内容如下：

这个 Prolog vanilla 元解释器使用两个规则/* rule 1 */ 和/* rule 2 */. 剩下的就是事实。执行的程序由程序事实表示。这是一个示例程序：

还有一个示例查询：

有没有办法将程序以不同的方式表示为事实，然后编写一个不同的元解释器，它只使用事实，除了一个规则而不是两个规则？适用于所有纯 Prolog 程序的东西，而不仅仅是 nrev 示例？

让我们假设有带有 dif/2 的 pure_2 Prolog 和没有 dif/2 的 pure_1 Prolog。我们能否在不使用 dif/2 的情况下实现 Peano 值的独立性，即 Peano 数？因此，让我们假设我们在 pure_2 Prolog 中有这样的 Peano 独立性：

我们可以用更纯粹的定义替换 neq(X,Y)，即来自不使用 dif/2 的 pure_1 Prolog 吗？所以我们有一个终止的 neq/2 谓词可以决定 Peano 数的不等式？那么它的定义是什么？

假设我们只查看 Peano 数字列表。让我们假设 pure_2 Prolog 不是带有 dif/2 的 pure_1 Prolog，而是带有带有 when/2 的 pure_1 Prolog。我们可以实现列表交集吗？

我们会退后一步，从编程语言 Gödel 和 Nu-Prolog 中汲取灵感。因此，对于任何需要的 if-then-else，我们将在此处使用此答案。会是什么：

请注意，尽管如此，与 Gödel 和 Nu-Prolog 相反，为了在此问题中坚持 pure_2 Prolog，我们将不允许使用 ISO Prolog if-then-else ( -> ;_)。但是我们可以按照这里的要求使用分离关系。

一个测试用例将是坚定不移：

设想皮亚诺数的关联关系并不难。甚至可以像这里一样制作一个具体的 eq/3 谓词。

现在的问题是，我们是否可以突破边界并equal?以纯粹和具体化的方式实现 Scheme 谓词？问题将是例如实现这种减少，也称为 δ 规则（请参阅此处的第 6 章扩展）：

如果术语用 deBruijn 索引表示。equal?除了处理列表（树）之外，这会将 alpha 转换合并到谓词中。纯可以表示本质上纯或操作纯，如逻辑纯度标签中所定义。

测试用例是与列表（树）的纯交集，而只是 Peano 数字。

Peano算术中的这个小于谓词

循环时

有没有更好的写作方式less/2（仅使用 Horn 子句）？

有这篇论文：

William E. Byrd、Eric Holk、Daniel P. Friedman，2012
miniKanren，
通过关系解释器实时和未标记的 Quines 生成
http://webyrd.net/quines/quines.pdf

它使用逻辑编程来查找 Scheme Quine。这里考虑的 Scheme 子集不仅包含 lambda 抽象和应用程序，还包含通过以下归约处理的小列表处理，已翻译为 Prolog：

因此，除了用于 lambda 抽象和绑定变量的 lembda 之外，唯一的符号是引号、[] 和 cons。我们将使用 Prolog 列表作为 Scheme 列表。目标是通过 Prolog 找到一个 Scheme 程序 Q，这样我们得到 Q ~~> Q，即对自身求值。

有一个复杂性，这使得努力变得不平凡，[lembda,X,Y] 不会在语法上对其自身进行评估，而是应该返回一个环境闭包。因此，评估器与此处的 Plotkin 评估器不同。

周围有任何 Prolog 解决方案吗？圣诞快乐