正如Will Ness在评论中指出的那样，
我正在尝试为prolog中的统一编写一个简单的元解释器，这就是我迄今为止得到的
unify(A,B):-var(A),A=B.
unify(A,B):-nonvar(A),var(B),B=A.
unify(A,B):-compound(A),compound(B),A=..[F|ArgsA],B=..[F|ArgsB],unify_args(ArgsA,ArgsB).
unify_args([A|TA],[B|TB]):-unify(A,B),unify_args(TA,TB).
unify_args([],[]).
meta(true).
meta((A,B)):- meta(A),meta(B).
meta(C):-clause(H,B), unify(H,C), meta(B).
我遇到的问题是，当我试图统一两个变量时，例如
meta((A,B)).
我得到正确的结果
A = B, B = true .
但当我试图统一其他任何东西时，例如
meta((a,a)).
或者甚至是计算机，我得到以下错误：
ERROR: Arguments are not sufficiently instantiated
ERROR: In:
ERROR: [12] clause(_4306,_4308)
ERROR: [11] meta(a) at path_redacted/unify1.pl:22
ERROR: [10] meta((a,a)) at path_redacted/unify1.pl:21
ERROR: [9] <user>
我不明白为什么在这种特殊的情况下，子句/2需要实例化argouments，或者我可能遗漏了其他东西？
感谢您的帮助
clause/2需要实例化Head。
正如所写的，元解释器试图枚举程序中所有谓词的所有子句，以找到与目标术语C一致的子句。您必须将其限制为仅枚举与C匹配的子句。一种方法是直接调用clause(C, Body)。我想你想避免这种情况，因为这会通过为你做统一来欺骗你。
另一种方法是复制C的函子，但不复制其参数。您可以使用此副本查找感兴趣谓词的子句，但您仍然可以自己进行统一。
以下是如何做到这样的"；骨架；副本：
?- C = f(x, y), functor(C, Functor, Arity), functor(Skeleton, Functor, Arity).
C = f(x, y),
Functor = f,
Arity = 2,
Skeleton = f(_70, _72).
在元解释器的上下文中，这样的东西可以让你更接近你想要的东西：
meta(Goal) :-
functor(Goal, Functor, Arity),
functor(Head, Functor, Arity),
clause(Head, Body),
unify(Head, Goal),
meta(Body).
例如，使用以下示例程序：
f(x).
g(y).
fg(X, Y) :-
f(X),
g(Y).
我们得到：
?- meta(fg(X, Y)).
X = x,
Y = y ;
ERROR: No permission to access private_procedure `true/0'
ERROR: In:
ERROR: [12] clause(true,_2750)
...
解决方案是正确的，但回溯以获得进一步的答案会尝试访问true的子句。SWI Prolog不允许这样做。在使元解释器的子句互斥时，您必须更加小心。您可能需要进行切割。