我需要知道变量是否在给定规则中被实例化,但我不允许使用var(X),并且不知道如何这样做.
具体来说,我的规则得到4个参数(P,A,B,C).
如果P,A,B,C被实例化,则我的规则应该"返回"为真iff(A + B)mod(P)= C(mod(P)).
如果AB和C中的一个没有被实现,我应该返回它的哪个值将保证(A + B)mod(P)= C(mod(P)).因此,例如,如果C未被实例化,则规则应该"返回"(A + B)mod(P)为C,并且如果A或B未被实例化,则类似的行为.编写每个规则很容易,但是如果我不知道变量是否被实例化,我怎么知道我所处的情况呢？如前所述,我不能使用var(X)或数字(X)等,我只能假设P总是被实例化.
提前致谢!
我认为@mat答案肯定是解决问题的方法.
但是,如果你想检查一个变量是否没有使用内置的谓词var/1来实例化(由于某些限制,例如你的老师明确禁止它),你可以使用两次双重否定来测试绑定的能力一个变量没有真正实例化它,如果它没有绑定:
not_inst(Var):-
\+(\+(Var=0)),
\+(\+(Var=1)).
测试用例:
?- not_inst(X).
true.
?- not_inst(a).
false.
手动测试某些东西是否被实例化使得正确处理实践中可能出现的所有情况变得非常困难。对于您没有考虑过的某些实例化模式，您生成的代码几乎总是会表现不正确。
幸运的是，对于此类问题有一个声明性的解决方案：约束在所有情况下都能正确工作，无论实例化什么和未实例化什么。
例如，使用 Prolog 系统的CLP(FD) 约束来解决您的任务：
:- use_module(library(clpfd)).
same_sum_mod(A, B, C, P) :-
(A+B) mod P #= C mod P.
它在各个方向上都能正常工作，例如：
?- same_sum_mod(1, 2, 3, 3).
true.
?- same_sum_mod(1, B, 3, 2).
1+B#=_G823,
_G823 mod 2#=1.
?- same_sum_mod(1, 2, 3, P).
P in inf..-1\/1..sup,
3 mod P#=_G855,
3 mod P#=_G855.
还要检查以下情况，其中B最初未实例化，但其域已知，并且约束求解器可以推导出单个可接受的解决方案：
?- 0..1 中的 B，same_sum_mod(1, B, 3, 2)。 B = 0。
这种情况不能通过简单的实例化检查来处理，而是需要对约束进行推理。
有关 CLP(FD) 约束的更多信息，请参阅clpfd 。