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

Question

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

我有三个版本的 minikanren 实现：

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

   https://github.com/miniKanren/TheReasonedSchemer

   PS。它说它condi已被conde执行交织的改进版本所取代。

2. The Reasoned Schemer，第二版（麻省理工学院出版社，2018 年）。我叫它TRS2

   https://github.com/TheReasonedSchemer2ndEd/CodeFromTheReasonedSchemer2ndEd

3. 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)))))
             (== `(,x ,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产生了不同的结果。

似乎conde inTRS2和TRS1*使用相同的搜索算法，但是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

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

1. 概念澄清

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

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

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

2. 解释condeor的不同版本condi

2.1conde及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.2conde英寸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 的 named 来产生无限的结果或发散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.3conde英寸TRS1*

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

类似in ，但仅当conde第一个选择本身是 a 时才交错。condeTRS2conde

也解决了上述conde问题condi。

请注意，没有defrefin TRS1*。因此，如果递归关系不是从开始的conde，您将遇到与condiin相同的问题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)) ，因为condeinTRS1是 DFS。

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

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

请注意，如果我们conde用condiin替换TRS1，结果将与 相同TRS1*。

第二次实验

TRS1 => '(() (()) (() ()) (() () ()) (() () () ())) ，因为condeinTRS1是 DFS。condein的第二个子句listo从未尝试过，因为 when(fresh (d) (cdro l d) (lolo d)被bind添加到 in 的第一个子句，conde它listo提供了无限数量的结果。

TRS2=> '(() (()) ((_0)) (() ()) ((_0 _1))) ，因为现在可以尝试 condein的第二个子句。并且被定义为他们可能会导致暂停。当这两个暂停时，每个都采取一个步骤，然后将控制权交给另一个。listolistololodefrelappend-inf

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

请注意，替换conde为condiinTRS1不会改变结果。如果您想获得与TRS2or相同的结果，请在 的第二个子句处TRS1*换行。alliconde

第三次实验

请注意，正如@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))，因为condeinTRS1是 DFS。tmp-rel分歧tmp-rel-2于。

请注意，用 and 替换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))因为 in 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))，因为 in 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 Transformers

Answer 2

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

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>)。

直到ordering，结果都是一样的。

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

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