在理解自定义 core.logic 约束时需要澄清

Need clarification in understanding a custom core.logic constraint

我试图理解如下定义的自定义 core.logic 约束,

(defne lefto
  "x appears to the left of y in collection l."
  [x y l]
  ([_ _ [x . tail]] (membero y tail))
  ([_ _ [_ . tail]] (lefto x y tail)))

如何在 core.logic 的上下文中解释 _.

defne 是一个使用特殊模式匹配语法的宏,但其行为类似于 conde。 (仅供参考,其中每个中的 e 代表 "everything" 即每个子句都可以贡献。)

  • _ 下划线表示必须存在的值,但您不关心它是什么。
  • . 表示 . 左侧的项目和 . 右侧的列表尾部的串联。这用于将列表的单个项目和列表的其余部分绑定到不同的值。 (另见 core.logic 中的 llist。)

Clojure 中类似的序列解构将使用 & 而不是 .:

(let [[_ _ [_ & tail]] coll] ...)

所以下面的模式意味着"we don't care about the first or second input argument, but the third should be a list where we the head is x (i.e. equal to the function's x input argument) and bind the tail to tail":

[_ _ [x . tail]]

还要注意这里tail可以是空列表,在.前可以绑定多个值。

由于您的示例是一个递归目标,它最终将通过在 y 之前找到 x 来终止,或者它将无法匹配任一模式,因为 l 将(最终)是空列表 (),它不会匹配任何一种情况。

更简单的示例

membero 定义本身是同一思想的一个更​​简单的例子:

(defne membero
  "A relation where l is a collection, such that l contains x."
  [x l]
  ([_ [x . tail]])
  ([_ [head . tail]]
    (membero x tail)))

有两个子句,每个子句由一个 top-level 列表表示 ():

  1. [_ [x . tail]] - 第一个 _ 表示我们不关心 匹配 的输入 x arg。 [x . tail] 描述了第二个参数 l 的模式,如果 xl 的头部,那么这个模式匹配并且 membero 成功。
  2. [_ [head . tail] - _ 在这里表示相同的意思。但是请注意,我们已经为 l 的头部赋予了一个新名称,它只需要是一个 non-empty 列表即可满足此模式。如果匹配,则我们递归 (membero x tail) 继续搜索。

只有第一个子句才能使目标成功,方法是在 l 的(子)列表中找到 x;第二个子句仅用于解构 lheadtail 并递归。

这里的 membero 翻译成 conde,没有模式匹配:

(defn memberoo [x l]
  (conde
    [(fresh [a d]
       (conso a d l)
       (== a x))]
    [(fresh [a d]
       (conso a d l)
       (memberoo x d))]))