3

理解MicroKanren DSL的核心术语有点困难。第 4 节说：

语言的术语由unify操作员定义。在这里，语言的术语由变量、在 下被视为相同的对象eqv?以及上述内容的对组成。

但他们从不描述“对”的实际含义。对是否应该表示两个子项的相等性，如下所示：

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

所以像这样的术语：

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

生成一对(≡ a 7)?

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

4

2 回答 2

3

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

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

a与 5 和6相关联b。

于 2015-03-06T12:47:04.173 回答
1
  1. 很抱歉给您带来困惑和困难！！谢谢你的问题！

您可以将（典型的）Kanren 术语语言视为具有单个二进制函子标记cons/2和无限数量的常数（确切的构成从嵌入到嵌入发生变化）。

假设cons/2是唯一的 (n < 0) 元函子标记，则每个复合项都将使用它构建。如果您查看统一的标准表示形式（例如 Martelli-Montanari），您通常会看到一个 step f(t0,...,tn) g(s0,...,sm) => fail if f =/= g or n =/= m。在比较基本原子术语时，我们处理统一中的冲突失败；对我们来说，复合词必须具有相同的数量和标签。

pair?承认conses。实际上，在 Racket 中，它们提供了一个cons?别名，以使这一点更清晰！

再次感谢您！

于 2020-07-20T13:35:14.530 回答