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

Posted

技术标签:

【中文标题】阐明不同 minikanren 实现中的搜索算法【英文标题】:Clarify search algorithms in different minikanren implementation 【发布时间】:2021-07-08 20:44:34 【问题描述】:

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

我有三个版本的 minikanren 实现:

    理性的计划者,第一版(麻省理工学院出版社,2005 年)。我叫它TRS1

    https://github.com/miniKanren/TheReasonedSchemer

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

    理性的计划者,第二版(麻省理工学院出版社,2018 年)。我叫它TRS2

    https://github.com/TheReasonedSchemer2ndEd/CodeFromTheReasonedSchemer2ndEd

    理性的计划者,第一版(麻省理工学院出版社,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))

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

似乎TRS1TRS2 中的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)))

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

似乎TRS2TRS1* 中的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 2run 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 循环。

【问题讨论】:

看起来像是将结果流组合成一个结果流的各种方式的结果,例如可以看出here 以及从那里链接的答案。 顺便说一句,我不知道你可以这样写(define (tmp-rel-2 y) (== 'd y) (tmp-rel-2 y)),没有任何特殊的minikanren形式包含两个目标...... @WillNess 当我问这个问题时,我正在阅读 The Reasoned Schemer。我对第 3:24 帧的结果感到困惑。当时,这本书还没有解释回溯机制。 (此机制在第 6 章中解释。) @WillNess 所以我想我现在可以解释第 3:24 帧了,虽然我还没有读完整本书。原因(非正式地)是TR1发出一个值后,它会回到最近的回溯点。但是由于我还没有读完整本书,所以我现在无法对这个问题添加答案。 @WillNess 第一版。 【参考方案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 ==&gt; ,即什么都没有,因为这两个分配彼此不一致。它还可以通过替换进行简化,从X=a*Y=c*R=[X,Y] 变为X=a*Y=c*R=[a,c]

显然,在这个实现中,((&lt;A&gt; + &lt;B&gt;) + (&lt;C&gt; + &lt;D&gt;)) == (&lt;A&gt; + &lt;B&gt; + &lt;C&gt; + &lt;D&gt;)(如;; 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))

所以它一定是((&lt;A&gt; + &lt;B&gt;) + (&lt;C&gt; + &lt;D&gt;)) == (&lt;A&gt; + &lt;C&gt; + &lt;B&gt; + &lt;D&gt;)

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

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

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

【讨论】:

【参考方案2】:

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

1。概念澄清

首先,我想澄清一些概念:

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

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

2。解释condecondi的不同版本

2.1 condecondiTRS1

TRS1 为非确定性选择提供了两个目标构造函数,condecondi

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 中,流是标准流,即惰性列表。

condemplus 实现:

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

condimplusi 实现

:(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 condeTRS2

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

condecondi 类似,但仅当第一个替代项是由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来定义一个关系,你会遇到condeTRS1中同样的问题(有限深度优先搜索是可以的)。

请注意,我必须在“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)   

condeappend-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 condeTRS1*

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

condeTRS2 中的 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。从未尝试过 listoconde 的第二个子句,因为当 (fresh (d) (cdro l d) (lolo d)binded 到 listoconde 的第一个子句时,它会提供无限数量的结果。

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

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

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

第三次实验

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

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

是的,关于TRS1TRS1*的第三个实验有一个错误:

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

不同于TRS2TRS1TRS1*没有内置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)))

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

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

TRS1 => '((a c)),因为TRS1 中的conde 是DFS。 tmp-reltmp-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。参考文献

    理性的计划者,第一版(麻省理工学院出版社,2005 年)

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

    理性的计划者,第二版(麻省理工学院出版社,2018 年)

    µKanren:关系编程的最小功能核心

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

【讨论】:

以上是关于阐明不同 minikanren 实现中的搜索算法的主要内容,如果未能解决你的问题,请参考以下文章

图 DB 与 Prolog(或 miniKanren)

为啥 miniKanren 中的“disj”在 Scheme 中有效,而在 Racket 中无效?

Prolog 匹配 vs miniKanren 统一

网站ALT标签的规范与技巧

算法专家解读 | 开放搜索教育搜题能力和实践

CSDN搜索可以搜博客代码了