在minikanren中编写向量成员

Question

我正在尝试为miniKanren (1)编写一个处理向量的membero等价物。到目前为止，我找不到一种不需要观察值是逻辑变量还是部分实例化的方法。有什么建议吗？

目前，我有：

(defun rangeo (x n)
  (when (mu-var-p n)
    (error "rangeo must be called with a fully instantiated second argument"))
  (if (<= n 0)
    +fail+
    (conde
      ((== x (1- n)))
      ((rangeo x (1- n))))))

(defun vmembero (x v)
  (when (mu-var-p v)
    (error "vmembero must be called with a partially instantiated second argument"))
  (fresh (i)
    (rangeo i (length v))
    (project (i)
      (== x (aref v i)))))

(1)：这无关紧要，但我实际上使用的是cl-kanren；我认为这里的任何东西都不应该依赖于它。cl-kanren的特点是向量的统一。

Answer 1

要实现此下拉，请返回到方案。你不能在纯minikanren中实现它。

此外，您不应该将过程应用程序嵌套在表达式中，如(== x (1- n))和(rangeo i (length v))。尽量使用纯逻辑谓词或纯模式谓词。

Answer 2

您可能想要扩展我们的统一算法，以透明地统一向量。您可能会发现，您会希望完全转换术语的表示形式。