如何定义一个元逻辑谓词,使用当前ISO标准(ISO / IEC 13211-1:1995,包括Cor.2)的内置函数,测试(因此仅成功或失败)两个唯一变量列表是否完全相同。
换句话说,如果一个唯一变量列表是另一个列表的排列,则该谓词应该成功。类比于library(ordsets)
,我们将这个元逻辑谓词称为varset_seteq(As, Bs)。
请注意,与ord_seteq/2
相比,这个谓词不能简单地写作As == Bs
。
如何定义一个元逻辑谓词,使用当前ISO标准(ISO / IEC 13211-1:1995,包括Cor.2)的内置函数,测试(因此仅成功或失败)两个唯一变量列表是否完全相同。
换句话说,如果一个唯一变量列表是另一个列表的排列,则该谓词应该成功。类比于library(ordsets)
,我们将这个元逻辑谓词称为varset_seteq(As, Bs)。
请注意,与ord_seteq/2
相比,这个谓词不能简单地写作As == Bs
。
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.
term_variables/2
可以利用它必须检查第二个参数的完整性这个事实,所以计算其长度是免费的,这样就可以更早地失败。 - falsevarset_seteq([A,B,a], [A,B])
不会成功吗? - Shon如果我们假设这两个列表包含唯一变量,那么使用双重否定的方法如下:
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的解决方案类似,但避免了变量排序仅在单个sort/2
执行中保持一致的问题。
<?php foreach ($array as $key => $value) echo "<p>$key: $value</p>"; ?>
varset_seteq(As, Bs) :-
sort(As, Sa), sort(Bs, Sb), Sa == Sb.
varlist/1
谓词来检查两个列表是否由变量组成。但后来我意识到,Tudor Berariu指出,这种方法在例如As = [A,A,B,C], Bs = [B,C,B,C,A]
的情况下也会成功。我可能应该也保留我的原始尝试.. - ShonSa == Sb
处,不能再保证Sa
和Sb
仍然是排序的。想象一下,在不保留变量顺序的实现中发生GC的情况 - 当它在sort/2
期间不调用GC时,仍可能符合要求。 - falseord_seteq/1
一样期望但不测试有序集)。 - Shon另一种方法。如果我们提供给自己这些更高级的谓词(每个都很有用),
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).
< p >(至少在 SWI Prolog 上,使用 sort/2
比上述方法需要更少的推理次数。据推测这是因为排序在 C 中完成。此外,这个答案仍然没有达到term_vars/2
方法的优雅——这就是“语义上升”的威力 :))< /p >
As
和Bs
是否真的是自由变量集合。在我的答案中,这可以通过它们必须与term_variables/2
的第二个参数统一来保证。 - Tudor Berariuvarset_seteq([A+B,a],[])
在许多系统中都会成功(默认情况下)。...并统一参数。 - false