如何修复Prolog中rev/2列表反转谓词的反向查询资源耗尽问题

问题原因 #

两个版本的rev/2出现反向查询（第一个参数为自由变量、第二个参数为固定列表）超时的核心原因是：没有对两个参数的长度做前置约束，Prolog的回溯机制会在得到第一个正确解后，无限尝试为第一个自由变量生成更长的列表进行匹配，最终耗尽系统资源。

问题1：修复方案 #

我们可以通过新增等长约束的方式解决终止性问题，首先实现通用的列表等长判断谓词：

same_length([], []).
same_length([_|T1], [_|T2]) :- same_length(T1, T2).

该谓词会保证两个输入列表长度完全一致，当其中一个列表为固定值时，另一个列表的长度也会被同步约束，避免无限生成长列表。

针对基于append的朴素实现修复 #

将原有实现封装为内部谓词，在入口处先做等长校验：

rev(L, R) :-
    same_length(L, R),
    rev_unsafe(L, R).

rev_unsafe([], []).
rev_unsafe([XH|XT], Y) :-
  rev_unsafe(XT, Z),
  append(Z, [XH], Y).

append([], Y, Y).
append([XH|XT], Y, [XH|ZT]) :-
  append(XT, Y, ZT).

针对尾递归实现修复 #

同样在入口处增加等长校验即可：

rev(L, R) :-
    same_length(L, R),
    revappend(L, [], R).

revappend([], Y, Y).
revappend([XH|XT], Y, Z) :-
  revappend(XT, [XH|Y], Z).

修复后执行反向查询?- rev(X, [a, b, c]).，会正常返回结果：

?- rev(X, [a, b, c]).
   X = [c, b, a]
;  false.

问题2：修复前后的等价性 #

两者并非完全等价，差异仅体现在终止性和自由变量的搜索行为上：

• 当两个输入参数都是完全绑定的ground列表时，修复前后的输出结果完全一致，没有任何差异。
• 当存在自由变量时：
  • 原程序在反向查询（第二个参数固定、第一个参数自由）场景下，得到第一个解后不会终止，会无限搜索更长的列表。
  • 修复后的程序只要任意一个输入是有限的ground列表，就会在遍历完所有可能解后正常终止；如果两个参数都是自由变量，两者都会生成无限的列表反转对，但修复后的版本会按长度有序生成，不会出现无意义的资源耗尽。
• 从逻辑语义上看，修复后的程序不会新增原程序没有的解，也不会漏掉原程序的正确解，仅解决了原程序的非终止缺陷。

内容的提问来源于stack exchange，提问作者Géry Ogam