cha*_*sey 6 scheme logic-programming racket minikanren reasoned-schemer
我目前正在学习 The Reasoned Schemer 和 Racket 的 miniKanren。
我有三个版本的 minikanren 实现：
《理性策划者》，第一版（麻省理工学院出版社，2005 年）。我叫它TRS1
https://github.com/miniKanren/TheReasonedSchemer
附言。它说它已被执行交错的condi改进版本所取代。conde
《理性的阴谋家》，第二版（麻省理工学院出版社，2018 年）。我叫它TRS2
https://github.com/TheReasonedSchemer2ndEd/CodeFromTheReasonedSchemer2ndEd
《理性策划者》，第一版（麻省理工学院出版社，2005 年）。我叫它TRS1*
我对上面的三种实现做了一些实验：
第一个实验：
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*产生了不同的结果。
看来condeinTRS1和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中TRS2和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, thenrun 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循环。
经过几天的研究，我想我已经能够回答这个问题了。
\n首先，我想澄清一些概念：
\n有两种著名的非确定性计算模型：流模型和双连续模型。大多数 miniKanren 实现都使用流模型。
\n附言。术语“回溯”通常意味着深度优先搜索（DFS），其可以通过流模型或两个连续模型来建模。（所以当我说“xxx get attempts”时，并不意味着底层实现必须使用两次延续模型。它可以通过流模型来实现，例如minikanren。）
\nconde2. 解释或的不同版本condiconde及condi中TRS1TRS1为非确定性选择提供两个目标构造函数，conde并且condi.
conde使用DFS，由流的MonadPlus实现。
MonadPlus 的缺点是不公平。当第一个替代方案提供无限数量的结果时，永远不会尝试第二个替代方案。它使搜索不完整。
\n为了解决这个不完全问题，TRS1引入了condi可以将两个结果交错的方法。
的问题condi是它不能很好地处理分歧（我的意思是没有价值的死循环）。例如，如果第一种选择出现分歧，则仍然无法尝试第二种选择。
书中第 6:30 和 6:31 帧描述了这种现象。在某些情况下你可以使用allirescue，参见第6:32帧，但一般来说它仍然不能覆盖所有发散的情况，参见第6:39帧或下面的情况：（PS.所有这些问题都不存在TRS2。）
(define (nevero)\n (all (nevero)))\n\n(run 2 (q)\n (condi\n ((nevero))\n ((== #t q))\n ((== #f q))))\n;; => divergence\n实施细节：
\n在 中TRS1，流是标准流，即惰性列表。
其conde实施方式是mplus：
(define (nevero)\n (all (nevero)))\n\n(run 2 (q)\n (condi\n ((nevero))\n ((== #t q))\n ((== #f q))))\n;; => divergence\n其condi实现方式是mplusi
(define mplus\n (lambda (a-inf f)\n (case-inf a-inf\n (f)\n ((a) (choice a f))\n ((a f0) (choice a (lambdaf@ () (mplus (f0) f)))))))\nconde英寸TRS2TRS2删除了上述两个目标构造函数并提供了一个新的conde.
与conde类似condi，但仅当第一个替代项是由 定义的关系的返回值时才进行交错defref。因此，conde如果您不使用defref.
还conde解决了上述问题condi。
实施细节：
\n在 中TRS2，流不是标准流。
正如书上所说
\n\n\n流要么是空列表，要么是 cdr 是流的对，要么是暂停。
\n悬挂是由 (lambda () body) 形成的函数，其中 (( lambda () body)) 是流。
\n
所以在 中TRS2，流并不是在每个元素上都是惰性的，而只是在暂停点上是惰性的。
只有一个地方可以最初创建暂停，即defref：
:(define mplusi\n (lambda (a-inf f)\n (case-inf a-inf\n (f) \n ((a) (choice a f))\n ((a f0) (choice a (lambdaf@ () (mplusi (f) f0)))))) ; interleaving \n这是合理的，因为产生无限结果或发散的“唯一”方式是递归关系。这也意味着，如果你使用define而不是defrel定义一个关系，你会遇到同样的问题condein TRS1（对于有限深度优先搜索来说是可以的）。
请注意，我必须在“only”上加上引号，因为大多数时候我们将使用递归关系，但是您仍然可以通过混合Scheme\'snamed来产生无限结果或发散let，例如：
(define-syntax defrel\n (syntax-rules ()\n ((defrel (name x ...) g ...)\n (define (name x ...)\n (lambda (s)\n (lambda ()\n ((conj g ...) s)))))))\n由于现在没有暂停，所以出现了分歧。
\n我们可以通过手动包裹悬架来解决这个问题：
\n(run 10 q\n (let loop ()\n (conde\n ((== #f q))\n ((== #t q))\n ((loop)))))\n;; => divergence\n其conde实施方式是append-inf：
(define-syntax Zzz\n (syntax-rules ()\n [(_ g) (\xce\xbb (s) (\xce\xbb () (g s)))]))\n\n(run 10 q\n (let loop ()\n (Zzz (conde\n ((== #f q))\n ((== #t q))\n ((loop)))) ))\n;; => \'(#f #t #f #t #f #t #f #t #f #t) \nconde英寸TRS1*TRS1*源于早期论文《From Variadic Functions to Variadic Relations A miniKanren Perspective》。作为TRS2，TRS1*还删除了两个旧的目标构造函数并提供了一个新的conde。
与inconde类似，但仅当第一个替代项本身是 a 时才交错。condeTRS2conde
还conde解决了上述问题condi。
defref请注意，中没有TRS1*。因此，如果递归关系不是从 from 开始，您将遇到inconde的相同问题。例如，condiTRS1
(define (append-inf s-inf t-inf)\n (cond\n ((null? s-inf) t-inf)\n ((pair? s-inf) \n (cons (car s-inf)\n (append-inf (cdr s-inf) t-inf)))\n (else (lambda () ; interleaving when s-inf is a suspension \n (append-inf t-inf (s-inf))))))\n我们可以通过手动包装来解决这个问题conde：
(define (nevero)\n (fresh (x)\n (nevero)))\n \n(run 2 (q)\n (conde\n ((nevero))\n ((== #t q))\n ((== #f q))))\n;; => divergence\n实施细节：
\n中TRS1*，流为标准流+悬浮。
(define (nevero)\n (conde\n ((fresh (x)\n (nevero)))))\n\n(run 2 (q)\n (conde\n ((nevero))\n ((== #t q))\n ((== #f q))\n ))\n;; => \'(#t #f)\n这也意味着上面的命名letloop问题在TRS1*.
这conde是通过交错实现的mplus：
(define-syntax conde\n (syntax-rules ()\n ((_ (g0 g ...) (g1 g^ ...) ...)\n (lambdag@ (s)\n (inc ; suspension which represents a incomplete stream\n (mplus* \n (bind* (g0 s) g ...)\n (bind* (g1 s) g^ ...) ...))))))\n\n(define-syntax mplus*\n (syntax-rules ()\n ((_ e) e)\n ((_ 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.\n请注意，虽然该函数名为mplus，但它不是合法的 MonadPlus，因为它不遵守 MonadPlus 法则。
现在我可以在问题中解释这些实验了。
\nTRS1 => \'((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使两个最里面的condes 交错）。
请注意，如果我们替换conde为condiin TRS1，结果将与 相同TRS1*。
TRS1 => \'(() (()) (() ()) (() () ()) (() () () ())) ，因为condeinTRS1是 DFS。condein的第二个子句listo从未被尝试过，因为当(fresh (d) (cdro l d) (lolo d)ed到inbind的第一个子句时，它提供了无限数量的结果。condelisto
TRS2=> ，因为现在可以尝试 in\'(() (()) ((_0)) (() ()) ((_0 _1))) 的第二个子句。并被定义为它们可能会造成暂停。当这两种暂停时，各自迈出一步，然后将控制权让给对方。condelistolistololodefrelappend-inf
TRS1*=> \'(() (()) ((_.0)) (() ()) ((_.0 _.1)), 与 相同TRS2，只是暂停是由 产生的conde。
请注意，替换conde为condiinTRS1不会改变结果。如果您想获得与TRS2or相同的结果TRS1*，请alli在 的第二个子句处换行conde。
请注意，正如 @WillNess 在他对问题的评论中所说：
\n\n\n顺便说一句，我不知道你可以
\n(define (tmp-rel-2 y) (== \'d y) (tmp-rel-2 y))这样写，没有任何特殊的迷你看联形式包含两个目标......
是的，第三个实验TRS1有TRS1*一个错误：
(define mplus\n (lambda (a-inf f)\n (case-inf a-inf\n (f)\n ((a) (choice a f))\n ((a f^) (choice a (lambdaf@ () (mplus (f) f^)))) \n ((f^) (inc (mplus (f) f^)))))) ; interleaving when a-inf is a suspension\n ; assuming f must be a suspension\n与 ,不同TRS2，TRS1并且TRS1*没有内置defrel，因此该define形式来自Scheme，而不是minikaren。
我们应该使用一种特殊的迷你看联形式来包含这两个目标。
\n所以，
\n对于TRS1，我们应该将定义更改为
(define (tmp-rel-2 y) ; <--- wrong relation definition!\n (== \'d y)\n (tmp-rel-2 y))\n对于TRS1*，没有all构造函数，但我们可以使用(fresh (x) ...)它来解决它
(define (tmp-rel-2 y)\n (all (== \'d y)\n (tmp-rel-2 y)))\n我犯这个错误是因为我之前对minikanren不熟悉。
\n不过，这个错误不会影响最终的结果，下面对 和 的解释TRS1既TRS1*适用于错误的定义，也适用于正确的定义。
TRS1 => \'((a c))，因为condeinTRS1是 DFS。发散tmp-rel于tmp-rel-2。
注意，conde用condiand替换(run 2 ...)，我们会得到 \'((a c) (b e)). 这是因为condi可以交织。但是，它仍然无法打印第三个解决方案(b f)，因为condican\xe2\x80\x99t 可以很好地处理发散。
TRS2 => \'((b e) (b f) (a c)) ，因为如果我们使用定义关系TRS2可以归档完整的搜索。defrel
请注意，最终结果不是\'((b e) (b f) (a c))因为\'((a c) (b e) (b f))在 中TRS2，暂停最初是由 产生的defrel。如果我们期望的话\'((a c) (b e) (b f))，我们可以手动包裹悬架：
(define (tmp-rel-2 y)\n (fresh (x)\n (== \'d y)\n (tmp-rel-2 y)))\nTRS1*=> \'((a c) (b e))，因为在 中TRS1*，悬浮液被包裹在condes 处。
请注意，它仍然无法打印第三个解决方案(b f)，因为tmp-rel-2它没有被包裹在 中conde，因此这里没有创建暂停。如果我们期望的话\'((a c) (b e) (b f))，我们可以手动包裹悬架：
(define-syntax Zzz\n (syntax-rules ()\n [(_ g) (\xce\xbb (s) (\xce\xbb () (g s)))]))\n \n(run 3 r\n (fresh (x y)\n (conde\n ((== \'a x) (tmp-rel y))\n ((== \'b x) (Zzz (conde ; wrap a suspension by Zzz\n ((== \'e y) )\n ((== \'f y))))))\n (== `(,x ,y) r)))\n\n;; => \'((a c) (b e) (b f)) \n总而言之，迷你看联不是一种语言，而是语言家族。每个 minikanren 实现都可能有自己的 hack。可能存在一些极端情况，在不同的实现中其行为略有不同。幸运的是，minikanren 很容易理解。当遇到这些极端情况时，我们可以通过阅读源码来解决。
\n《理性的阴谋家》，第一版（麻省理工学院出版社，2005 年）
\n从可变参数函数到可变参数关系 - miniKanren 视角
\n《理性的阴谋家》，第二版（麻省理工学院出版社，2018 年）
\n\xc2\xb5Kanren：关系编程的最小功能核心
\n回溯、交错和终止 Monad 变压器
\n| 归档时间： |
|
| 查看次数： |
319 次 |
| 最近记录： |