3

让我们定义自定义运算符 - 顺其自然++，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

返回

yes

如何在 Prolog 中实现这一点？（代码片段，请。有可能吗？我错过了什么吗？）

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

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

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

此外

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

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

可能的结果之一（感谢@mat 向其他人展示）

X=c, Y=a

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

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

4

2 回答 2

5

您的表示称为“默认”：为了处理这种形式的表达式，您需要一个“默认”案例，或显式检查 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 这样的术语检查谓词来系统地处理所有情况，但它们通常会阻止或至少阻碍好的声明性解决方案可以在各个方向使用来测试并生成所有案例。

于 2011-08-29T15:07:12.640 回答
0

这个问题相当古老，但无论如何我都会发布我的解决方案。我在业余时间学习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 生成一个长度，而第二次调用将长度作为约束。切割是必要的，因为第一次调用可能会继续生成不断增长的列表，这些列表将永远不会再次与第二个列表匹配，从而导致无限递归。我还没有找到更好的解决方案...

感谢您发布如此有趣的问题！

/彼得

编辑： 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.
于 2013-11-30T05:15:59.553 回答