MiniKanren 有“非”运算符吗？

Posted 2023-05-08

【中文标题】MiniKanren 有“非”运算符吗？

【英文标题】：Does MiniKanren have the "not" operator?

【发布时间】：2018-01-20 12:12:38

【问题描述】：

MiniKanren 有“not”运算符吗？

例如，如何表示 Prolog 的

a :- b, not(c)

如果b 为真而c 不为真，则

a 为真（Prolog 使用否定作为失败，ie 如果c 无法被证明，则not(c) 被视为已证明）

Prolog 的 not 也适用于非地面表达式，例如

a(X, d(Y)) :- b(d(X), d(Y)), not(c(d(X)))

【参考方案1】：

根据https://github.com/zhjhxxxjh/ykanren，答案是否定的。

【讨论】：

core.logic 仍然允许negation as failure。

@AndersonGreen 这完全等同于 Prolog 的 not 吗？ （见编辑）

【参考方案2】：

minikanren 中没有not 运算符，但你可以使用conda 实现类似的效果：

(defmacro not
  "fail if the given goal succeeds, use with extreme caution"
  [goal]
  `(conda 
     [~goal fail]
     [succeed]))

见my similar question on Google Groups

【讨论】：

我是否正确理解这与 Prolog 的不同？ （见编辑）

@MaxB 我认为这与 Prolog 的不一样，因为它们都成功当且仅当他们的论点在那个特定时刻无法被证明。但是，我是逻辑编程的新手，求反很棘手，所以如果我错了，我不会感到惊讶。

据我了解，miniKanren 中的这个构造无法处理变量，如第二个示例所示。

那么 Minikanren 建议如何处理通常用否定来恰当表达的问题呢？在我看来，否定是逻辑中的一项基本操作，缺少它的逻辑语言（以一种或另一种形式）具有严重的局限性。对此问题有何建议/见解？

在逻辑编程中为否定提供完整的通用、适当的语义是恕我直言的棘手业务。我会向您指出 Shepherdson 或 Apt 以获得该地区最近（-ish）的良好调查。简而言之，您可能会发现 Prolog 的 not 的某些行为并不完全令人满意。我们已经下注了。在您可能遇到的实现中，您会发现否定的等式约束和可能的否定子项约束。与一般的关系不同，这些约束需要是原子操作并保证终止。更多信息，如果你喜欢：hdl.handle.net/2022/25183