了解 Prolog 列表

我试图理解 Prolog 列表，以及如何在递归函数末尾“返回”/实例化值。

我正在看这个简单的例子：

val_and_remainder(X,[X|Xs],Xs).
val_and_remainder(X,[Y|Ys],[Y|R]) :-
   val_and_remainder(X,Ys,R).

如果我打电话val_and_remainder(X, [1,2,3], R).然后我会得到以下输出：

X = 1, R = [2,3]; 
X = 2, R = [1,3];
X = 3, R = [1,2];
false.

但我很困惑为什么在基本情况下（val_and_remainder(X,[X|Xs],Xs).) Xs必须按其实际情况出现。

如果我打电话val_and_remainder(2, [1,2,3], R).那么在我看来，它会像这样运行该程序：

% Initial call
val_and_remainder(2, [1,2,3], R).

val_and_remainder(2, [1|[2,3]], [1|R]) :- val_and_remainder(2, [2,3], R).

% Hits base case
val_and_remainder(2, [2|[3]], [3]).

如果上面的运行是正确的，那么它如何获得正确的值R？如上例所示，R 的值应为R = [1,3].

在Prolog中，你需要考虑谓词 not as 功能就像您通常在其他语言中所做的那样。谓词描述关系，其中可能包括有助于定义该关系的参数。

例如，让我们看这个简单的例子：

same_term(X, X).

这是一个谓词定义两个参数之间的关系。通过统一也就是说，如果第一个和第二个参数是统一的，那么它们是相同的（这个定义取决于我们，谓词的作者）。因此，same_term(a, a)将会成功，same_term(a, b)将会失败，并且same_term(a, X)将会成功X = a.

您还可以以更明确的形式编写：

same_term(X, Y) :-
    X = Y.  % X and Y are the same if they are unified

现在让我们看看你的例子，val_and_remainder/3。首先，它是什么意思？

val_and_remainder(X, List, Rest)

这意味着X是一个元素List and Rest是一个由所有其余元素组成的列表（没有X）。 （注意：您没有立即解释这个含义，但我从您的示例的实现中确定了这个含义。）

现在我们可以写出描述规则了。首先，一个简单的基本情况：

val_and_remainder(X,[X|Xs],Xs).

这说的是：

Xs是列表的剩余部分[X|Xs]没有X.

根据 的定义，这个陈述应该是非常明显的[X|Xs]Prolog 中列表的语法。您需要所有这些参数，因为第三个参数Xs必须与列表的尾部（其余部分）统一[X|Xs]，那么这也是Xs（根据定义，同名的变量是统一的）。和以前一样，您可以更详细地写出：

val_and_remainder(X, [H|T], R) :-
    X = H,
    R = T.

但其实简写形式更清晰。

现在递归子句说：

val_and_remainder(X, [Y|Ys], [Y|R]) :- 
    val_and_remainder(X, Ys, R).

所以这意味着：

[Y|R]是列表的剩余部分[Y|Ys]没有X if R是列表的剩余部分Ys没有元素X.

您需要考虑该规则以说服自己它在逻辑上是正确的。这Y第二个和第三个参数是相同的，因为它们引用相同的元素，所以它们必须统一。

因此，这两个谓词子句形成了涵盖这两种情况的两条规则。第一种情况是简单的情况，其中X是列表的第一个元素。第二种情况是递归定义whenX不是第一个元素。

当您进行查询时，例如val_and_remainder(2, [1,2,3], R).Prolog看看是否可以unify期限val_and_remainder(2, [1,2,3], R)与一个事实或一个谓词子句的头部。它试图与val_and_remainder(X,[X|Xs],Xs)因为它需要统一X with 2，这意味着需要统一[1,2,3] with [2|Xs]从第一个元素开始就失败了[1,2,3]是 1，但是第一个元素[2|Xs] is 2.

所以 Prolog 继续前进并成功统一val_and_remainder(2, [1,2,3], R) with val_and_remainder(X,[Y|Ys],[Y|R])通过统一X与 2,Y与 1,Ys with [2,3], and R with [Y|R]（注意，这很重要，R您的调用中的变量与R谓词定义中的变量，所以我们应该命名它R1以避免这种混乱）。我们将为您命名R as R1并说R1统一于[Y|R].

当执行第二个子句的主体时，它调用val_and_remainder(X,Ys,R).或者，换句话说，val_and_remainder(2, [2,3], R)。现在这将与第一个子句统一并为您提供R = [3]。当你解开所有这些，你会发现，R1 = [Y|[3]]，并回忆起Y绑定到 1，结果是R1 = [1,3].