Frame 6:8 - Why do we not get stuck in the recursion?

Question

We get:

(defrel (alwayso)
  (conde
    (#s)
    ((alwayso))))

(run 1 q
  (alwayso)
  #u)

The book (2nd ed) says:

"alwayso succeeds, followed by #u, which causes (alwayso) to be retried, which succeeds again".

I still don't get the control flow. Why aren't both arms of the conde tried (continuing in the recursion) before stepping out to #u?

Answer 1

"Why aren't both arms of the conde tried (continuing in the recursion) before stepping out to #u?"

You meant, why the second arm is not tried before stepping out to #u with the result from the first.

The short answer is, lazy-sequences (also, lazy-evaluation) paradigm.

Under the eager evaluation paradigm, each goal produces all if its solutions in full. If their number is unbounded ("infinite"), this means infinite looping, indeed as you expected.

Under the lazy evaluation paradigm, each goal produces its solutions one by one -- meaning, it produces only its first result and stays ready to produce the next when and if requested.

---

Goals produce their resulting substitutions one by one, as if by yield in Python. So do the combined goals as well. The conde combination combines its subgoal in a certain way (see below), and produces the combined goal's results one by one. Thus

#| (defrel (alwayso)
  (conde
    (#s)
    ((alwayso)))) |#

(run 1 q
  (alwayso)
  #u)
=
(run 1 q
  (conde
    (#s)          ; 1.1
    ((alwayso)))  ; 1.2  ->  ; 1  
  #u)                        ; 2

run's first goal, the combined goal conde, produces its results one by one, each result being fed to the second run goal, #u, as soon as it is produced.

If all the solutions of run's first subgoal were to be produced before feeding the list of results to the next subgoal, the evaluation would never end for any goal capable of producing infinite list (or more precisely, unbounded stream) of results.

These streams are thus lazy streams, and lists are eager lists. The difference is operational. Under eager scheme, the first subgoal's list is first built in full, and only then processed by the next goal. When the number of results is infinite, building an infinite eager list will take infinite time.

Thus under the eager evaluation paradigm it would indeed get stuck in the recursion inside that conde.

Under the lazy evaluation paradigm, chosen by the book's implementation, it gets stuck in a bigger loop, bouncing off the #u back every time. But the conde works, producing its resulting substitutions successfully one by one.

Scheme itself is an eager language. Delaying the production of the rest of stream is achieved by putting it behind the lambda, Roughly,

(cons   1       rest-of-list)

(an eager list) is replaced with

(cons   1  (^() code-to-produce-the-rest-of-stream))

(a lazy stream).

---

alwayso is defined so that it produces an infinite stream of copies of its input substitution, unchanged. But it produces them one by one.

Then run feeds this stream from its first goal, to the second goal, #u, which rejects it. Since run 1 demands one solution from its subgoals, it retries them until one solution / substitution goes through.

Which never happens.

So this should result in infinite looping.

Again, both arms are tried -- first, the first one; then, after its (one) result gets rejected by the subsequent #u, the second arm is tried. And the resulting substitution gets rejected, again. Ad infinitum:

;; we have
(defrel (alwayso)
  (conde
    (#s)
    ((alwayso))))

;; running:
(run 1 q
  (alwayso)
  #u)
=
(run 1 q
  (conde         ; (a OR b) , c
    (#s)
    ((alwayso)))
  #u)
=
(run 1 q         ; (a , c) OR (b , c)
  (conde
    (#s #u)
    ((alwayso) #u)))
=
(run 1 q 
  (alwayso) 
  #u)
=
.....

Getting stuck.

---

Following the implementation's definitions closer,

(defrel (alwayso)
  (conde
    (#s)
    ((alwayso))))
= ; by def of defrel; with ^ for lambda
(define (alwayso)
  (^s (^() ( (conde
               (#s)                 ; first 
               ((alwayso))) s))))   ; second
= ; by defs of conde, conj and disj
(define (alwayso)
  (^s (^() ( (disj2
                #s                  ; first
                (alwayso) ) s))))   ; second
= ; by def of disj2
(define (alwayso)           ; (-1-)
  (^s (^() (append-inf
               (#s s)               ; first
               ((alwayso) s)) )))   ; second
= ; by defs of #s and alwayso (-1-)
(define (alwayso)
  (^s (^() (append-inf
               (list s)             ; first
               (^() (append-inf     ; second
                      (#s s)
                      ((alwayso) s)) )) )))
= ; by def of append-inf
(define (alwayso)
  (^s (^() (cons s                  ; first
               (^() (append-inf     ; second
                      (#s s)
                      ((alwayso) s)) )) )))
= ; by def of append-inf
(define (alwayso)
  (^s (^() (cons s
               (^() (cons s
                      ((alwayso) s)) )) )))
=
  ....

so indeed we see here a definition which produces a stream of an unbounded number of copies of the input substitution s, as and when requested, as the result of a call ((alwayso) <s>).

Or, in pseudocode, writing ++ for append-inf and [s] for (list s),

((alwayso) s) 
= 
  ((#s OR (alwayso)) s)
=
  (#s s) ++ ((alwayso) s)
=
  [s] ++ ((#s OR (alwayso)) s)
=
  [s] ++ [s] ++ ((#s OR (alwayso)) s)
=
  [s] ++ [s] ++ [s] ++ ((#s OR (alwayso)) s)
=
  [s      s      s      .... ]

Finally,

(run 1 q (alwayso) #u)
= ; by def of run
  (let ((q (var 'q)))
    (map (reify q)
         (run-goal 1 (conj (alwayso) #u))))
= ; by defs of run-goal and conj
  (let ((q (var 'q)))
    (map (reify q)
         (take-inf 1 ((conj2 (alwayso) #u) empty-s))))
= ; by defs of conj2 and #u
  (let ((q (var 'q)))
    (map (reify q)
         (take-inf 1 
           (append-map-inf (^s '())
               ((alwayso) empty-s)))))

and no matter how many empty-s's it applies the (^s '()) to, to append the results together, all the results are empty lists, so it can't take even one of the contained results because there are none. In pseudocode, writing s0 for empty-s,

  (take-inf 1 
              (append-map-inf (^s '())
                     ((alwayso) empty-s)))
= ; as established above
  (take-inf 1 (append-map-inf (^s [])
                          [ s0 s0 s0 .... ]))
= ; by def of append-map-inf
  (take-inf 1 
    (append-inf ((^s []) s0)
              (append-map-inf (^s [])
                             [ s0 s0 .... ])))
= ; by beta-reduction
  (take-inf 1 
    (append-inf []
              (append-map-inf (^s [])
                             [ s0 s0 .... ])))
= ; be def of append-if
  (take-inf 1 
              (append-map-inf (^s [])
                             [ s0 s0 .... ]))
= ; and we're back where we've started
  <LOOPING> 

Or, symbolically,

  (take 1 (append-map-inf (^s [])
                      [ s0 s0 s0 .... ]))
=
  (take 1 (append-inf [ [] [] [] .... ]))
=
  (take 1 [             ; sic!

So it gets stuck.