测试该术语是不同变量的列表答案

【问题标题】：Test that term is a list of distinct variables测试该术语是不同变量的列表
【发布时间】：2014-12-29 00:51:18
【问题描述】：

在 ISO Prolog 中测试不同变量列表的最紧凑和最规范的方法是什么？我们称这个元逻辑谓词为is_varset/1。

因此，如果它的参数是一个完全不同的变量列表，它应该会成功。请注意，列表始终在其末尾包含 []。如果变量位于末尾，我们称其为部分列表（因此不是列表）。如果非变量项作为后缀出现，既不是[] 也不是变量，那么这既不是部分列表也不是列表。

术语既不是部分列表也不是列表的一个值得注意的特殊情况是无限列表。它们包含至少两个相同的后缀，实际上它们拥有无限这样的后缀。无限列表超出了标准的范围——所有创建它们的尝试都会导致结果未定义的 STO 统一。尽管如此，一些系统仍然支持它们，因此对于那些无限列表来说，理想情况下，is_varset/1 应该会无限失败。

?- is_varset([A|nonlist]).
false.

?- is_varset([A,B]), is_varset([B,A]).
true.

?- is_varset([A,B,A]).
false.

?- is_varset([A,f(B)]).
false.

?- is_varset([A|_]).
false.

?- L = [_|L], is_varset(L).  % may loop, should rather terminate
false.

这是 ISO/IEC 13211-1:1995 中的 overview of the built-ins，包括 Cor.2:2012。

【问题讨论】：

标签： prolog iso-prolog

【解决方案1】：

SWI-Prolog 中这个简单的定义似乎满足了要求

is_varset(Vs) :- /*is_list(Vs),*/ term_variables(Vs, T), T == Vs.

【讨论】：

看起来不错！你能证明为什么你不使用= 代替== 吗？
这个测试用例 ?- is_varset([A,f(B)]). 它在使用 (=)/2 时回答 B = f(B).。诚然，我只是根据直觉首先使用 (==)/2 ，并在您发表评论后再次测试...
如果用unify_with_occurs_check代替==呢？
逻辑上可行，我认为它可能会破坏线索......但我对内部运作的了解还不够，无法进一步推动这个假设......
"trashing the trail"，这是一些性能特征。但除此之外，是否会在成功时实例化变量？