The Reasoned Schemer : Not understanding Exercise 57

Question

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?

Onyx

Answer 1

(teacupo x) means "succeed twice: once with x unified with tea, and the second time with x unified with cup". Then,

(conde
  ((teacupo x) (= #t y) #s)
  ((= #f x) (= #t y))        ; you had a typo here
  (else #u)

means,

• for each solution produced by (teacupo x), also unify y with #t and succeed; and also
• for each solution produced by (= #f x), also unify y with #t and succeed; and also
• produce no more solutions

So each x in (tea cup) is paired up with y in (#t), and also x in (#f) is paired up with y in (#t), to form r; and then r is reported, i.e. collected into the final result list of solutions, giving ( (tea #t) (cup #t) (#f #t) ).

"it appears that teacupo only gives up one of its solutions at a time."

yes, this is exactly right, conceptually.

"after a line succeeds, pretend that it failed, refresh the variables and find the next line that succeeds."

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 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."

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:

for each x in (tea cup):
   for each y in (#t):    ; does _not_ introduce separate scope for `y`;
       collect (x y)      ;   `x` and `y` belong to the same logical scope
for each x in (#f):       ;   so if `x` is used in the nested `for` too,
   for each y in (#t):    ;   its new value must be compatible with the 
       collect (x y)      ;   one known in the outer `for`, or else 
for each _ in ():         ;   it will be rejected (x can't be two different
       collect (x y)      ;   things at the same time)

---

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),

data Val = Fresh | B Bool | S String | L [Val] deriving Show 
type Store = [(String,Val)]

teacupo x =   unify x (S "tea") &&: true               -- ((= tea x ) #s)
          ||: unify x (S "cup") &&: true               -- ((= cup x ) #s)
          ||: false                                    -- (else #u)

run = [[("r", Fresh)]]                                 -- (run* (r) ......
  >>: (\s -> [ s ++: [("x", Fresh), ("y", Fresh)] ])   -- (fresh (x,y)
  >>:                                                  -- (conde  
    (    teacupo "x"          &&:  unify "y" (B True)  
                              &&:  true                -- ((teacupo x) (= #t y) #s)
     ||: unify "x" (B False)  &&:  unify "y" (B True)  -- ((= #f x) (= #t y))
     ||: false                                         -- (else #u)
    ) 
     &&: project ["x", "y"] (unify "r" . L)            -- (= r (list x y))
  >>:                                                  
     reporting ["r"]                                   --              ...... )

reporting names store = [[a | a@(n,_) <- store, elem n names]]

with bare minimum implementation, just enough to make the above code work,

project vars kont store = 
     kont [val | var <- vars, (Just val) <- [lookup var store]] store

unify :: String -> Val -> Store -> [Store]
unify sym val store = 
   let 
      (Just v) = (lookup sym store)
   in 
      case (val_unify v val) of
        Just newval -> [replace_val sym newval store]  -- [updated store], if unifies
        Nothing     -> []                              -- couldn't unify - reject it

val_unify v     Fresh             = Just v             -- barely working,
val_unify Fresh  v                = Just v             --  initial
val_unify (B v) (B u) | v == u    = Just (B v)         --  implementation
                      | otherwise = Nothing
val_unify (S v) (S u) | v == u    = Just (S v)
                      | otherwise = Nothing
val_unify  _     _                = Nothing

replace_val s n ((a,b):c) | s == a    = (a,n) : c
                          | otherwise = (a,b) : replace_val s n c

producing the output

*Main> run
[[("r", L [S "tea",B True])], [("r", L [S "cup",B True])], [("r", L [B False,B True])]]

And if we change the second line in the translated conde expression to

       ||: unify "x" (B False)  &&:  unify "x" (B True)  -- ((= #f x) (= #t x))

we indeed get only two results,

*Main> run
[[("r", L [S "tea",B True])], [("r", L [S "cup",B True])]]

Roley

Thanks so much for this answer, it really did help. The key, as I pointed out in soegaard's comment, was that a line in conde can succeed many times. The book's rule is that "to get another answer, pretend that the last successful conde line did not succeed, and refresh the variables." I took that to mean that a line succeeded only once, and if there were solutions, they would all have to be offered up at once. Per this, and the example, that is not how it works. Thank you for the clarification. – Onyx

@Onyx glad it helped. to really understand how it works it's best to work through the code in teh back of the book. it was kinda hard for me to read it in Scheme macros syntax, so I had to translate it into a simple Haskell, in that answer which I mention. :) – Roley

yes, that other link of yours is quite helpful too (as is, tangentially, your broken-down example of Y-combinator in another thread). I've been working through the book from front to back, and haven't looked at the end yet, but will now. The big idea for me, on nested calls, is a general "how does the odometer spin?" on different control structures -- i.e., what is the order in which goals are iterated over based on the construct used. – Onyx

@Onyx ah, the Y-combinator. I liked the idea of pseudo-execution with the let-expressions, simulating the environment model of evaluation. – Roley

Your let-expression rewriting totally opened up a new way of modeling what is going on and I am going back and re-reading other examples that I had trouble wrapping my head around because I was previously forced to keep that whole stack in my head, which was overwhelming. This whole thing has gained me more than an answer to this specific question... – Onyx

Answer 2

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.

The variable x is unified to one value at a time. The form (run* (x) <goals>) collects values for x which fulfill the goals.

> (run* (x)
    (teacupo x))
'(tea cup)

In

(conde
  ((teacupo x) (== #t y))
  ((== #f x)   (== #t y)))

there is two ways to succeed: either the goal (teacupo x) is met and x is one of tea or cup -- or -- the goals (== #f x) is met, and x is (unified to) #f.

In short run* runs through the possible possible value for x one at time collecting those values that meets all goals. This means that x is unified to one value at a time.

A simpler example:

> (run* (x)
  (fresh (y)
    (== y 10)
    (conde
     [(== x 1) (== y 10)]
     [(== x 2) (== y 20)]
     [(== x 3) (== y 10)])))
'(1 3)

Full code for those who want to try the snippets in DrRacket:

#lang racket
(require minikanren)
(define-syntax succeed (syntax-id-rules () [_ (fresh (t) (== t t))]))

(run* (x)
  (fresh (y)
    (== y 10)
    (conde
     [(== x 1) (== y 10)]
     [(== x 2) (== y 20)]
     [(== x 3) (== y 10)])))    

(define teacupo
  (lambda (x)
    (fresh (result)
      (conde
       ((== 'tea x ) succeed)
       ((== 'cup x ) succeed)))))

(run* (x)
  (teacupo x))

(run* (r)
  (fresh (x y)
    (conde
      ((teacupo x) (== #t y))
      ((== #f x)   (== #t y)))
    (== (cons x (cons y '())) r)))

Housemaid

Thank you so much for this answer, I do appreciate it. It was hard to choose an accepted answer, and I chose Will's only because he had a sentence that really spoke to the heart of my problem, which was "yes, but each line can succeed a multiple number of times". But this is an awesome answer nonetheless. – Onyx

@Onyx No problem. It was fun to play with MiniKanren again. – Housemaid