Блог

Я работаю над реализацией алгоритма унификации для системы перезаписи терминов в Prolog. Чтобы полностью реализовать это, мне нужен предикат, заменяющий данный подтерм на другой термин. К сожалению, способ, которым Prolog создает новые переменные, не позволяет системе успешно достичь этого. У меня есть несколько встроенных операторов, star и divi (на самом деле просто представляющих символы * и /, но в форме префикса). Мой замещающий предикат состоит из следующих предикатов:

 replace(A,B, [], []).
replace(A,B, [H|T], [B|T2]) :- (H==A)->replace(A, B, T, T2).
replace(A,B, [H|T], [H|T2]) :- (H==A)->replace(A, B, T, T2).

replace_lst([], [H|T], [H2|T2]).
replace_lst([H1|T1], [H|T], [H2|T2]) :- 
    arg(1,H1,X),
    arg(2,H1,Y),
    replace(X,Y,[H|T],[H2|T2]),
    replace_lst(T1,[H|T],[H2|T2]).

substitute([H|T],A,X):-
    A=..List,
    replace_lst([H|T],List,C),
    X=..C.
 

Проблема заключается в том, что, например, термины star(X, X) и star(Y, Y), по логике моей системы перезаписи, структурно эквивалентны и не требуют такой замены. Однако сравнение этих двух терминов с использованием унифицируемого предиката приведет Prolog к попытке унификации для двух, и результирующий термин больше не эквивалентен по структуре исходной структуре star(X, X). Поэтому я попытался проверить равенство терминов через их структуру, но это приводит к еще одному набору червей, в котором, например, моя система перезаписи содержит правило перезаписи:

звезда (X, X)==>X.

Однако попытка замены на основе оператора равенства вариантов =@= приводит к тому, что Prolog видит два разных экземпляра терминов с той же структурой, что и у одного и того же термина. Поэтому определение предиката подстановки на основе вариантов следующим образом:

 variant_replace(A,B, [], []).
variant_replace(A,B, [H|T], [B|T2]) :- (H=@=A)->variant_replace(A, B, T, T2).
variant_replace(A,B, [H|T], [H|T2]) :- (H=@=A)->variant_replace(A, B, T, T2).

variant_replace_lst([], [H|T], [H2|T2]).
variant_replace_lst([H1|T1], [H|T], [H2|T2]) :- 
    arg(1,H1,X),
    arg(2,H1,Y),
    variant_replace(X,Y,[H|T],[H2|T2]),
    variant_replace_lst(T1,[H|T],[H2|T2]).


variant_substitute([H|T],A,X):-
    A=..List,
    variant_replace_lst([H|T],List,C),
    X=..C.

 

Приводит к проблеме, когда, если у меня есть какой-то термин:

 star((star(X,Y),star(A,B))

 

и я хочу заменить подтерм звезды (X, Y) следующим предикатом:

 ?- variant_substitute([star(X,Y)=hole],star(star(X,Y),star(A,B)),D).
D = star(hole, hole) .

 

Мы можем видеть, что Prolog, по логике предиката подстановки вариантов, просто проверяет условия заданной структуры, игнорируя фактическое создание экземпляра переменной. Поэтому мне нужен способ объявления переменных. Я хочу иметь систему, которая может использовать метапеременные, объявленные таким образом, чтобы каждый заданный термин имел до N уникальных переменных в диапазоне значений от V(0) до V (N-1). В идеале такая система метапеременных должна выглядеть так:

  substitute([star(v(0),v(1))=hole],star(star(v(0),v(1)),star(v(2),v(3))),D).
D = star(hole, star(v(2), v(3)))

 

Мне нужно, чтобы Prolog видел термины, обозначаемые с помощью v(#) в качестве переменных, поскольку мне нужно будет использовать унифицируемый предикат в будущем, чтобы сравнить их с исходным объявлением моих правил перезаписи, которое объявлено следующим образом :

 star(X,X) ==> X.
divi(X,X) ==>  X.
divi(star(X,Y),Y) ==>  X.
star(divi(X,Y),Y) ==>  X.
star(X, star(Y,Z)) ==> star(star(divi(X,Z),Y),Z).
divi(X, star(Y,Z)) ==> star(divi(divi(X,Z),Y),Z).
star(X, divi(Y,Z)) ==> divi(star(star(X,Z),Y),Z).
divi(X, divi(Y,Z)) ==> divi(divi(star(X,Z),Y),Z).

 

Каков наилучший способ реализовать этот формат метапеременных в Prolog?