Блог

я пытаюсь написать простой мета-интерпретатор для объединения в 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 в данном конкретном случае потребуются экземпляры аргументов, или, может быть, я что-то еще упускаю?

Спасибо за любую помощь

Как указано в комментарии, 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)
...
 

Решение найдено правильно, но при возврате для получения дальнейших ответов пытается получить доступ к предложению for true . Это не разрешено SWI-Prolog. Вам нужно будет быть более осторожным, чтобы сделать предложения мета-интерпретатора взаимоисключающими. Вероятно, вам нужно будет сделать надрезы.