Prolog：如何执行“检查(a++b++c++d 等于 d++a++ ;c++b) ->是的”

Question

让我们定义自定义运算符 - 让它为 ++、equals

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

事实上：

check(A equals A).

我尝试创建谓词，让它为 check/1，即在以下所有情况下将返回 true：

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

如何在 Prolog 中实现此功能？ （代码片段，请问。可能吗？我错过了什么吗？）

Gnu-Prolog 是首选，但 SWI-Prolog 是也可以接受。

PS 请将代码视为草稿“伪代码”，并且不要关心小的语法问题。

PPS“++”才刚刚开始。我想添加更多运算符。这就是为什么我担心将东西放入列表可能不是一个好的解决方案。

另外

，如果可以进行查询，那就太好了（但是，这部分不是必需的，如果您能够回答第一部分，那就太好了）

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

可能的结果之一（感谢@用于向其他人展示的垫子）

X=c, Y=a

我主要寻找问题第一部分的解决方案 - “是/否”检查。

第二部分 X,Y 将是很好的补充。其中X，Y应该是简单原子。对于上面的示例，X、Y 的域被指定为：domain(X,[a,b,c]),domain(Y,[a,b,c])。

Answer 1

您的表示称为“defaulty”：为了处理这种形式的表达式，您需要一个“default”情况，或者显式检查atom/1（这不是单调的） - 您不能直接使用模式匹配来处理所有情况。因此，再次考虑您的情况：

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

您说这应该回答 X=c, Y=a。但是，它也可以回答 X = (c ++ d), Y = (a ++ d)。这个解决方案也应该出现吗？如果不是，它就不会是单调的，从而使程序的声明式调试和推理变得非常复杂。在您的情况下，将此类表达式表示为列表有意义吗？例如，[a,b,c,d] 等于 [c,d,b,a]？然后，您可以简单地使用库谓词 permutation/2 来检查此类“表达式”是否相等。

当然也可以使用默认表示，并且在许多情况下，它们可能对用户更方便（想想 Prolog 源代码本身及其目标的默认表示法，或 Prolog 算术表达式）。您可以使用非单调谓词（如 var/1 和atom/1）以及术语检查谓词（如 functor/3 和 (=..)/2）来系统地处理所有情况，但它们通常会阻止或至少阻碍良好的声明性解决方案可以在各个方向上使用它来测试并生成所有案例。

Answer 2

这个问题相当老了，但无论如何我都会发布我的解决方案。我在业余时间学习 prolog，发现这是一个相当具有挑战性的问题。

我学到了很多关于 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

编辑：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.