Prolog 中如何解释匿名变量？答案

【问题标题】：How are anonymous variables interpreted in Prolog?Prolog 中如何解释匿名变量？
【发布时间】：2020-03-06 18:15:37
【问题描述】：

一个关于匿名变量在给定一组程序规则的 Prolog 查询解析中扮演什么角色的快速而简单的问题。因此，按照我理解 SLD 解析的最简单形式如何工作的方式，SLD 树是通过从一组目标术语中获取一些术语（基于选择规则，例如 FIRST）并遍历所有程序规则来查看哪个规则的左手边（可以这么说的结果）可以与手头的术语统一。统一两个给定项的方法是取两个项的差异集，看看是否可以用变量替换项，使差异消失，你可以通过连续取最左边的单个差异并检查是否，在两个集合中构成差异，一个是没有出现在另一个中的变量，并与一个将变量映射到术语（从空或身份替换开始）组成您当前的替换。

现在，当匿名变量 (_) 发挥作用时，我怀疑正确有效地执行此操作的诀窍在于改变确定两个术语之间最左边差异的方式，以便在其中一个术语是匿名变量。显然正确的方法是重命名目标中 _ 的每个实例，并将程序设置为一个新的变量名并使用它们来解决。

它实际上是如何完成的？我的想法是否足够，或者还有更多？（此外，如果我理解 SLD 解析工作的方式中缺少某些东西，我将不胜感激，除非否定、调用、封装、算术谓词和更复杂的东西。）

【问题讨论】：

在阅读中你让我想到的问题。我不相信 SLD 解析有匿名变量的概念。如果是这样，那么任务就落到了 Prolog 之类的实现上，并且在那里选择绑定到匿名变量的内容是基于术语中的位置。任何东西都可以与匿名变量统一，但是当它们中的两个统一时，IIRC 有一些值得注意的地方。对此持保留态度，我没有检查所有这些，但这是我脑海中浮现的内容，因此是评论的原因。
您可以考虑更改标题。它说Prolog，但问题更多的是关于SLD resolution。
如果术语绑定到匿名变量，那么它们需要重命名，以防止在一个术语中使用多个术语时发生冲突等。但是统一替换是否只是让它们成为唯一的两个术语之间的区别是一个在某个位置有 _ 而另一个是整个术语？但如果 SLD 解析没有任何匿名变量的概念，那么明智的做法是重命名所有匿名变量。变量以消除它们来 SLD 分辨率，对吗？
不过，我的问题与 Prolog 内部如何解释 _ 相关。也许我不应该强调 SLD 分辨率...
如果您需要更技术性的解释，那么您可以查看 WAM 的说明。请参阅：Warren’s Abstract Machine - A Tutorial Reconstruction 搜索 anonymous variable。

标签： prolog evaluation prolog-anonymous-variable sld-resolution

【解决方案1】：

Prolog 匿名变量在 SLD 解析或术语统一中不发挥作用，但在 Prolog 代码和 Prolog 查询中发挥实际作用。匿名变量的一个基本方面是每次出现的匿名变量都是不同的变量。考虑以下查询：

| ?- a(_, _) = a(1, 2).

yes

如果两个匿名变量是同一个变量，则统一将失败。现在考虑查询：

| ?- a(X, _) = a(1, 2).

X = 1
yes

仅针对非匿名变量的变量报告变量绑定。这允许每次我们对变量的任何绑定都不感兴趣时使用匿名变量。

匿名变量还简化了谓词定义的编写，它们类似地充当“无关”变量。以member/2 谓词的通常定义为例：

member(Element, [Element| _]).
member(Element, [_| List]) :-
    member(Element, List).

在第一个子句中，我们不关心列表尾。在第二个子句中，我们不关心列表头。通过使用匿名变量，我们可以忽略这些子项，并避免编译器抱怨将在子句中使用一次的变量。

更新

请注意，查询中的所有不同变量都会获得唯一的内部变量引用，不要与用户键入的变量名称混淆。变量名称仅由顶级解释器用于报告成功查询的绑定。用于证明查询的推理机制使用变量（内部）引用。以下查询，使用带有标准选项的 ISO Prolog 标准 read_term/2 谓词可能会有所帮助：

| ?- read_term(Term, [variable_names(Names), variables(Variables)]).
a(X, _, Y, _).

Names = ['X'=A,'Y'=B]
Term = a(A,C,B,D)
Variables = [A,C,B,D]

yes

在术语读取中，有四个不同的变量，但其中只有两个具有（用户提供的）名称。

【讨论】：

【解决方案2】：

这是答案中的评论，因为评论无法根据需要对其进行格式化。

使用 SWI-Prolog

?- trace,(_=_).
   Call: (11) _1834=_1836 ? creep
   Exit: (11) _1834=_1834 ? creep
true.

每个匿名变量都被创建为一个单独的变量。当统一发生时，一个变量与另一个变量统一。

【讨论】：