Prolog:如何做 "check(a++b++c++d equals d++a++c++b) -> yes"

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

返回

yes

如何在 Prolog 中实现它？(请提供代码片段。这可能吗？我错过了什么吗？)

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

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

P.P.S '++' 才刚刚开始。我想添加更多的运算符(operator)。这就是为什么我担心将内容放入列表可能不是好的解决方案。

此外

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

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])。

Answer 1

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