scheme - MicroKanren - 术语是什么？

Question

在理解 MicroKanren DSL 的核心术语时遇到一点困难.第 4 节说:

Terms of the language are defined by the unify operator. Here, terms of the language consist of variables, objects deemed identical under eqv?, and pairs of the foregoing.

但他们从不描述“对”的实际意思。这些对是否应该表示两个子项的相等性，如下所示:

type 'a ukanren = KVar of int | KVal of 'a | KEq of 'a kanren * 'a kanren

所以像这样的术语:

(call/fresh (λ (a) (≡ a 7)))

生成一对 (≡ a 7)?

编辑:经过进一步思考，我不认为是这样。论文中提到“对”似乎要晚得多，对基本系统进行了扩展和改进，这意味着这些对在基本介绍的术语中没有任何意义。这是正确的吗？

Answer 1

在此上下文中，“pair”仅表示 cons 对，例如 (5 . 6) 或 (foo . #t)。两对之间的统一示例是:

(call/fresh
  (λ (a)
    (call/fresh
      (λ (b)
        (≡ (cons a b) (cons 5 6))))))

将 a 与 5 关联，将 b 与 6 关联。