小贝子编程

阐明不同迷你坎人实现中的搜索算法



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

我有三个版本的迷你坎人实现：

  1. The Reasoned Schemer，第一版(麻省理工学院出版社，2005年)。我称之为TRS1

    https://github.com/miniKanren/TheReasonedSchemer

    附言。它说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*产生了不同的结果。

似乎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使用不同的算法。

这些让我非常困惑。

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

非常感谢。

----添加新的实验

----第三个实验：

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循环。

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

1. 概念澄清

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

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

附言。术语"回溯"通常意味着深度优先搜索 (DFS)，可以通过流模型或双延续模型进行建模。(因此，当我说"xxx get tryed"时，这并不意味着底层实现必须使用双延续模型。它可以通过流模型实现，例如迷你坎人。

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

2.1TRS1conde和condi

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

conde使用DFS，DFS由流的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.2TRS2conde

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

conde类似于condi，但只有当第一个备选方案是由defref定义的关系的返回值时才交错。所以如果你不使用defref，它实际上更像是旧的conde.

该conde还修复了上述condi问题。

实施细节：

在TRS2中，流不是标准流。

正如书中所说

流可以是空列表、其 cdr 是流的对或挂起。

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

所以在TRS2中，流并不是在每个元素上都懒惰，而只是在悬挂点上懒惰。

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

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

这是合理的，因为产生无限结果或发散的"唯一"方法是递归关系。这也意味着，如果使用define而不是defrel来定义关系，则会遇到相同的TRS1conde问题(有限深度优先搜索是可以的)。

请注意，我不得不在"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.3TRS1*conde

TRS1*起源于早期的论文"从可变参数函数到可变参数关系的迷你Kanren视角"。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.

这也意味着上面命名的让loop问题在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))，因为TRS1中的conde是DFS。

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

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

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

第二次实验

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

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

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

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

第三次实验

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

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

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

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

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

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

因此

对于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*中，悬浮液被包裹在conde秒。

请注意，它仍然无法打印第三个解决方案(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. The Reasoned Schemer，第一版(麻省理工学院出版社，2005年)

    2. 从可变参数

  2. 函数到可变参数关系 - 迷你Kanren视角

  3. The Reasoned Schemer，第二版(麻省理工学院出版社，2018

    )

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

  5. 回溯、交错和端接单元变压器

你在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>).

直到订购，结果是相同的。

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

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

相关内容

最新更新


热门标签：

javascript python java c# php android html jquery c++ css ios sql mysql arrays asp.net json python-3.x ruby-on-rails .net sql-server django objective-c excel regex ruby linux ajax iphone xml vba spring asp.net-mvc database wordpress string postgresql wpf windows xcode bash git oracle list vb.net multithreading eclipse algorithm macos powershell visual-studio image forms numpy scala function api selenium