title: Clarify search algorithms in different minikanren implementation
body: <p>I am currently learning miniKanren by The Reasoned Schemer and Racket.</p>
  <p>I have three versions of minikanren implementation:</p>
  <ol>
  <li><p>The Reasoned Schemer, First Edition  (MIT Press, 2005). I called it <code>TRS1</code></p>
  <p><a href="https://github.com/miniKanren/TheReasonedSchemer" rel="nofollow noreferrer">https://github.com/miniKanren/TheReasonedSchemer</a></p>
  <p>PS. It says that <code>condi</code> has been replaced by an improved version of <code>conde</code> which performs interleaving.</p>
  </li>
  <li><p>The Reasoned Schemer, Second Edition  (MIT Press, 2018). I called it <code>TRS2</code></p>
  <p><a href="https://github.com/TheReasonedSchemer2ndEd/CodeFromTheReasonedSchemer2ndEd" rel="nofollow noreferrer">https://github.com/TheReasonedSchemer2ndEd/CodeFromTheReasonedSchemer2ndEd</a></p>
  </li>
  <li><p>The Reasoned Schemer, First Edition  (MIT Press, 2005). I called it <code>TRS1*</code></p>
  <p><a href="https://docs.racket-lang.org/minikanren/" rel="nofollow noreferrer">https://docs.racket-lang.org/minikanren/</a></p>
  </li>
  </ol>
  <p>I have did some experiments about the three implementations above:</p>
  <p>1st experiment:</p>
  <p><code>TRS1</code></p>
  <pre><code>(run* (r)
        (fresh (x y)
               (conde
                ((== 'a x) (conde
                            ((== 'c y) )
                            ((== 'd y))))
                ((== 'b x) (conde
                            ((== 'e y) )
                            ((== 'f y)))))
               (== `(,x ,y) r)))
  
  ;; =&gt; '((a c) (a d) (b e) (b f))
  </code></pre>
  <p><code>TRS2</code></p>
  <pre><code>(run* (x y)
        (conde
         ((== 'a x) (conde
                     ((== 'c y) )
                     ((== 'd y))))
         ((== 'b x) (conde
                     ((== 'e y) )
                     ((== 'f y))))))
  ;; =&gt; '((a c) (a d) (b e) (b f))  
  </code></pre>
  <p><code>TRS1*</code></p>
  <pre><code>(run* (r)
        (fresh (x y)
               (conde
                ((== 'a x) (conde
                            ((== 'c y) )
                            ((== 'd y))))
                ((== 'b x) (conde
                            ((== 'e y) )
                            ((== 'f y)))))
               (== `(,x ,y) r)))
  ;; =&gt; '((a c) (b e) (a d) (b f))
  </code></pre>
  <p>Notice that, in the 1st experiment, <code>TRS1</code> and <code>TRS2</code> produced the same result, but <code>TRS1*</code> produced a different result.</p>
  <p>It seems that the <code>conde</code> in <code>TRS1</code> and <code>TRS2</code> use the same search algorithm, but <code>TRS1*</code> use a different algorithm.</p>
  <p>2nd experiment:</p>
  <p><code>TRS1</code></p>
  <pre><code>(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))
  ;; =&gt; '(() (()) (() ()) (() () ()) (() () () ()))
  </code></pre>
  <p><code>TRS2</code></p>
  <pre><code>(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))
  ;; =&gt; '(() (()) ((_0)) (() ()) ((_0 _1)))
  </code></pre>
  <p><code>TRS1*</code></p>
  <pre><code>(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))
  ;; =&gt; '(() (()) ((_.0)) (() ()) ((_.0 _.1)))
  </code></pre>
  <p>Notice that, in the 2nd experiment, <code>TRS2</code> and <code>TRS1*</code> produced the same result, but <code>TRS1</code> produced a different result.</p>
  <p>It seems that the conde in <code>TRS2</code> and <code>TRS1*</code> use the same search algorithm, but <code>TRS1</code> use a different algorithm.</p>
  <p>These makes me very confusion.</p>
  <p>Could someone help me to clarify these different search algorithms in each minikanren implementation above?</p>
  <p>Very thanks.</p>
  <p>---- ADD A NEW EXPERIMENT ----</p>
  <p>3nd experiment:</p>
  <p><code>TRS1</code></p>
  <pre><code>(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)))
  
  ;; =&gt; '((a c))
  </code></pre>
  <p>However, <code>run 2</code> or <code>run 3</code> loops.</p>
  <p>If I use <code>condi</code> instead of <code>conde</code>, then <code>run 2</code> works but <code>run 3</code> still loop.</p>
  <p><code>TRS2</code></p>
  <pre><code>(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)))
               
  ;; =&gt; '((b e) (b f) (a c)) 
  </code></pre>
  <p>This is OK, except that the order is not as expected.</p>
  <p>Notice that <code>(a c)</code> is at the last now.</p>
  <p><code>TR1*</code></p>
  <pre><code>(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)))
  
  ;; =&gt; '((a c) (b e))
  </code></pre>
  <p>However, <code>run 3</code> loops.</p>