scheme - 在 minikanren 中编写 vector-membero

Question

我正在尝试为membero适用于向量的 miniKanren (1) 编写等价物。到目前为止，我找不到不涉及观察值是逻辑变量还是部分实例化的方法。任何指针？

目前，我有：

(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

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

Answer 2

要实现此下拉回方案。您将无法在纯 minikanren 中实现它。

此外，您不应该在表达式中嵌套过程应用程序，例如(== x (1- n))and (rangeo i (length v))。尝试坚持纯逻辑谓词或纯方案谓词。