Reasonable Researcher: Not Understanding Exercise 57

Question

In exercise (or entry?) 57, I just don't understand how logic flows. The question is: given: given

(define teacupo (lambda (x) (conde ((= tea x ) #s) ((= cup x ) #s) (else #u)))) 

where '=' is actually a triune unified (?) operator. Do the following:

 (run* (r) (fresh (xy) (conde ((teacupo x) (= #ty) #s) ((= #fx) (= #ty)) (else #u) (= (cons x (cons y ())) r))) 

the book gives the answer:

 ((tea #t) (cup #t) (#f #t)) 

I would think the answer would be this:

 (((tea cup) #t) (#f #t)) 

My reasoning is that "x" in (teaupo x) must have its own conde in order to go through all its solutions and combine with a list of all its solutions. But it looks like the cup is only giving away one of its solutions at a time. This bothers me because my interpretation of conde is that, using the rule that it gives, you have to go through the conde lines, and after the line succeeds, pretend it failed, refresh the variables and find the next line which will be successful. Given how the solution works, it looks like conde in this code returns to a successful line, and then causes conduo conduo to fail and discard the next possible value. Again, I would think that teaupo would abandon all of its conde solutions in the list, and then go into an external conde call. Can someone give me directions as to why it works, as stated in the book, and not as I reasoned?

Answer 1

(teacupo x) means "execute twice: once with x combined with tea , and a second time with x combined with cup ". Then,

 (conde ((teacupo x) (= #ty) #s) ((= #fx) (= #ty)) ; you had a typo here (else #u) 

means

• for each solution created (teacupo x) , also unify y with #t and succeed; and
• for each solution created (= #fx) , also unify y with #t and succeed; and
• do not create more solutions

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

"it looks like the cup is only giving away one of its solutions at a time."

yes, that’s absolutely correct, conceptually.

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

yes, but each line can be executed several times if the conditional (or subsequent goal) succeeds several times.

"it looks like conde in this code returns to a successful line, and then causes conudo conuco to fail and discard the next possible value.

it actually prepares for their production in advance (but as a stream, not as a list), and then each is processed separately, fed through the entire chain of subsequent steps, until either the last step is reached, or the chain is broken, interrupted by #u or otherwise unsuccessful goal. Thus, the next one is checked when the processing of the previous one is completed.

In pseudo code:

 for each x in (tea cup): for each y in (#t): ; does _not_ introduce separate scope for `y`; collect (xy) ; `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 (xy) ; one known in the outer `for`, or else for each _ in (): ; it will be rejected (x can't be two different collect (xy) ; things at the same time) 

---

As for this, I can point out another answer of mine that might help (although it does not use schema syntax).

Using it, as an illustration, we can write your test as Haskell code, which is actually functionally equivalent to the code of the book that I think (in this particular 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) (= #ty) #s) ||: unify "x" (B False) &&: unify "y" (B True) -- ((= #fx) (= #ty)) ||: false -- (else #u) ) &&: project ["x", "y"] (unify "r" . L) -- (= r (list xy)) >>: reporting ["r"] -- ...... ) reporting names store = [[a | a@ (n,_) <- store, elem n names]] 

with a minimum minimum implementation sufficient to execute the above code,

 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 sn ((a,b):c) | s == a = (a,n) : c | otherwise = (a,b) : replace_val snc 

producing 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 translating the conde expression to

  ||: unify "x" (B False) &&: unify "x" (B True) -- ((= #fx) (= #tx)) 

we get only two results:

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

Answer 2

My reasoning is that the "x" in (teaupo x) must have its conde first go through all its solutions and unify the list of all its solutions.

The variable x combined into one value at a time. The form (run* (x) <goals>) collects values ​​for x that fulfill the goals.

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

IN

 (conde ((teacupo x) (== #ty)) ((== #fx) (== #ty))) 

There are two ways to achieve success: either the target (teacupo x) is met, and x is one of the tea or cup - or - the goals are fulfilled (== #fx) , and x is (unified to) #f .

In short, run* runs through the possible possible value for x , one at a time, collects those values ​​that correspond to all goals. This means that x combined into one value at a time.

The simplest 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 anyone who wants to try snippets in DrRacket:

 #lang racket (require minikanren) (define-syntax succeed (syntax-id-rules () [_ (fresh (t) (== tt))])) (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 (xy) (conde ((teacupo x) (== #ty)) ((== #fx) (== #ty))) (== (cons x (cons y '())) r)))