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

Question

我试图理解如下定义的自定义 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的上下文中解释_和.？

Answer 1

defne 是一个使用特殊模式匹配语法的宏，但其行为类似于 conde。 (仅供引用，其中每一个中的 e 都代表“一切”，即每个子句都可以做出贡献。)

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

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

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

所以下面的模式意味着“我们不关心第一个或第二个输入参数，但第三个应该是一个列表，其中我们的头部是x(即等于函数的x 输入参数)并将尾部绑定(bind)到 tail":

[_ _ [x . tail]]

另请注意，此处tail可以为空列表，您可以在.前绑定(bind)多个值。

由于您的示例是一个递归目标，它最终将通过在 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)))

有两个子句，每个子句由一个顶级列表()表示:

1. [_ [x . tail]] - 第一个 _ 代表我们不关心匹配的输入 x arg。 [x 。 tail] 描述了第二个参数 l 的模式，如果 x 是 l 的头部，那么这个模式匹配和 membero 成功。
2. [_ [头。 tail] - _ 在这里意味着同样的事情。但是请注意，我们已经为 l 的头部赋予了一个新名称，它只需要是一个非空列表即可满足此模式。如果匹配，则我们使用 (membero x tail) 进行递归以继续搜索。

只有第一个子句可以通过在 l 的(子)列表中找到 x 来使目标成功；第二个子句只用于解构l的head和tail并递归。

这是用 conde 翻译的 membero，没有模式匹配:

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