After several days of research, I think I have been able to answer this question.
1. Concept clarification
First of all, I'd like to clarify some concepts:
There are two well-known models of non-deterministic computation: the stream model and the two-continuations model. Most of miniKanren implementations use the stream model.
PS. The term "backtracking" generally means depth-first search (DFS), which can be modeled by either the stream model or the two-continuations model. (So when I say "xxx get tried", it doesn't mean that the underlying implementation have to use two-continuations model. It can be implemented by stream model, e.g. minikanren.)
2. Explain the different versions of the conde or condi
2.1 conde and condi in TRS1
TRS1 provides two goal constructors for non-deterministic choice, conde and condi.
conde uses DFS, which be implemented by MonadPlus of stream.
The disadvantage of MonadPlus is that it is not fair. When the first alternative offers an infinite number of results, the second alternative is never tried. It making the search incomplete.
To solve this incomplete problem, TRS1 introduced condi which can interleave the two results.
The problem of the condi is that it can’t work well with divergence (I mean dead loop with no value). For example, if the first alternative diverged, the second alternative still cannot be tried.
This phenomenon is described in the Frame 6:30 and 6:31 of the book. In some cases you may use alli to rescue, see Frame 6:32, but in general it still can not cover all the diverged cases, see Frame 6:39 or the following case: (PS. All these problems do not exist in TRS2.)
(define (nevero)
(all (nevero)))
(run 2 (q)
(condi
((nevero))
((== #t q))
((== #f q))))
;; => divergence
Implementation details:
In TRS1, a stream is a standard stream, i.e. lazy-list.
The conde is implemented by mplus:
(define mplus
(lambda (a-inf f)
(case-inf a-inf
(f)
((a) (choice a f))
((a f0) (choice a (lambdaf@ () (mplus (f0) f)))))))
The condi is implemented by 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 in TRS2
TRS2 removed the above two goal constructors and provided a new conde .
The conde like the condi, but only interleaving when the first alternative is a return value of a relation which be defined by defref. So it is actually more like the old conde if you won't use defref.
The conde also fixed the above problem of condi.
Implementation details:
In TRS2, a stream is not a standard stream.
As the book says that
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.
So in TRS2, streams are not lazy in every element, but just lazy at suspension points.
There is only one place to initially create a suspension, i.e. defref:
(define-syntax defrel
(syntax-rules ()
((defrel (name x ...) g ...)
(define (name x ...)
(lambda (s)
(lambda ()
((conj g ...) s)))))))
This is reasonable because the "only" way to produce infinite results or diverge is recursive relation. It also means that if you use define instead of defrel to define a relation, you will encounter the same problem of conde in TRS1 (It is OK for finite depth-first search).
Note that I had to put quotation marks on the "only" because most of the time we will use recursive relations, however you still can produce infinite results or diverge by mixing Scheme's named let, for example:
(run 10 q
(let loop ()
(conde
((== #f q))
((== #t q))
((loop)))))
;; => divergence
This diverged because there is no suspension now.
We can work around it by wrapping a suspension manually:
(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)
The conde is implemented by 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 in TRS1*
TRS1* originates from the early paper "From Variadic Functions to Variadic Relations A miniKanren Perspective". As TRS2, TRS1* also removed the two old goal constructors and provided a new conde.
The conde like the conde in TRS2, but only interleaving when the first alternative itself is a conde.
The conde also fixed the above problem of condi.
Note that there is no defref in TRS1*. Therefore if the recursive relations are not starting from conde, you will encounter the same problem of condi in TRS1. For example,
(define (nevero)
(fresh (x)
(nevero)))
(run 2 (q)
(conde
((nevero))
((== #t q))
((== #f q))))
;; => divergence
We can work around this problem by wrapping a conde manually:
(define (nevero)
(conde
((fresh (x)
(nevero)))))
(run 2 (q)
(conde
((nevero))
((== #t q))
((== #f q))
))
;; => '(#t #f)
Implementation details:
In TRS1*, the stream is the standard stream + suspension.
(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.
It also means that the named let loop problem above does not exist in TRS1*.
The conde is implemented by the interleaving 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
Note that although the function is named mplus, it is not a legal MonadPlus because it does not obey MonadPlus law.
3. Explain these experiments in the question.
Now I can explain these experiments in the question.
1st experiment
TRS1 => '((a c) (a d) (b e) (b f)) , because conde in TRS1 is DFS.
TRS2 => '((a c) (a d) (b e) (b f)) , because conde in TRS2 is DFS if no defref involved.
TRS1* => '((a c) (b e) (a d) (b f)), because conde in TRS1* is interleaving (the outmost conde make the two innermost condes interleaving).
Note that if we replace conde with condi in TRS1, the result will be the same as TRS1*.
2nd experiment
TRS1 => '(() (()) (() ()) (() () ()) (() () () ())) , because conde in TRS1 is DFS. The second clause of conde in listo is never tried, since when (fresh (d) (cdro l d) (lolo d) is binded to the first clause of conde in listo it offers an infinite number of results.
TRS2 => '(() (()) ((_0)) (() ()) ((_0 _1))) , because now the second clause of conde in listo can get tried. listo and lolo being defined by defrel means that they will potentially create suspensions. When append-inf these two suspensions, each takes a step and then yield control to the other.
TRS1* => '(() (()) ((_.0)) (() ()) ((_.0 _.1)), is the same as TRS2, except that suspensions are created by conde.
Note that replacing conde with condi in TRS1 will not change the result. If you want to get the same result as TRS2 or TRS1*, wrap alli at the second clause of conde.
3rd experiment
Note that as @WillNess said in his comment of the question:
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...
Yes, the 3rd experiment about TRS1 and TRS1* has a mistake:
(define (tmp-rel-2 y) ; <--- wrong relation definition!
(== 'd y)
(tmp-rel-2 y))
Unlike TRS2, TRS1 and TRS1* have no build-in defrel, so the define form is from Scheme, not minikaren.
We should use a special minikanren form enclosing the two goals.
Therefore,
For TRS1, we should change the definition to
(define (tmp-rel-2 y)
(all (== 'd y)
(tmp-rel-2 y)))
For TRS1*, there is no all constructor, but we can use (fresh (x) ...) to work around it
(define (tmp-rel-2 y)
(fresh (x)
(== 'd y)
(tmp-rel-2 y)))
I made this mistake because I was not familiar with minikanren before.
However, this mistake won't affect the final result, and the explanation below for TRS1 and TRS1* are suitable for both the wrong definition and the correct definition.
TRS1 => '((a c)), because conde in TRS1 is DFS. The tmp-rel diverges at tmp-rel-2.
Note that replacing conde with condi and (run 2 ...), we will get '((a c) (b e)). This because condi can interleave. However, it still cannot print the third solution (b f) because condi can’t work well with divergence.
TRS2 => '((b e) (b f) (a c)) , because TRS2 can archive complete search if we use defrel to define relation.
Note that the final result is '((b e) (b f) (a c)) instead of '((a c) (b e) (b f)) because in TRS2, a suspension only initially be created by defrel. If we expect '((a c) (b e) (b f)), we can wrap the suspension manually:
(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)), because in TRS1*, suspensions be wrapped at condes .
Note that it still cannot print the third solution (b f) because tmp-rel-2 does not be wrapped in conde, so no suspension is created here. If we expect '((a c) (b e) (b f)), we can wrap the suspension manually:
(define (tmp-rel-2 y)
(conde ((== 'd y) (tmp-rel-2 y)))) ; wrap a suspension by conde
4. Conclusion
All in all, minikanren is not one language but families of languages. Each minikanren implementation may have its own hack. There may be some corner cases which have slightly different behaviors in different implementations. Fortunately, minikanren is easy to understand. When encountering these corner cases, we can solve them by reading the source code.
5. References
The Reasoned Schemer, First Edition (MIT Press, 2005)
From Variadic Functions to Variadic Relations - A miniKanren Perspective
The Reasoned Schemer, Second Edition (MIT Press, 2018)
µKanren: A Minimal Functional Core for Relational Programming
Backtracking, Interleaving, and Terminating Monad Transformers
(define (tmp-rel-2 y) (== 'd y) (tmp-rel-2 y))like that, without any special minikanren form enclosing the two goals... – TranssonicTR1emits a value, it will back to the nearest backtracking point. But since I haven't finished reading the whole book yet, I can't add an answer to this question now. – Livi(A=1) __OR__ (A=2)(in pseudocode) does not produce(A=1)and waits, like a Prolog implementation would, for user's request, at which point it backtrack and produces the next solution,(A=2). instead, both are produced, in a stream, like{ (A=1) , (A=2) }. but the stream is lazy. – TranssonicTR1, we don’t need additional special form (e.g.defrel) to define the relation. I guess the sequence expressions in the body of thedefinemeansall. – Liviallsurprised me. – Transsonic'(() (()) (() ()) (() () ()) (() () () ()))because after the 2nd result(())produced, the control flow jump back to the second clause of thecondeoflolo, rather thanlisto. – LiviTRS2,TRS1andTRS1*have no build-indefrel, so thedefineform is from Scheme, not minikaren. We still needallor(fresh (x) ...)to wrap a sequence expressions. BTW after several days of research, I added an answer to my own question. – Livi