Prolog: how to do it "check (a ++ b ++ C ++ d equals d ++ a ++ C ++ b) & # 8594; yes"

Question

Define custom operators - let it be ++ , equals

 :- op(900, yfx, equals). :- op(800, xfy, ++). 

And the fact:

 check(A equals A). 

I am trying to make a predicate, let it be check/1 , which will return true in all of the following situations:

 check( a ++ b ++ c ++ d equals c ++ d ++ b ++ a ), check( a ++ b ++ c ++ d equals d ++ a ++ c ++ b), check( a ++ b ++ c ++ d equals d ++ b ++ c ++ a ), % and all permutations... of any amount of atoms check( a ++ ( b ++ c ) equals (c ++ a) ++ b), % be resistant to any type of parentheses 

return

 yes 

How to implement this in Prolog? (code snippet, please. Is this possible? Am I missing something?)

Gnu-Prolog is preferred, but SWI-Prolog is also possible.

PS Handle the code like a pseudo-code project, and don’t worry about minor syntax issues.

PPS '++' is just beginning. I would like to add more operators. This is why I am afraid that listing material may not be the best solution.

Additionally

In addition, it would be nice if requests were possible (but this part is not required , if you can answer the first part, this is great and enough)

 check( a ++ (b ++ X) equals (c ++ Y) ++ b) ) 

one of the possible results (thanks @mat for showing others)

 X=c, Y=a 

Basically, I am looking for a solution to the first part of the question - a yes / no check.

The second part with X, Y will be a nice addition. In it X, Y must be simple atoms. For the above examples of domains for X, Y the following are indicated: domain(X,[a,b,c]),domain(Y,[a,b,c]) .

Answer 1

Your representation is called "defaulty": to process expressions of this form, you need a "default case" or an explicit check for atom / 1 (which is not monotonous) - you cannot use pattern matching directly to handle all cases. As a result, consider your case again:

 check( a ++ (b ++ X) equals (c ++ Y) ++ b) ) 

You say that this should answer X=c, Y=a . However, it can also answer X = (c ++ d), Y = (a ++ d) . Should this solution also arise? If not, it will not be monotonous and thus greatly complicate declarative debugging and reasoning about your program. In your case, would it make sense to present expressions such as lists? For example, [a, b, c, d] is equal to [c, d, b, a]? Then you can simply use the predicate permutation of the / 2 library to check if such "expressions" are equal.

Of course, it is also possible to work with incomplete representations, and in many cases they may be more convenient for users (think of the Prolog source code itself with its standard notation for purposes or Prolog arithmetic expressions). You can use nonmonotonic predicates such as var / 1 and atom / 1, as well as term test predicates such as functor / 3 and (= ..) / 2, to systematically handle all cases, but they usually prevent, or at least measure, interfere with good declarative solutions that can be used in all directions for testing, as well as generate all cases.

Answer 2

This question is pretty old, but I will post my solution anyway. I study prologue in my free time and found this rather complex problem.

I learned a lot about DCG and difference lists. I'm afraid I did not come up with a solution that does not use lists. Like the proposed layout, it converts terms to flat lists to deal with parentheses, and uses permutation/2 to match lists, given the commutative nature of the ++ operator ...

Here is what I came up with:

 :- 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). 

The predicate sum_pp/3 is a workhorse that accepts the term and converts it into a flat list of terms, returning (or checking) the length, being immune to parentheses. It is very similar to the DCG rule (using difference lists), but it is written as a regular predicate because it uses length to help break left recursion, which would otherwise lead to infinite recursion (it took me quite a while to defeat it )

He can check ground conditions:

 ?- sum_pp(((a++b)++x++y)++c++d, L, N). L = [a,b,x,y,c,d], N = 6 ; false. 

It also generates solutions:

 ?- 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 . 

The equ/2 operator "merges" two members and can also provide solutions if there are variables:

 ?- 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. 

In the equ / 2 rule

 equ(A,B) :- sum_pp(A,AL,Len), sum_pp(B,BL,Len), !, permutation(AL, BL). 

the first call to sum_pp generates a length, while the second call takes the length as a constraint. Reduction is necessary because the first call can continue to generate ever-growing lists that will never coincide with the second list, resulting in infinite recursion. I have not found a better solution ...

Thanks for posting such an interesting issue!

/ Peter

edit: sum_pp_, written as DCG rules:

 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). 

update:

 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). 

I divided sum_pp into two options. The first is a thin version that checks ground terms and is deterministic. The second option calls length/2 to do some iterative deepening to prevent the left recursion from disappearing before the right recurson gets a chance to create something. Together with length checks before each recursive call, this is now endless proof of recursion for many other cases than before.

In particular, the following queries are now executed:

 ?- 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.