阐明不同 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))
请注意,在第一个实验中,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
循环。
【问题讨论】:
看起来像是将结果流组合成一个结果流的各种方式的结果,例如可以看出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 ==>
,即什么都没有,因为这两个分配彼此不一致。它还可以通过替换进行简化,从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>)
。
直到排序,结果都是一样的。
书中没有搜索算法,只有解决方案流的混合算法。但是由于流是惰性的,所以它实现了同样的目标。
您可以以相同的方式完成其余部分,并在每个特定实现中发现+
的更多属性。
【讨论】:
【参考方案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
使得最里面的两个conde
s交错)。
请注意,如果我们在TRS1
中将conde
替换为condi
,结果将与TRS1*
相同。
第二次实验
TRS1
=> '(() (()) (() ()) (() () ()) (() () () ()))
,因为TRS1
中的conde
是DFS。从未尝试过 listo
中 conde
的第二个子句,因为当 (fresh (d) (cdro l d) (lolo d)
是 bind
ed 到 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*
,暂停被包裹在conde
s。
请注意,它仍然无法打印第三个解决方案(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 实现中的搜索算法的主要内容,如果未能解决你的问题,请参考以下文章