在理解自定义 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 代表 "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 列表表示 ():

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

只有第一个子句才能使目标成功，方法是在 l 的（子）列表中找到 x；第二个子句仅用于解构 l 的 head 和 tail 并递归。

这里的 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))]))

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

Need clarification in understanding a custom core.logic constraint

clojure

clojure-core.logic

functional-logic-progr

更简单的示例