在Prolog中，“semidet”的概念是否已经确定？

Question

作为一个Prolog新手，我发现在2012年底发生了一个非常有趣的讨论。

当时我注意到，在Prolog社区中有两种“semidet”的概念，分别是：

1. 最多只成功一次的计算。
2. 成功后不留下选择点的计算。

显然第二个概念意味着第一个，但反之则不然。

阅读这个帖子，我明白了第一个概念是Neumerkel博士的想法，而第二个概念是Wielemaker、O'Keefe博士等人的想法。

Google搜索时，我看到一些数据库研究者认为“半确定性”（semi-deterministic）是指仅能回答一个等价类的查询，更接近第一个概念。

Neumerkel博士说（指称那里的call_semidet谓词）：

在进行优化和基准测试之前，实现可能会得到改进，但需要先解决实际含义的问题。

那么，这个含义已经解决了吗？

“det”的情况如何？

根据SWI-Prolog的定义（见下面），习惯上将谓词分类为它们的解的数量。'det'可以进行完全非确定性（比如并行）计算，只要它承诺现在一定存在一个解决方案即可。类比一下，我猜想可能有两种'det'的概念：

1. 仅成功一次的计算。
2. 成功一次且在成功之后不留下选择点的计算。

第一个更加逻辑但通常是不可判定的，直到计算结束。第二个一旦找到解决方案就很容易判断，但是程序化的，其含义取决于Prolog所使用的特定搜索策略，即深度优先搜索。

我想知道社区是否已经达成共识？为什么不把这两个不同的概念命名为不同的名称呢？

以下是SWI-Prolog页面中的摘录：

det [determinism]

缩写：确定性的。

deterministic

如果一个谓词成功一次并且没有留下选择点，则它是确定性的。

semidet

半确定性的缩写。

semi deterministic

半确定性的谓词无论是失败还是恰好成功一次，都不会有选择点。另见确定性。

- mnish

---

“...实际含义需要确定。”这句话实际上是指用户的编程过程中，我们希望确定谓词的含义。它并不是指需要确定已经确定的call_semidet/1的含义。 - false

Answer 1

这是一个非常好的问题！

从水星决定论类别中，也有权威地解释了这一点：

6.1 确定性分类

对于谓词或函数的每个模式，我们根据其能够成功的次数以及在生成第一个解之前是否可能失败来对其进行分类。

如果对于谓词或函数的特定模式的所有可能调用都返回给调用者（终止调用，不抛出异常并且不会导致运行时错误）：

• 恰好有一个解，则该模式是确定性的（det）；
• 没有解或只有一个解，则该模式是半确定性的（semidet）；
• 至少有一个解，但可能有多个解，则该模式是多解的（multi）；
• 有零个或多个解，则该模式是非确定性的（nondet）；
• 恰好没有解，即在不生成解的情况下失败，则该模式具有失败的确定性（failure）。

(强调为我所加)

请注意，这个定义中甚至没有提到是否留下选择点，整个部分也没有。Mercury不同于Prolog，但关键是这个定义原则上也完全适用于Prolog。显然，它对应于您的变体(1)。

在我看来，这样做是正确的：是否留下“选择点”并不重要，这取决于例如您的系统的参数索引功能有多强大和灵活。良好的索引方案可以防止其他系统引入的选择点的创建。这是一个依赖于特定Prolog系统的特殊习惯性的概念，并且可能会因为引入更好的参数索引等而从一个版本到另一个版本中断。这不是非常健壮的，也没有太大的价值。

确实，我们经常说“谓词是确定性的”时，实际上是指：“谓词是确定性的且没有剩余选择点”，但即使如此，主要观点几乎总是这样的：该谓词仅成功一次。请注意，“确定性”是一个具有其他含义的相当重载的形容词。在SWI文档中，这种歧义也延续到了半确定性。然而，即使SWI从其他地方的这个实现导向的定义中稍微后退了一步：

2.2.2 测试半确定性谓词

半确定性谓词是指要么失败要么成功一次，并且对于良好行为的谓词，不会留下选择点。

因此，一个不良行为的半确定性谓词也可能留下选择点......

在讨论中，特别注意以下内容：Ulrich在这里使用更弱且更健壮的概念来获得适用于两个定义的谓词。

因此，无论您选择哪个变体，call_semidet/1都是有用的！从这里，引语的含义变得更加清晰。当乌尔里希（Ulrich）说：

（实现可能会得到改进，但在优化和基准测试之前，必须解决实际含义的问题。）

显然并不是指"semidet"的含义必须在两个变体之间解决，而是应该首先明确call_semidet/1实际上保证了什么：它比人们认为的乌尔里希发布的要有用得多。例如，Jan给出的定义：

call_semidet(Goal) :- 
        call_cleanup(Goal, Det=true), 
        (   Det == true 
        ->  true 
        ;   throw(error(mode_error(semidet,Goal),_)) 
        ). 

只适用于你的第二个"semidet"定义。

- mat

---

请注意，在 Mercury 中，“答案”和“解决方案”几乎可以互换使用，因为 Mercury 的答案只是基础答案。 - false

感谢您详细的回答！优化问题正是我所考虑的，但我的意图是“两个定义都是明确定义且有用的，值得拥有自己的术语吗？”也许我明天会重写我的问题，以澄清我所说的“明确定义”的含义。 - mnish

也许最好写一篇新的问题。 - false

我同意这个错误：最好提出一个新问题，因为更改问题还需要更改现有答案。 - mat

Answer 2

目前在SWI-Prolog中使用的分类（例如@mat所提到的）是从Mercury中采用的。所使用的模式名称（det、semidet、multi和nondet）选择非常糟糕（也不足够）。它们不仅是缩写，而且需要新用户查阅文档才能理解它们的含义！具有讽刺意味的是，每个这些模式的含义描述已经建议了最好的非缩写和清晰的名称。请记住我们正在谈论的是解决方案数量：zero、one、zero_or_one、zero_or_more、one_or_more（可能还有一个很有用的error，可以用来指示给定调用模式导致错误）。顺便说一句，这些是Logtalk中使用的模式名称。

将谓词的解决方案数量（在给定模式下）的规范与剩余选择点的问题混合在一起也是一个糟糕的选择，充满了歧义，正如@mat所描述的那样。代码优化问题与解决方案数量的规范无关。此外，任何除zero之外的模式在解决方案用尽时都可能留下多余的选择点。因此，这比仅区分名为det和semidet的模式更通用。

- Paulo Moura

---

call_semidet/1 关注的是答案，而不是解决方案。 - false

@false 问题和我的回答都不涉及call_semidet/1谓词。此外，尽管问题和迄今为止的答案都谈到了解决方案，但可以区分解决方案、答案和证明。但这需要对这些术语进行精确定义，并在公众中达成共识。目前，这些术语经常以自由的方式使用。在这方面，Logtalk实际上将谓词mode/2指令中的第二个参数描述为证明数，这符合推理引擎的工作方式。 - Paulo Moura

非常感谢，我收到您的意见，但是我对“选择点”的“歧义性”有另一个看法。在我看来，选择点是一个独立于特定实现的明确定义的ISO概念。但也许我需要准确理解call_cleanup/2的作用。 - mnish

@mnish：请查看此定义，这是目前为止最好的。如有任何问题，请使用新的SO问题。 - false

@false：哦，所以实现可以在实现相关的时刻调用清理操作。那么我对SWI的定义的看法似乎并不是很相关。嗯，我有点困惑了。 - mnish

@mnish：再次提醒：如有任何问题，请使用新的SO问题。 - false