Prolog使用DCGs反转字符串时如何终止递归？

我正在使用Scryer Prolog，从Power of Prolog油管频道获取了如下DCG代码：

qes([]) --> [].
qes([L|Ls]) --> qes(Ls), [L].

通过listing(qes/3)命令得到其Prolog子句形式（注：原输出存在笔误，已修正关键逻辑）：

?- listing(qes/3).
qes([],A,B) :-
   A=B.
qes([L|Ls],A,B) :-
   qes(Ls,A,C),
   C=[L|B].

我尝试逐行分析其执行过程：当调用phrase(qes(X), "abc")时，它会被内部转换为qes(X, "abc", [])。

首先进行合一：X = [L|Ls]，A = "abc"，B = []。Prolog尝试匹配基例，但"abc"不等于[]。

第一次调用：

qes([L1|Ls1], "abc", []) :- qes(Ls1,"abc",C1), C1=[L1|[]].

第二次调用：

qes([L2|Ls2], "abc", C1) :- qes(Ls2,"abc",C2), C2=[L2|C1].

第三次调用类似。由于L和Ls都是变量，在基例成功前不会被绑定，我疑惑Prolog如何知道何时终止递归——看起来没有任何Ls会等于[]的情况，它是如何进入基例的？

解答 #

首先要明确：你看到的listing输出里存在笔误，第二个子句的C=[A|B]应该是C=[L|B]，这是DCG翻译的正确逻辑——DCG中的[L]对应状态转换C=[L|B]，其中C是递归调用后的输入状态，B是当前子句的输出状态。

关于递归终止的核心逻辑，关键在于Prolog的延迟合一特性：

1. 当调用phrase(qes(X), "abc")时，实际触发的是qes(X, "abc", [])。Prolog会优先尝试第二个子句（因为第一个子句要求第一个参数为[]，此时若X=[]会导致"abc"=[]，直接失败）。
2. 每次递归调用qes(Ls, A, C)时，Ls是未绑定的变量，直到某次递归中，Prolog尝试匹配基例qes([], A, B)——也就是要求Ls被实例化为[]。
3. 这个绑定不是提前判断出来的，而是通过反向合一完成的：
   • 递归展开三次后，会得到C3 = [L3|C2]、C2 = [L2|C1]、C1 = [L1|[]]，将这些串联起来就是C3 = [L3, L2, L1]。
   • 此时基例要求A = C3，也就是"abc" = [L3, L2, L1]，Prolog会完成合一：L3='a'、L2='b'、L1='c'，同时Ls3=[]（满足基例的第一个参数为[]的条件）。
4. 递归终止后，反向回溯绑定所有变量：Ls2=[L3|Ls3] = [a]，Ls1=[L2|Ls2] = [b,a]，最终X=[L1|Ls1] = [c,b,a]，也就是输入字符串的反转。

本质上，Prolog不是“提前知道”何时终止，而是通过递归展开后，基例的合一要求反向推导出变量的绑定，从而满足终止条件。你可以直接运行phrase(qes(X), "abc")验证，会得到X = "cba"的结果。

内容的提问来源于stack exchange，提问作者Zaynab Khan