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

Viewed 41

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?

1 Answers

Goals produce their resulting substitutions one by one, as if by yield in Python.

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.

Related