阐明不同 minikanren 实现中的搜索算法
Clarify search algorithms in different minikanren implementation
我目前正在通过 The Reasoned Schemer 和 Racket 学习 miniKanren。
我有三个版本的 minikanren 实现：
The Reasoned Schemer，第一版（麻省理工学院出版社，2005 年）。我叫它 TRS1
https://github.com/miniKanren/TheReasonedSchemer
PS。它说 condi 已被 conde 的改进版本取代，后者执行交错。
The Reasoned Schemer，第二版（麻省理工学院出版社，2018 年）。我叫它 TRS2
https://github.com/TheReasonedSchemer2ndEd/CodeFromTheReasonedSchemer2ndEd
The Reasoned Schemer，第一版（麻省理工学院出版社，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* 产生了不同的结果。
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 循环。
你在 TRS1 实现中的第一个实验，在 Prolog 中（“and”是 ,，“or”是 ;）和等效的符号逻辑符号（“and”是 *，“或”是 +)，就好像
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>)。
直到排序，结果都是一样的。
书中没有搜索算法，只有解决方案流的混合算法。但是由于流是惰性的，它实现了同样的事情。
您可以以相同的方式完成其余部分，并在每个特定实现中发现 + 的更多属性。
经过几天的研究，我想我已经能够回答这个问题了。
1。概念澄清
首先，我想澄清一些概念：
有两种著名的非确定性计算模型：流模型和双连续模型。大多数 miniKanren 实现都使用流模型。
PS。术语“回溯”通常表示深度优先搜索 (DFS)，可以通过流模型或双连续模型对其进行建模。 （所以当我说“xxx get tried”时，并不意味着底层实现必须使用两个连续模型。它可以通过流模型实现，例如minikanren。）
2。解释conde或condi
的不同版本
2.1 conde 和 condi 在 TRS1
TRS1 为非确定性选择提供了两个目标构造函数，conde 和 condi.
conde使用DFS，由stream的MonadPlus实现
MonadPlus的缺点是不公平。当第一个选择提供无限数量的结果时，第二个选择永远不会被尝试。它使搜索不完整。
为了解决这个不完整的问题，TRS1 引入了 condi 可以交错两个结果。
condi 的问题是它不能很好地处理发散（我的意思是没有价值的死循环）。例如，如果第一个方案出现分歧，则第二个方案仍然无法尝试。
本书的Frame 6:30和6:31中描述了这种现象。有些情况下可以用alli来挽救，见Frame 6:32，但总的来说还是不能覆盖所有发散的情况，见Frame 6:39或下面的情况：(PS.TRS2.)
中不存在所有这些问题
(define (nevero)
(all (nevero)))
(run 2 (q)
(condi
((nevero))
((== #t q))
((== #f q))))
;; => divergence
实施细节：
在TRS1中，流是标准流，即lazy-list。
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 定义的关系的 return 值时才会交错。所以它实际上更像旧的 conde 如果你不使用 defref.
conde也修复了condi的上述问题。
实施细节：
在 TRS2 中，流不是标准流。
正如书上所说
A stream is either the empty list, a pair whose cdr is a stream, or a suspension.
A suspension is a function formed from (lambda () body) where (( lambda () body)) is a stream.
所以在TRS2中，流并不是在每个元素上都是惰性的，只是在挂点上是惰性的。
只有一个地方可以初始创建暂停，即 defref:
(define-syntax defrel
(syntax-rules ()
((defrel (name x ...) g ...)
(define (name x ...)
(lambda (s)
(lambda ()
((conj g ...) s)))))))
这是合理的，因为产生无限结果或发散的“唯一”方式是递归关系。这也意味着如果你使用 define 而不是 defrel 来定义关系，你将遇到 TRS1 中 conde 相同的问题（有限深度是可以的-第一次搜索）。
请注意，我必须在“唯一”上加上引号，因为大多数时候我们会使用递归关系，但是您仍然可以产生无限的结果或通过混合 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.3 conde 在 TRS1*
TRS1*源于早期论文《从可变参数函数到可变参数关系的迷你看人视角》。由于 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.
也就是上面的named let 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) 被 binded 到 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 在他对问题的评论中所说：
BTW I didn't know you could write (define (tmp-rel-2 y) (== 'd y) (tmp-rel-2 y)) like that, without any special minikanren form enclosing the two goals...
是的，关于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)))
我犯了这个错误，因为我之前不熟悉 minikanren。
但是这个错误不会影响最终的结果，下面对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* 中，暂停在 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 实现都可能有自己的 hack。可能有一些极端情况在不同的实现中具有略微不同的行为。幸运的是，minikanren 很容易理解。遇到这些corner case，我们可以通过阅读源码来解决。
5。参考文献
The Reasoned Schemer，第一版（麻省理工学院出版社，2005 年）
从可变函数到可变关系 - miniKanren 视角
The Reasoned Schemer，第二版（麻省理工学院出版社，2018 年）
µKanren：关系编程的最小功能核心
回溯、交错和终止 Monad 转换器
我目前正在通过 The Reasoned Schemer 和 Racket 学习 miniKanren。
我有三个版本的 minikanren 实现：
The Reasoned Schemer，第一版（麻省理工学院出版社，2005 年）。我叫它
TRS1https://github.com/miniKanren/TheReasonedSchemer
PS。它说
condi已被conde的改进版本取代，后者执行交错。The Reasoned Schemer，第二版（麻省理工学院出版社，2018 年）。我叫它
TRS2https://github.com/TheReasonedSchemer2ndEd/CodeFromTheReasonedSchemer2ndEd
The Reasoned Schemer，第一版（麻省理工学院出版社，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* 产生了不同的结果。
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 循环。
你在 TRS1 实现中的第一个实验，在 Prolog 中（“and”是 ,，“or”是 ;）和等效的符号逻辑符号（“and”是 *，“或”是 +)，就好像
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>)。
直到排序，结果都是一样的。
书中没有搜索算法，只有解决方案流的混合算法。但是由于流是惰性的，它实现了同样的事情。
您可以以相同的方式完成其余部分，并在每个特定实现中发现 + 的更多属性。
经过几天的研究，我想我已经能够回答这个问题了。
1。概念澄清
首先，我想澄清一些概念：
有两种著名的非确定性计算模型：流模型和双连续模型。大多数 miniKanren 实现都使用流模型。
PS。术语“回溯”通常表示深度优先搜索 (DFS)，可以通过流模型或双连续模型对其进行建模。 （所以当我说“xxx get tried”时，并不意味着底层实现必须使用两个连续模型。它可以通过流模型实现，例如minikanren。）
2。解释conde或condi
的不同版本
2.1 conde 和 condi 在 TRS1
TRS1 为非确定性选择提供了两个目标构造函数，conde 和 condi.
conde使用DFS，由stream的MonadPlus实现
MonadPlus的缺点是不公平。当第一个选择提供无限数量的结果时，第二个选择永远不会被尝试。它使搜索不完整。
为了解决这个不完整的问题，TRS1 引入了 condi 可以交错两个结果。
condi 的问题是它不能很好地处理发散（我的意思是没有价值的死循环）。例如，如果第一个方案出现分歧，则第二个方案仍然无法尝试。
本书的Frame 6:30和6:31中描述了这种现象。有些情况下可以用alli来挽救，见Frame 6:32，但总的来说还是不能覆盖所有发散的情况，见Frame 6:39或下面的情况：(PS.TRS2.)
(define (nevero)
(all (nevero)))
(run 2 (q)
(condi
((nevero))
((== #t q))
((== #f q))))
;; => divergence
实施细节：
在TRS1中，流是标准流，即lazy-list。
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 定义的关系的 return 值时才会交错。所以它实际上更像旧的 conde 如果你不使用 defref.
conde也修复了condi的上述问题。
实施细节：
在 TRS2 中，流不是标准流。
正如书上所说
A stream is either the empty list, a pair whose cdr is a stream, or a suspension.
A suspension is a function formed from (lambda () body) where (( lambda () body)) is a stream.
所以在TRS2中，流并不是在每个元素上都是惰性的，只是在挂点上是惰性的。
只有一个地方可以初始创建暂停，即 defref:
(define-syntax defrel
(syntax-rules ()
((defrel (name x ...) g ...)
(define (name x ...)
(lambda (s)
(lambda ()
((conj g ...) s)))))))
这是合理的，因为产生无限结果或发散的“唯一”方式是递归关系。这也意味着如果你使用 define 而不是 defrel 来定义关系，你将遇到 TRS1 中 conde 相同的问题（有限深度是可以的-第一次搜索）。
请注意，我必须在“唯一”上加上引号，因为大多数时候我们会使用递归关系，但是您仍然可以产生无限的结果或通过混合 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.3 conde 在 TRS1*
TRS1*源于早期论文《从可变参数函数到可变参数关系的迷你看人视角》。由于 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.
也就是上面的named let 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) 被 binded 到 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 在他对问题的评论中所说：
BTW I didn't know you could write
(define (tmp-rel-2 y) (== 'd y) (tmp-rel-2 y))like that, without any special minikanren form enclosing the two goals...
是的，关于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)))
我犯了这个错误，因为我之前不熟悉 minikanren。
但是这个错误不会影响最终的结果，下面对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* 中，暂停在 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 实现都可能有自己的 hack。可能有一些极端情况在不同的实现中具有略微不同的行为。幸运的是，minikanren 很容易理解。遇到这些corner case，我们可以通过阅读源码来解决。
5。参考文献
The Reasoned Schemer，第一版（麻省理工学院出版社，2005 年）
从可变函数到可变关系 - miniKanren 视角
The Reasoned Schemer，第二版（麻省理工学院出版社，2018 年）
µKanren：关系编程的最小功能核心
回溯、交错和终止 Monad 转换器