求无循环的纯Prolog same_length/2实现方案

要实现纯逻辑、无循环且能处理same_length(L, [_|L])这类查询的版本，可通过约束驱动的方式实现，完全避免var/1这类不纯的元逻辑谓词，同时保持原定义的纯特性。

基于CLP(FD)的最优纯实现 #

借助CLP(FD)的长度约束，将两个列表的长度绑定为同一变量，让Prolog自动处理约束求解，从根源避免无限递归：

:- use_module(library(clpfd)).

same_length(A, B) :-
    length(A, Len),
    length(B, Len).

测试目标查询时，会直接返回无解（因为Len = Len + 1无整数解），不会陷入循环：

?- same_length(L, [_|L]).
false.

这个实现的纯逻辑特性完整：

• 支持所有方向的查询：已知两列表判断长度、给定单列表求同长列表、变量列表枚举等
• 对存在明确矛盾的查询（如same_length(L, [_|L])）能直接终止并返回结果
• 未使用任何破坏纯逻辑的元谓词

无库依赖的纯递归实现 #

如果不想依赖CLP(FD)库，可通过同步遍历+显式长度校验的纯递归版本实现，核心是对已实例化的列表提前校验长度，避免无约束的变量扩展：

same_length([], []).
same_length([_|As], [_|Bs]) :-
    same_length(As, Bs).
same_length(A, B) :-
    ground(A), ground(B),
    length(A, LenA), length(B, LenB),
    LenA = LenB.

该版本对same_length(L, [_|L])这类查询能终止返回false，但在枚举所有同长列表对（如same_length(L1, L2)）时仍会进入预期的无限枚举（这类查询本身无法终止，符合问题备注说明）。

核心原理说明 #

原定义的循环问题源于：当L为变量时，[_|L]会不断递归扩展L为[_|...]，形成无限递归链。纯逻辑实现的关键是提前绑定长度相等约束，而非依赖无约束的递归扩展，从逻辑层面阻断无限递归的可能。

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