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

Question

我目前正在通过 The Reasoned Schemer 和 Racket 学习 miniKanren。
我有三个版本的 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)))))
             (== `(,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产生了不同的结果。
似乎在 TRS2 中的 conde和 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

您在 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>) .
直到排序，结果都是一样的。
书中没有搜索算法，只有解决方案流的混合算法。但由于流是惰性的，它实现了同样的目的。
您可以按照相同的方式浏览其余部分并发现 + 的更多属性。在每个特定的实现中。