Prolog 中如何解释匿名变量？

Question

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

现在，当匿名变量 (_) 发挥作用时，我怀疑正确有效地做到这一点的诀窍在于改变确定两个项之间最左边差异的方式，以便在其中一个项时忽略一对项是匿名变量。显然正确的方法是重命名目标中 _ 的每个实例，并将程序设置为新的变量名称并使用这些名称求解。

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

Answer 1

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

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

yes

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

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

X = 1
yes

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

匿名变量还简化了谓词定义的编写，它们与 "don't care" 变量类似。以 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

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

Answer 2

这是一个答案中的评论，因为评论无法根据需要格式化它。

使用 SWI-Prolog

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

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

Prolog 中如何解释匿名变量？

How are anonymous variables interpreted in Prolog?

evaluation

prolog

sld-resolution

prolog-anonymous-variable