阐明不同 minikanren 实现中的搜索算法

Question

我目前正在通过 The Reasoned Schemer 和 Racket 学习 miniKanren。

我有三个版本的 minikanren 实现：

1. 理性的计划者，第一版（麻省理工学院出版社，2005 年）。我叫它TRS1

   https://github.com/miniKanren/TheReasonedSchemer

   附言。它说condi 已被conde 的改进版本取代，它执行交织。

2. 理性的计划者，第二版（麻省理工学院出版社，2018 年）。我叫它TRS2

   https://github.com/TheReasonedSchemer2ndEd/CodeFromTheReasonedSchemer2ndEd

3. 理性的计划者，第一版（麻省理工学院出版社，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)))))
             (== `(,x ,y) r)))
;; => '((a c) (b e) (a d) (b f))

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

似乎TRS1 和TRS2 中的conde 使用相同的搜索算法，但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)))))
             (== `(,x ,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)))))
             (== `(,x ,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)))))
             (== `(,x ,y) r)))

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

但是，run 3 循环。

Answer 1

您在TRS1 实现中的第一个实验，在 Prolog（“and” 是 ,，“or” 是 ;）和等效的符号逻辑表示法（“and” 是 *，“or”是+)，就好像

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>     +     <B>    ) + (    <C>     +     <D>    ) )------------
 ----(      <A>     +     <B>      +      <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> + <B>) + (<C> + <D>)) == (<A> + <B> + <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=c ; Y=d)  ;  X=b, (Y=e ; Y=f) ), R=[X,Y].
;; => ((a c) (b e) (a d) (b f))

所以它一定是((<A> + <B>) + (<C> + <D>)) == (<A> + <C> + <B> + <D>)。

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

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

您可以以相同的方式完成其余部分，并在每个特定实现中发现+ 的更多属性。

Answer 2

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

1。概念澄清

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

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

PS。术语“回溯”通常是指深度优先搜索（DFS），可以通过流模型或双连续模型来建模。 （所以我说“xxx 试试”，并不是说底层实现一定要使用二续模型，可以用流模型实现，比如minikanren。）

2。解释conde或condi的不同版本

2.1 conde 和 condi 在 TRS1

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

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

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

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

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

本书的 6:30 和 6:31 描述了这种现象。在某些情况下你可以使用alli进行救援，见6:32，但总的来说还是不能涵盖所有的分歧情况，见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 在TRS2

TRS2 去掉了上面两个目标构造函数，提供了一个新的conde。

conde 与condi 类似，但仅当第一个替代项是由defref 定义的关系的返回值时才交错。所以如果你不使用defref，它实际上更像是旧的conde。

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”上加上引号，因为大多数时候我们将使用递归关系，但是您仍然可以通过混合名为 let 的 Scheme 来产生无限的结果或发散，例如：

(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 在TRS1*

TRS1*源于早期论文《From Variadic Functions to Variadic Relations A miniKanren Perspective》。和TRS2一样，TRS1*也去掉了两个旧的目标构造函数，提供了一个新的conde。

conde 与 TRS2 中的 conde 类似，但仅在第一个备选方案本身为 conde 时才交错。

conde也修复了condi上面的问题。

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

(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.

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

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)) ，因为TRS1 中的conde 是DFS。

TRS2 => '((a c) (a d) (b e) (b f)) ，因为TRS2 中的conde 是DFS，如果没有defref 参与。

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

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

第二次实验

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

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

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

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

第三次实验

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

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

是的，关于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)))

我犯这个错误是因为我以前不熟悉迷你看人。

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

TRS1 => '((a c))，因为TRS1 中的conde 是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)) ，因为如果我们使用defrel定义关系，TRS2可以归档完整的搜索。

请注意，最终结果是'((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*，暂停被包裹在condes。

请注意，它仍然无法打印第三个解决方案(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。参考文献

1. 理性的计划者，第一版（麻省理工学院出版社，2005 年）

2. 从可变参数函数到可变参数关系 - 迷你看人视角

3. 理性的计划者，第二版（麻省理工学院出版社，2018 年）

4. µKanren：关系编程的最小功能核心

5. 回溯、交错和终止 Monad 转换器