18

如何使用当前 ISO 标准（ISO/IEC 13211-1 :1995，包括Cor. 2 )。

换句话说，如果一个唯一变量列表是另一个变量的排列，则谓词应该成功。与 类比library(ordsets)，我们称这个元逻辑谓词 varset_seteq(As, Bs).

请注意，与 相比ord_seteq/2，此谓词不能是简单As == Bs的 。

4

4 回答 4

14

我提出的解决方案term_variables/2用于检查是否Bs没有多余的变量，As并且As没有没有出现在Bs.

varset_seteq(As, Bs):-
    term_variables(As-Bs, As),
    term_variables(Bs-As, Bs).

使用不是自由变量集的参数可以欺骗上述解决方案：

 | ?- varset_seteq([A], [a]).

 A = a

 yes

为了避免这种情况，可以用等价测试代替统一：

varset_seteq(As, Bs):-
    term_variables(As-Bs, A0),
    A0 == As,
    term_variables(Bs-As, B0),
    B0 == Bs.
于 2015-01-13T17:24:49.417 回答
7

如果我们可以假设这两个列表包含唯一变量，那么以下双重否定的使用是有效的：

varset_seteq(As, Bs) :-
    \+ \+ (numbered_from(As, 1),
           sort(Bs, SBs),
           As == SBs).

numbered_from([], _).
numbered_from([X|Xs], X) :-
    X1 is X + 1,
    numbered_from(Xs, X1).

这类似于 Paulo 的解决方案，但避免了 ISO/IEC 13211-1 仅要求变量排序在sort/2.

于 2015-02-27T09:08:20.693 回答
4

另一个解决方案，效率低于Tudor 的聪明解决方案，因此不推荐，但仍然值得一提，因为我看到它被多次使用，是：

varset_seteq(As, Bs) :-
    sort(As, Sa), sort(Bs, Sb), Sa == Sb.
于 2015-02-25T11:23:34.810 回答
3

另一种方法。如果我们为自己提供这些更高阶的谓词（它们各自都有用），

select_with(_, _, [], []).
select_with(P, X, [Y|Ys], Ys)     :- call(P, X, Y), !.
select_with(P, X, [Y|Ys], [Y|Ks]) :-
    select_with(P, X, Ys, Ks).

foldl(_,[],Vn,Vn).
foldl(P,[X|Xs],V0,Vn) :- 
    call(P,X,V0,V1),
    foldl_(P,Xs,V1,Vn).

那么我们可以很容易地定义一个谓词，如果一个列表中的每个成员在另一个列表中具有相等的元素（使用==/2），则该谓词为真：

members_equal(A, B :-
    foldl(select_with(==), A, B, []).

如果我们验证传入的参数是 varsets，那么这个谓词可以专门用于指定的目的。以下是我能够在这个方向上提出的最好的（但它吞噬了很多推论）：

is_varset([]).
is_varset([V|Vs]) :-
    var(V),
    maplist(\==(V), Vs),
    is_varset(Vs).

（至少在 SWI Prolog 上， usingsort/2比上面的推论要少。大概这是因为排序是在 C 中完成的。而且，这个答案仍然没有接近方法的优雅term_vars/2——这就是“语义上升”的力量” :)

于 2015-02-25T14:47:47.617 回答