9 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,你需要考虑的谓词没有的功能,你通常会在其他语言.谓词描述了可能包含有助于定义该关系的参数的关系.
例如,让我们来看看这个简单的例子:
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并且Rest是一个由所有其他元素组成的列表(没有X).(注意:你没有直接解释这个含义,但我从你的例子的实现中确定了这个含义.)
现在我们可以写出来描述规则.首先,一个简单的基础案例:
val_and_remainder(X,[X|Xs],Xs).
这表示:
Xs是[X|Xs]没有的列表的剩余部分X.
通过[X|Xs]Prolog中列表的语法定义,这个陈述应该非常明显.您需要所有这些参数,因为第三个参数Xs必须与list的尾部(rest)统一,[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,如果R是列表的其余部分Ys没有元素X.
你需要考虑这个规则来说服自己,这在逻辑上是正确的.该Y排在第二和第三个参数,因为它们指的是同一个元素是相同的,所以他们必须统一.
因此,这两个谓词条款形成了两个涵盖这两个案例的规则.第一种情况是简单的情况,其中X是列表的第一个元素.第二种情况是when X不是第一个元素的递归定义.
当您进行查询时,例如val_and_remainder(2, [1,2,3], R).Prolog会查看它是否可以将该术语与事实或谓词子句的头部统一起来val_and_remainder(2, [1,2,3], R).它不能在试图与统一val_and_remainder(X,[X|Xs],Xs),因为它需要统一X同2,这意味着它需要统一[1,2,3]与[2|Xs]该失败自的第一个元素[1,2,3]是1,但的第一个元素[2|Xs]是2.
所以Prolog的移动上,并成功地统一val_and_remainder(2, [1,2,3], R)与val_and_remainder(X,[Y|Ys],[Y|R])通过统一X与2,Y1,Ys与[2,3]和R用[Y|R](注意,这是很重要的,在R您的通话变量是不一样的R谓词中定义的变量,所以我们应该命名此R1来避免这种混乱).我们将你的名字命名R为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].