阐明不同 minikanren 实现中的搜索算法 2.1 conde 和 condi 在 TRS12.2 conde in TRS22.3 conde in TRS1*第一个实验第二个实验第三个实验

问题描述

我目前正在通过 The Reasoned Schemer 和 Racket 学习迷你看人。

我有三个版本的 minikanren 实现：

The Reasoned Schemer，第一版（麻省理工学院出版社，2005 年）。我叫它TRS1

https://github.com/miniKanren/TheReasonedSchemer

附注。它表示 condi 已被执行交错的改进版 conde 取代。
The Reasoned Schemer，第二版（麻省理工学院出版社，2018 年）。我叫它TRS2

https://github.com/TheReasonedSchemer2ndEd/CodeFromTheReasonedSchemer2ndEd
The Reasoned Schemer，第一版（麻省理工学院出版社，2005 年）。我叫它TRS1*

https://docs.racket-lang.org/minikanren/

我对上述三种实现做了一些实验：

第一个实验：

TRS1

(run* (r)
      (fresh (x y)
             (conde
              ((== 'a x) (conde
                          ((== 'c y) )
                          ((== 'd y))))
              ((== 'b x) (conde
                          ((== 'e y) )
                          ((== 'f y)))))
             (== `(,x,y) r)))

;; => '((a c) (a d) (b e) (b f))

TRS2

(run* (x y)
      (conde
       ((== 'a x) (conde
                   ((== 'c y) )
                   ((== 'd y))))
       ((== 'b x) (conde
                   ((== 'e y) )
                   ((== 'f y))))))
;; => '((a c) (a d) (b e) (b f))

TRS1*

(run* (r)
      (fresh (x y)
             (conde
              ((== 'a x) (conde
                          ((== 'c y) )
                          ((== 'd y))))
              ((== 'b x) (conde
                          ((== 'e y) )
                          ((== 'f y)))))
             (== `(,y) r)))
;; => '((a c) (b e) (a d) (b f))

请注意，在第一个实验中，TRS1 和 TRS2 产生了相同的结果，但 TRS1* 产生了不同的结果。

似乎conde和TRS1中的TRS2使用相同的搜索算法，但TRS1*使用不同的算法。

第二个实验：

TRS1

(define listo
  (lambda (l)
    (conde
     ((nullo l) succeed)
     ((pairo l)
      (fresh (d)
             (cdro l d)
             (listo d)))
     (else fail))))

(define lolo
  (lambda (l)
    (conde
     ((nullo l) succeed)
     ((fresh (a) 
             (caro l a)
             (listo a))
      (fresh (d)
             (cdro l d)
             (lolo d)))
     (else fail))))
     
(run 5 (x)
     (lolo x))
;; => '(() (()) (() ()) (() () ()) (() () () ()))

TRS2

(defrel (listo l)
  (conde
   ((nullo l))
   ((fresh (d)
           (cdro l d)
           (listo d)))))

(defrel (lolo l)
  (conde
   ((nullo l))
   ((fresh (a)
           (caro l a)
           (listo a))
    (fresh (d)
           (cdro l d)
           (lolo d)))))

(run 5 x
     (lolo x))
;; => '(() (()) ((_0)) (() ()) ((_0 _1)))

TRS1*

(define listo
  (lambda (l)
    (conde
      ((nullo l) succeed)
      ((pairo l)
       (fresh (d)
         (cdro l d)
         (listo d)))
      (else fail))))

(define lolo
  (lambda (l)
    (conde
      ((nullo l) succeed)
      ((fresh (a) 
         (caro l a)
         (listo a))
       (fresh (d)
         (cdro l d)
         (lolo d)))
      (else fail))))

(run 5 (x)
     (lolo x))
;; => '(() (()) ((_.0)) (() ()) ((_.0 _.1)))

请注意，在第二个实验中，TRS2 和 TRS1* 产生了相同的结果，但 TRS1 产生了不同的结果。

似乎 TRS2 和 TRS1* 中的 conde 使用相同的搜索算法，但 TRS1 使用不同的算法。

这些让我很困惑。

有人可以帮我在上面的每个 minikanren 实现中澄清这些不同的搜索算法吗？

非常感谢。

---- 添加一个新的实验 ----

第三个实验：

TRS1

(define (tmp-rel y)
  (conde
   ((== 'c y) )
   ((tmp-rel-2 y))))

(define (tmp-rel-2 y)
  (== 'd y)
  (tmp-rel-2 y))

(run 1 (r)
      (fresh (x y)
             (conde
              ((== 'a x) (tmp-rel y)) 
              ((== 'b x) (conde
                          ((== 'e y) )
                          ((== 'f y)))))
             (== `(,y) r)))

;; => '((a c))

然而，run 2 或 run 3 循环。

如果我使用 condi 而不是 conde，那么 run 2 可以工作但 run 3 仍然循环。

TRS2

(defrel (tmp-rel y)
  (conde
   ((== 'c y) )
   ((tmp-rel-2 y))))

(defrel (tmp-rel-2 y)
  (== 'd y)
  (tmp-rel-2 y))

(run 3 r
      (fresh (x y)
             (conde
              ((== 'a x) (tmp-rel y))
              ((== 'b x) (conde
                          ((== 'e y) )
                          ((== 'f y)))))
             (== `(,y) r)))
             
;; => '((b e) (b f) (a c))

这没问题，只是顺序不符合预期。

注意 (a c) 现在是最后一个。

TR1*

(define (tmp-rel y)
  (conde
   ((== 'c y) )
   ((tmp-rel-2 y))))

;;
(define (tmp-rel-2 y)
  (== 'd y)
  (tmp-rel-2 y))

(run 2 (r)
      (fresh (x y)
             (conde
              ((== 'a x) (tmp-rel y))
              ((== 'b x) (conde
                          ((== 'e y) )
                          ((== 'f y)))))
             (== `(,y) r)))

;; => '((a c) (b e))

然而，run 3 循环。

解决方法

您在 TRS1 实现中的第一个实验，在 Prolog（“and”是 ,，“or”是 ;）和等效的符号逻辑符号（“and”是 { {1}}，“或”是 *），如同

ex1_TRS1( R ) := ( X=a,( Y=c ; Y=d ) ; X=b,( Y=e ; Y=f ) ),R=[X,Y] ;; Prolog == ( {X=a} * ({Y=c} + {Y=d}) + {X=b} * ({Y=e} + {Y=f}) ) * {R=[X,Y]} ;; Logic == ( ({X=a}*{Y=c} + {X=a}*{Y=d}) + ({X=b}*{Y=e} + {X=b}*{Y=f}) ) * {R=[X,Y]} ;; 1 ----( ( <A> + ) + ( <C> + <D> ) )------------ ----( <A> + + <C> + <D> )------------ == ( {X=a}*{Y=c} + {X=a}*{Y=d} + {X=b}*{Y=e} + {X=b}*{Y=f} ) * {R=[X,Y]} ;; 2 == {X=a}*{Y=c}*{R=[X,Y]} ;; Distribution + {X=a}*{Y=d}*{R=[X,Y]} + {X=b}*{Y=e}*{R=[X,Y]} + {X=b}*{Y=f}*{R=[X,Y]} == {X=a}*{Y=c}*{R=[a,c]} + {X=a}*{Y=d}*{R=[a,d]} ;; Reconciling + {X=b}*{Y=e}*{R=[b,e]} + {X=b}*{Y=f}*{R=[b,f]} ;; Reporting == {R=[a,c]} + {R=[a,d]} + {R=[b,e]} + {R=[b,f]} ;; => ((a c) (a d) (b e) (b f)) 操作必须执行一些验证，因此 *，即什么都没有，因为这两个分配彼此不一致。它还可以通过替换执行简化，从 {P=1}*{P=2} ==> {} 到 {X=a}*{Y=c}*{R=[X,Y]}。

显然，在此实现中，{X=a}*{Y=c}*{R=[a,c]}（如 ((<A> + ) + (<C> + <D>)) == (<A> + + <C> + <D>) --> ;; 1 步骤中所示）。显然它在 ;; 2 中是一样的：

TRS2

但是在 ex1_TRS2( [X,Y] ) := ( X=a,(Y=c ; Y=d) ; X=b,(Y=e ; Y=f) ). ;; => ((a c) (a d) (b e) (b f)) 中，结果的顺序是不同的，

TRS1*

所以它一定是ex1_TRS1_star( R ) := ( X=a,(Y=e ; Y=f) ),Y]. ;; => ((a c) (b e) (a d) (b f))。

直到排序，结果都是一样的。

书中没有搜索算法，只有解决方案流的混合算法。但由于流是惰性的，它实现了同样的目的。

您可以按照相同的方式完成其余部分，并在每个特定实现中发现 ((<A> + ) + (<C> + <D>)) == (<A> + <C> + + <D>) 的更多属性。

经过几天的研究，我想我已经能够回答这个问题了。

1.概念澄清

首先，我想澄清一些概念：

有两种众所周知的非确定性计算模型：流模型和双连续模型。大多数 miniKanren 实现使用流模型。

附注。术语“回溯”通常意味着深度优先搜索（DFS），它可以通过流模型或双连续模型进行建模。（所以当我说“xxx得到尝试”时，并不意味着底层实现必须使用两个延续模型。它可以通过流模型实现，例如minikanren。）

2.解释 `conde` 或 `condi`

的不同版本

2.1 `conde` 和 `condi` 在 `TRS1`

TRS1 为非确定性选择提供了两个目标构造函数，conde 和 condi。

conde 使用 DFS，由流的 MonadPlus 实现。

MonadPlus 的缺点是不公平。当第一个选择提供无限数量的结果时，永远不会尝试第二个选择。它使搜索不完整。

为了解决这个不完整的问题，TRS1引入了condi，它可以交错两个结果。

condi 的问题在于它不能很好地处理发散（我的意思是没有价值的死循环）。例如，如果第一个选择出现分歧，则第二个选择仍然无法尝试。

本书的第 6:30 和 6:31 帧描述了这种现象。在某些情况下你可以使用alli来救援，见Frame 6:32，但一般情况下它仍然不能覆盖所有分歧的情况，见Frame 6:39或以下情况：（PS。所有这些问题都可以TRS2 中不存在。）

(define (nevero)
  (all (nevero)))

(run 2 (q)
     (condi
      ((nevero))
      ((== #t q))
      ((== #f q))))
;; => divergence

实施细节：

在 TRS1 中，流是标准流，即惰性列表。

conde 由 mplus 实现：

(define mplus
  (lambda (a-inf f)
    (case-inf a-inf
              (f)
              ((a) (choice a f))
              ((a f0) (choice a (lambdaf@ () (mplus (f0) f)))))))

condi 由 mplusi 实现

:(define mplusi
  (lambda (a-inf f)
    (case-inf a-inf
              (f) 
              ((a) (choice a f))
              ((a f0) (choice a (lambdaf@ () (mplusi (f) f0)))))) ; interleaving

2.2 `conde` in `TRS2`

TRS2 删除了上述两个目标构造函数并提供了一个新的 conde 。

conde 与 condi 类似，但仅在第一个选项是由 defref 定义的关系的返回值时才交错。因此，如果您不使用 conde，它实际上更像是旧的 defref。

conde 也解决了上述 condi 的问题。

实施细节：

在 TRS2 中，流不是标准流。

正如书中所说

一个流要么是空列表，要么是一个 cdr 是一个流的对，要么是一个暂停。

悬浮是由 (lambda () body) 形成的函数，其中 (( lambda () body)) 是一个流。

所以在 TRS2 中，流并不是在每个元素上都是惰性的，而只是在暂停点上是惰性的。

最初只有一个地方可以创建暂停，即defref：

(define-syntax defrel
  (syntax-rules ()
    ((defrel (name x ...) g ...)
     (define (name x ...)
       (lambda (s)
         (lambda ()
           ((conj g ...) s)))))))

这是合理的，因为产生无限结果或发散的“唯一”方法是递归关系。这也意味着如果你用define而不是defrel来定义一个关系，你会遇到conde中TRS1同样的问题（对于有限深度是可以的-第一次搜索）。

请注意，我必须在“only”上加上引号，因为大多数时候我们将使用递归关系，但是您仍然可以通过混合使用 Scheme 的命名 let 来产生无限结果或发散，例如：

(run 10 q
     (let loop ()
       (conde
        ((== #f q))
        ((== #t q))
        ((loop)))))
;; => divergence

之所以出现分歧，是因为现在没有暂停。

我们可以通过手动包装悬架来解决这个问题：

(define-syntax Zzz
    (syntax-rules ()
        [(_ g) (λ (s) (λ () (g s)))]))

(run 10 q
     (let loop ()
       (Zzz (conde
             ((== #f q))
             ((== #t q))
             ((loop)))) ))
;; => '(#f #t #f #t #f #t #f #t #f #t)

conde 由 append-inf 实现：

(define (append-inf s-inf t-inf)
  (cond
    ((null? s-inf) t-inf)
    ((pair? s-inf) 
     (cons (car s-inf)
       (append-inf (cdr s-inf) t-inf)))
    (else (lambda () ; interleaving when s-inf is a suspension 
            (append-inf t-inf (s-inf))))))

2.3 `conde` in `TRS1*`

TRS1* 源自早期论文“From Variadic Functions to Variadic Relations A miniKanren Perspective”。作为 TRS2，TRS1* 还删除了两个旧的目标构造函数并提供了一个新的 conde。

conde 类似于 conde 中的 TRS2，但仅在第一个选项本身是 conde 时才交错。

conde 也解决了上述 condi 的问题。

请注意，defref 中没有 TRS1*。因此如果递归关系不是从conde开始，你会遇到condi中TRS1同样的问题。例如，

(define (nevero)
  (fresh (x)
         (nevero)))
          
(run 2 (q)
     (conde
      ((nevero))
      ((== #t q))
      ((== #f q))))
;; => divergence

我们可以通过手动包装 conde 来解决这个问题：

(define (nevero)
  (conde
   ((fresh (x)
          (nevero)))))

(run 2 (q)
     (conde
      ((nevero))
      ((== #t q))
      ((== #f q))
      ))
;; => '(#t #f)

实施细节：

在TRS1*中，流是标准流+暂停。

(define-syntax conde
  (syntax-rules ()
    ((_ (g0 g ...) (g1 g^ ...) ...)
     (lambdag@ (s)
               (inc ; suspension which represents a incomplete stream
                (mplus* 
                 (bind* (g0 s) g ...)
                 (bind* (g1 s) g^ ...) ...))))))

(define-syntax mplus*
  (syntax-rules ()
    ((_ e) e)
    ((_ e0 e ...) (mplus e0 (lambdaf@ () (mplus* e ...)))))) ; the 2nd arg of the mplus application must wrap a suspension,because multiple clauses of a conde are just syntactic sugar of nested conde with 2 goals.

这也意味着 loop 中不存在上面命名的 let TRS1* 问题。

conde 是由交错的 mplus 实现的：

(define mplus
   (lambda (a-inf f)
     (case-inf a-inf
        (f)
        ((a) (choice a f))
        ((a f^) (choice a (lambdaf@ () (mplus (f) f^)))) 
        ((f^) (inc (mplus (f) f^)))))) ; interleaving when a-inf is a suspension
                                       ; assuming f must be a suspension

请注意，虽然函数名为 mplus，但它不是合法的 MonadPlus，因为它不遵守 MonadPlus 定律。

3.在问题中解释这些实验。

现在我可以解释问题中的这些实验了。

第一个实验

TRS1 => '((a c) (a d) (b e) (b f)) ，因为 conde 中的 TRS1 是 DFS。

TRS2 => '((a c) (a d) (b e) (b f)) ，因为如果不涉及 conde，TRS2 中的 defref 是 DFS。

TRS1* => '((a c) (b e) (a d) (b f))，因为conde中的TRS1*是交错的（最外面的conde使两个最里面的conde交错） .

请注意，如果我们将 conde 中的 condi 替换为 TRS1，结果将与 TRS1* 相同。

第二个实验

TRS1 => '(() (()) (() ()) (() () ()) (() () () ())) ，因为 conde 中的 TRS1 是 DFS。 conde 中 listo 的第二个子句从未尝试过，因为当 (fresh (d) (cdro l d) (lolo d) 被 bind 修改为 conde 中 listo 的第一个子句时提供无限数量的结果。

TRS2 => '(() (()) ((_0)) (() ()) ((_0 _1))) ，因为现在可以尝试 conde 中 listo 的第二个子句。 listo 和 lolo 由 defrel 定义意味着它们可能会造成暂停。当 append-inf 这两个暂停时，每个都迈出一步，然后将控制权交给另一个。

TRS1* => '(() (()) ((_.0)) (() ()) ((_.0 _.1))，与 TRS2 相同，除了暂停是由 conde 创建的。

请注意，将 conde 中的 condi 替换为 TRS1 不会改变结果。如果您想获得与 TRS2 或 TRS1* 相同的结果，请将 alli 包裹在 conde 的第二个子句中。

第三个实验

请注意，正如@WillNess 在他对问题的评论中所说：

顺便说一句，我不知道你可以这样写 (define (tmp-rel-2 y) (== 'd y) (tmp-rel-2 y))，没有任何特殊的 minikanren 形式包含两个目标......

是的，关于 TRS1 和 TRS1* 的第三个实验有一个错误：

(define (tmp-rel-2 y) ; <--- wrong relation definition!
  (== 'd y)
  (tmp-rel-2 y))

与 TRS2 不同，TRS1 和 TRS1* 没有内置 defrel，因此 define 形式来自 Scheme，而不是 minikaren。

我们应该使用一个特殊的 minikanren 形式来包围这两个目标。

因此，

对于TRS1，我们应该将定义改为

(define (tmp-rel-2 y)
  (all (== 'd y)
       (tmp-rel-2 y)))

对于 TRS1*，没有 all 构造函数，但我们可以使用 (fresh (x) ...) 来解决它

(define (tmp-rel-2 y)
  (fresh (x)
         (== 'd y)
         (tmp-rel-2 y)))

我犯了这个错误，因为我之前不熟悉 minikanren。

但是，这个错误不会影响最终结果，下面对TRS1和TRS1*的解释既适用于错误的定义，也适用于正确的定义。

TRS1 => '((a c))，因为 conde 中的 TRS1 是 DFS。 tmp-rel 在 tmp-rel-2 处发散。

请注意，将 conde 替换为 condi 和 (run 2 ...)，我们将得到 '((a c) (b e))。这是因为 condi 可以交错。但是，它仍然无法打印第三个解 (b f)，因为 condi 不能很好地处理发散。

TRS2 => '((b e) (b f) (a c)) ，因为如果我们使用TRS2来定义关系，defrel可以归档完整的搜索。

请注意，最终结果是 '((b e) (b f) (a c)) 而不是 '((a c) (b e) (b f))，因为在 TRS2 中，暂停仅最初由 defrel 创建。如果我们期望 '((a c) (b e) (b f))，我们可以手动包装暂停：

(define-syntax Zzz
    (syntax-rules ()
        [(_ g) (λ (s) (λ () (g s)))]))
        
(run 3 r
     (fresh (x y)
            (conde
             ((== 'a x) (tmp-rel y))
             ((== 'b x) (Zzz (conde ; wrap a suspension by Zzz
                              ((== 'e y) )
                              ((== 'f y))))))
            (== `(,x,y) r)))

;; => '((a c) (b e) (b f))

TRS1* => '((a c) (b e))，因为在 TRS1* 中，暂停被包裹在 conde s 处。

注意它仍然无法打印第三个解决方案(b f)，因为tmp-rel-2没有被包裹在conde中，所以这里没有创建暂停。如果我们期望 '((a c) (b e) (b f))，我们可以手动包装暂停：

(define (tmp-rel-2 y)
  (conde ((== 'd y) (tmp-rel-2 y)))) ; wrap a suspension by conde

4.结论

总而言之，minikanren 不是一种语言，而是语言家族。每个 minikanren 实现都可能有自己的 hack。可能有一些极端情况在不同的实现中具有略有不同的行为。幸运的是，minikanren 很容易理解。遇到这些极端情况，我们可以通过阅读源码来解决。

5.参考资料

The Reasoned Schemer，第一版（麻省理工学院出版社，2005 年）
从可变参数函数到可变参数关系——一个迷你看人的视角
The Reasoned Schemer，第二版（麻省理工学院出版社，2018 年）
µKanren：关系编程的最小函数核心
回溯、交错和终止 Monad Transformers

logic-programming minikanren racket reasoned-schemer scheme scheme

阐明不同 minikanren 实现中的搜索算法 2.1 conde 和 condi 在 TRS12.2 conde in TRS22.3 conde in TRS1*第一个实验第二个实验第三个实验

问题描述

解决方法

1.概念澄清

2.解释 conde 或 condi

2.1 conde 和 condi 在 TRS1

2.2 conde in TRS2

2.3 conde in TRS1*

3.在问题中解释这些实验。

第一个实验

第二个实验

第三个实验

4.结论

5.参考资料

相关问答

2.解释 `conde` 或 `condi`

2.1 `conde` 和 `condi` 在 `TRS1`

2.2 `conde` in `TRS2`

2.3 `conde` in `TRS1*`