Этот вопрос довольно старый, но я все равно выложу свое решение. В свободное время я изучаю пролог и нашел, что это довольно сложная проблема.
Я многое узнал о DCG и списках различий. Боюсь, я не придумала решение, которое не использует списки. Как и предложенный mat, он преобразует термины в плоские списки, чтобы справиться с круглыми скобками, и использует permutation/2 для сопоставления списков, учитывая коммутативный характер оператора ++ ...
Вот что я придумал:
:- op(900, yfx, equ).
:- op(800, xfy, ++).
check(A equ B) :- A equ B.
equ(A,B) :- sum_pp(A,AL,Len), sum_pp(B,BL,Len), !, permutation(AL, BL).
sum_pp(Term, List, Len) :- sum_pp_(Term, List,[], 0,Len).
sum_pp_(A, [A|X],X, N0,N) :- nonvar(A), A\=(_++_), N is N0+1.
sum_pp_(A, [A|X],X, N0,N) :- var(A), N is N0+1.
sum_pp_(A1++A2, L1,L3, N0,N) :-
sum_pp_(A1, L1,L2, N0,N1), (nonvar(N), N1>=N -> !,fail; true),
sum_pp_(A2, L2,L3, N1,N).
Предикат sum_pp/3 - это рабочая лошадка, которая берет термин и преобразует его в плоский список слагаемых, возвращая (или проверяя) длину, в то же время не подвергаясь скобкам. Это очень похоже на правило DCG (с использованием списков различий), но оно написано как обычный предикат, потому что оно использует длину, чтобы помочь разбить левую рекурсию, которая в противном случае привела бы к бесконечной рекурсии (мне потребовалось довольно много времени, чтобы победить ее) .
Может проверять наземные условия:
?- sum_pp(((a++b)++x++y)++c++d, L, N).
L = [a,b,x,y,c,d],
N = 6 ;
false.
Он также генерирует решения:
?- sum_pp((b++X++y)++c, L, 5).
X = (_G908++_G909),
L = [b,_G908,_G909,y,c] ;
false.
?- sum_pp((a++X++b)++Y, L, 5).
Y = (_G935++_G936),
L = [a,X,b,_G935,_G936] ;
X = (_G920++_G921),
L = [a,_G920,_G921,b,Y] ;
false.
?- sum_pp(Y, L, N).
L = [Y],
N = 1 ;
Y = (_G827++_G828),
L = [_G827,_G828],
N = 2 ;
Y = (_G827++_G836++_G837),
L = [_G827,_G836,_G837],
N = 3 .
Оператор equ/2 "объединяет" два термина и может также предоставить решения, если есть переменные:
?- a++b++c++d equ c++d++b++a.
true ;
false.
?- a++(b++c) equ (c++a)++b.
true ;
false.
?- a++(b++X) equ (c++Y)++b.
X = c,
Y = a ;
false.
?- (a++b)++X equ c++Y.
X = c,
Y = (a++b) ;
X = c,
Y = (b++a) ;
false.
В правиле equ / 2
equ(A,B) :- sum_pp(A,AL,Len), sum_pp(B,BL,Len), !, permutation(AL, BL).
первый вызов sum_pp генерирует длину, а второй вызов принимает длину в качестве ограничения. Сокращение необходимо, потому что первый вызов может продолжать генерировать постоянно растущие списки, которые никогда больше не будут совпадать со вторым списком, что приведет к бесконечной рекурсии. Я еще не нашел лучшего решения ...
Спасибо за публикацию такой интересной проблемы!
/ Peter
edit: sum_pp_ записано как правила DCG:
sum_pp(Term, List, Len) :- sum_pp_(Term, 0,Len, List, []).
sum_pp_(A, N0,N) --> { nonvar(A), A\=(_++_), N is N0+1 }, [A].
sum_pp_(A, N0,N) --> { var(A), N is N0+1 }, [A].
sum_pp_(A1++A2, N0,N) -->
sum_pp_(A1, N0,N1), { nonvar(N), N1>=N -> !,fail; true },
sum_pp_(A2, N1,N).
Обновление:
sum_pp(Term, List, Len) :-
( ground(Term)
-> sum_pp_chk(Term, 0,Len, List, []), ! % deterministic
; length(List, Len), Len>0,
sum_pp_gen(Term, 0,Len, List, [])
).
sum_pp_chk(A, N0,N) --> { A\=(_++_), N is N0+1 }, [A].
sum_pp_chk(A1++A2, N0,N) --> sum_pp_chk(A1, N0,N1), sum_pp_chk(A2, N1,N).
sum_pp_gen(A, N0,N) --> { nonvar(A), A\=(_++_), N is N0+1 }, [A].
sum_pp_gen(A, N0,N) --> { var(A), N is N0+1 }, [A].
sum_pp_gen(A1++A2, N0,N) -->
{ nonvar(N), N0+2>N -> !,fail; true }, sum_pp_gen(A1, N0,N1),
{ nonvar(N), N1+1>N -> !,fail; true }, sum_pp_gen(A2, N1,N).
Я разделил sum_pp на два варианта. Первая - это тонкая версия, которая проверяет основные термины и является детерминированной. Второй вариант вызывает length/2 для выполнения некоторого итеративного углубления, чтобы не допустить того, чтобы левая рекурсия убежала до того, как правый рекурсон получит возможность что-то произвести. Вместе с проверками длины перед каждым рекурсивным вызовом это теперь бесконечное доказательство рекурсии для гораздо большего числа случаев, чем раньше.
В частности, теперь работают следующие запросы:
?- sum_pp(Y, L, N).
L = [Y],
N = 1 ;
Y = (_G1515++_G1518),
L = [_G1515,_G1518],
N = 2 .
?- sum_pp(Y, [a,b,c], N).
Y = (a++b++c),
N = 3 ;
Y = ((a++b)++c),
N = 3 ;
false.