Prolog 是和 =。为什么它们的工作方式与逻辑约束不同？答案

【问题标题】：Prolog is and =. Why don't they work the same way as the logical constraints?Prolog 是和 =。为什么它们的工作方式与逻辑约束不同？
【发布时间】：2011-02-16 03:15:13
【问题描述】：

我对 prolog 还是很陌生，我正试图弄清楚为什么数学约束似乎不像逻辑约束那样起作用。

似乎有足够的信息来解决这个问题：

f(A, B) :- A = (B xor 2).

但是当我尝试f(C, 3) 时，我会返回C = 3 xor 2.，这不是很有帮助。更没用的是，如果输入反转，它根本无法找到解决方案。使用 is 而不是 = 会使示例输入返回正确的答案，但反过来甚至拒绝尝试任何事情。

从我之前的实验来看，我似乎可以编写一个函数，使用二进制文件在逻辑上执行此操作而不会遇到麻烦，而且它实际上是双向的。是什么让数学与众不同？

作为参考，我第一次尝试解决我的问题是这样的：

f（输入，输出）：- A 是输入异或（输入 >> 11）， B 是 A xor ((A >> 7) /\ 2636928640)， C 是 B xor ((B > 18)。

从输入到输出都可以正常工作，但反之则不行。如果我将is 切换到=，它会产生一个长逻辑序列，其中的值被替换但找不到数值解。

我正在使用内置xor 的swi-prolog，但它也可以很容易地定义。我希望能够使用 prolog 在两个方向上运行此功能，并且真的不想手动实现逻辑行为。欢迎任何关于我如何重新表述问题的建议。

【问题讨论】：

标签： prolog bitwise-operators

【解决方案1】：

Pure Prolog 不应该处理数学。驱动 Prolog 的基本算法 - 失败时统一和回溯 - 没有提到算术运算符。大多数 Prolog 实现都在其字节码中添加了算术作为丑陋的 hack。

这样做的原因是算术函数的作用方式与函子不同。它们不能以相同的方式统一。并非每个函数都保证适用于地面和非地面参数的每种组合。例如，将 X 提升到 Y 次方的算法对于求 X 的 Y 次根不是对称的。如果所有算术函数都是对称的，那么加密和密码学就无法工作！

也就是说，以下是关于 Prolog 运算符的缺失事实：

首先，'=' 在 Prolog 中不是“等于”，而是“统一”。目标X = Y op Z 其中op 是一个运算符，将X 与函子'op'(Y,Z) 统一起来。它与算术相等或赋值无关。

其次，is，丑陋的数学黑客，不保证是可逆的。目标X is Expr，其中Expr 是一个算术表达式，首先计算表达式，然后尝试将其分配给X。它并不总是适用于数字和变量的每种组合 - 检查您的 Prolog 库文档。

总结一下：

编写可逆数学函数需要数学知识和算法来使函数可逆。在这种情况下，Prolog 不会为您施展魔法。
如果您正在寻找智能方程求解，您可能需要检查有限域和连续域的 Prolog 约束求解库。与可逆数学不同，但比 Prolog 朴素的算术运算符更聪明。

【讨论】：

谢谢，这对我来说很好。我想我毕竟必须基于二进制来实现我的问题，因为我知道它是对称的，但正如你所说，Prolog 不知道这一点是完全合理的。

【解决方案2】：

如果你想比较表达式的计算结果，你应该使用运算符（=:=）/2，或者在检查分离度时使用运算符（=/=）/2。

该运算符也适用于按位运算，因为按位运算适用于整数，而整数是数字。操作员是 ISO 核心标准的一部分。对于以下子句：

f(A, B) :- A =:= (B xor 2).

我在 SWI-Prolog、Jekejeke Prolog 等中得到以下运行：

Welcome to SWI-Prolog (Multi-threaded, 64 bits, Version 7.3.31)
Copyright (c) 1990-2016 University of Amsterdam, VU Amsterdam

?- f(100, 102).
true.

?- f(102, 100).
true.

?- f(100, 101).
false.

如果您想要一种更具声明性的方式来处理位，您可以使用集成到 Prolog 中的 SAT 求解器。一个好的 SAT 求解器还应该支持有限或无限位向量，但我目前无法确定这里有什么可用以及有什么限制。

例如在此处查看此问题： Prolog SAT Solver

【讨论】：