clp(Z) 与 Kiselyov 关系算术

clp(Z) vs. Kiselyov relational arithmetic

我很难理解 clp(Z) 和另一个 relational arithmetic system used in MiniKanren 在功能上的区别。

特别是,clp(Z) 显然适用于 有界 场,而 Kiselyov 等人 被描述为适用于 无界 字段。

我尝试使用与无穷大和不确定相关的各种边缘情况,但除了 Kiselyov 等人 显然不支持区间和负数之外,我无法找到明显的差异数字。

基谢廖夫系统的point/advantage是什么?主要是实现比较简单,还是比较多?

好问题! 有许多方法可以执行关系算术,包括 CLP(Z)、CLP(FD)、"Kiselyov Arithmetic" 和关系 Peano Arithmetic。您还可以将算术限制为仅对基础数字起作用(否则会发出错误信号),或者延迟算术约束的评估,直到关系的参数变得足够基础以决定性地解决关系。

所有这些方法都很有用,而且它们都有自己的权衡。

我一直在考虑写一篇关于这个主题的短文。如果大家有兴趣,或许我们可以一起写出来。

为了简要回答您的问题,我们应该记住 CLP(Z) 和 CLP(FD) 之间的区别。 'CLP(X)' 代表 "Constraint Logic Programming over domain 'X'"。 CLP(FD) 在整数的有限域 (FD) 上运行。在 CLP(Z) 中,域是所有整数的集合,因此在大小上是无限的。

显然 FD 域包含在 Z 域中,那么为什么还要有一个单独的 CLP(FD) domain/solver?因为在受限域内解决问题可能会更快或更容易。事实上,一些在一个域中不可判定的问题可能在一个受限域内变得可判定。​​

In particular, clp(Z) apparently applies to bounded fields while Kiselyov et al. is described to apply to unbounded fields.

CLP(Z)中的Z域实际上是无界的。 CLP(FD) 中的 FD 域是有界的。在 Kiselyov 算术中,定义域是无界的。

Kiselyov 数字很有趣,因为一个数字可以表示无限组具体数字。例如,

(0 1 1)

是表示 6 的 Kiselyov 数字。(Kiselyov 数字是以小端顺序排列的二进制数字列表,这就是为什么 6 用前导“0”而不是前导“1”表示的原因。)

考虑这个 Kiselyov 数字:

`(1 . ,x)

其中 x 是一个 "fresh" 逻辑变量。这个 Kiselyov 数字表示 任何 正奇数。这是 Kiselyov Arithmetic 的一个优势:可以对部分实例化的数字执行操作,代表可能无限多的具体自然数,并且无需基于(可能无限多的)答案。将无限多个自然数表示为单个数字有时可以让我们一次推理出无限多个具体数字。 las,这仅适用于我们想要表示的基础自然数集可以使用

形式的 Kiselyov Numerals 表示的情况
`(<bit sequence that doesn't end in 0> . ,x)

Kiselyov Arithmetic 的一个缺点是每个算术关系都是 "solved" 立即:如果我们想将两个 Kiselyov 数相加,然后将结果乘以另一个 Kiselyov 数,我们必须执行完整的加法或先完成乘法,再进行其他运算。相比之下,CLP(Z) 或 CLP(FD) 求解器可以累积约束,在每一步检查可满足性,并且仅在计算结束时(一旦累积了所有约束)才执行完整求解。这种方法可以更有效,并且还可以发现一组约束中的不一致,如果天真地使用 Kiselyov Arithmetic 会发散。

other than Kiselyov et al. obviously not supporting intervals and negative numbers.

Kiselyov Arithmetic 可以扩展为支持负数,也支持 fractions/rational 数。我怀疑支持间隔也是可行的。 las,我不知道有任何库包含这些扩展。

关系算术的不同方法之间还有许多其他权衡,至少值得写一篇短文!不过,我希望这能给你一些想法。

干杯,

--威尔