On Exercise (or entry?) 57, I'm just not understanding how the logic flows. The question is that this: given
(define teacupo
(lambda (x)
(conde
((= tea x ) #s)
((= cup x ) #s)
(else #u))))
where '=' is actually the triple-bar unify (?) operator. Running the following:
(run* (r)
(fresh (x y)
(conde
((teacupo x) (= #t y) #s)
((= #f x) (= #t y))
(else #u)
(= (cons x (cons y ())) r)))
the book gives the answer:
((tea #t) (cup #t) (#f #t))
I would have thought that the answer would have been:
(((tea cup) #t) (#f #t))
My reasoning being that the 'x' in (teacupo x) should have its conde go through all of its solutions first, and unify to the list of all of its solutions. But it appears that teacupo only gives up one of its solutions at a time. It confuses me because my interpretation of conde is that, using the rule it gives, is that you should go through the lines of conde, and after a line succeeds, pretend that it failed, refresh the variables and find the next line that succeeds. Given the way that the solution works, it seems like the conde in that code goes back to a successful line, then forcing the teacupo conde to fail and give up the next possible value. Again, I would have thought that the teacupo solution would give up all of its conde solutions in a list, and then move on in the outer conde call. Can anyone provide me guidance as to why it works as provided in the book and not in the way I reasoned?
(teacupo x)
means "succeed twice: once withx
unified withtea
, and the second time withx
unified withcup
". Then,means,
(teacupo x)
, also unifyy
with#t
and succeed; and also(= #f x)
, also unifyy
with#t
and succeed; and alsoSo each
x
in(tea cup)
is paired up withy
in(#t)
, and alsox
in(#f)
is paired up withy
in(#t)
, to formr
; and thenr
is reported, i.e. collected into the final result list of solutions, giving( (tea #t) (cup #t) (#f #t) )
.yes, this is exactly right, conceptually.
yes, but each line can succeed a multiple number of times, if the conditional (or a subsequent goal) succeeds a multiple number of times.
it actually prepares to produce them in advance (but as a stream, not as a list), and then each is processed separately, fed through the whole chain of subsequent steps until either the last step is reached successfully, or the chain is broken, cut short by an
#u
or by an otherwise failed goal. So the next one is tried when the processing of a previous one has finished.In pseudocode:
As to why does it work this way, I can point you to another answer of mine, which might be of help (though it doesn't use Scheme syntax).
Using it, as an illustration, we can write your test as a Haskell code which is actually functionally equivalent to the book's code I think (in this specific case, of course),
with bare minimum implementation, just enough to make the above code work,
producing the output
And if we change the second line in the translated
conde
expression towe indeed get only two results,