参数在子句/2中未被充分实例化

Question

我试图为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需要实例化的论证，或者我可能遗漏了其他什么东西？

谢谢你的帮助

Answer 1

正如Ness在评论中指出的那样，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的一个子句。不允许这样做。在使元解释器的子句相互排斥时，您必须更加小心。你可能需要把刀子放进去。