How to explain run 5 (x) g0 g1 in The Reasoned Schemer

Question

I don't understand how the run n (x) g0 g1 ... to run through listo

the listo is defined like this

(define listo
  (lambda (l)
    (conde
      [(nullo l) #s)]
      [(pairo l)
       (fresh (d)
         (cdro l d)
         (listo d))]
      [else #u])))

The Reasoned Schemer on page 29 in segment 14 says the code

(run 5 (x)
  (listo (a b c . x)))

produces the result

(()
 (_.0)
 (_.0 _.1)
 (_.0 _.1 _.2)
 (_.0 _.1 _.2 _.3))

Would you explain how does this happened ? Thank you in advance.

Answer 1

The query is

(run 5 (x)
  (listo `(a b c . ,x)))

I've added quasiquote ` and unquote ,, the book uses bold and non-bold text for that:

(run5 (x)
  (listo (a b c . x)))

anyway the way listo works is it tries to check (nullo `(a b c . ,x)) and this fails, so it tries to check (pairo `(a b c . ,x)) and this succeeds. So it follows that branch of the conde and runs

(fresh (d)
     (cdro `(a b c . ,x) d)
     (listo              d))

the cdro produces d = `(b c . ,x) so we have

(fresh (d)
     ; (cdro `(a b c . ,x) `(b c . ,x))  ;; disappears, has been solved
     (listo                `(b c . ,x)))

So now this whole process repeats for (listo `(b c . ,x)) and then (listo `(c . ,x)) and then (listo x)

That's also the only possible branch that can be taken, so (listo `(a b c . ,x)) is logically equivalent to (listo x). Both queries will produce the same results.