Frame 1:85 - Why does a conj2 of disj2 accumulate?

Question

In 85 there is:

(run* (x y)
  (teacupo x)
  (teacupo y))

which expands into:

(run* (x y)
  (disj 2
    (== 'tea x)
    (== 'cup x))
  (disj 2
    (== 'tea y)
    (== 'cup y)))

So then how does conj2 accumulate the results to be ((tea tea) (tea cup) (cup tea) (cup cup))? I don't think this has been explained properly in the book.

Will Ness · Answer 1 · 2022-09-11T21:25:25.893

The first goal in the conjunction instantiates the x, the second instantiates the y, and run (x y) says to report both.

Both x and y get instantiated because x is different from y, so they are independent from each other.

This can be modeled under the solutions streams' combination paradigm as in this answer of mine (equivalent to the book's model sans the logical variables), as this pseudocode:

(1.) s is a solution, a substitution, a record of (name,value) pairs. It is extended by unification:

(var ≡ val) s  =  [[(x,v)] ++: s]   //  IF (x,_) NOT IN s     , OR
|              =  [s]               //  IF (x,u) IN s AND u=v , OR
|              =  []                //  OTHERWISE.

(all the operators like ++: ("append" a.k.a. "mplus"), ||: ("or" a.k.a. "disj₂"), >>: ("push-through" a.k.a. "bind"), &&: ("and" a.k.a. "conj₂"), etc. are defined in the linked answer. The syntax is a free-licensed "curried application by juxtaposition", similar to Haskell's).

A substitution represents our knowledge so far. The unification (x ≡ TEA), say, is a goal -- a procedure which, given a substitution, produces a stream of new substitutions (here, one or none), augmented with the new knowledge that x ≡ TEA (we use all-caps names as auto-quoted symbols).

Augmenting a substitution involves possible rejection of irreconcilable values.

The result is a list containing either one valid, possibly extended substitution, or an empty list containing none, meaning (x,v) was incompatible with s. This expresses the notion that a logical variable's value, once set, can not change (except through backtracking).

(2.) A disjunction involves application of the goals, separately, and passing along all the resulting valid solutions (substitutions) together:

teacup° x    =  x ≡ TEA  ||:  x ≡ CUP
-- thus,
teacup° x s  = (x ≡ TEA  ||:  x ≡ CUP) s
             = (x ≡ TEA) s  ++:  (x ≡ CUP) s

(3.) A conjunction passes each solution of the first goal through the second:

(teacup° x &&: teacup° y) []    -- the initial substitution is empty
  =  teacup° x []                       >>:  teacup° y
  = ( (x ≡ TEA      ||:   x ≡ CUP) [] ) >>:  teacup° y
  = ( (x ≡ TEA) []  ++:  (x ≡ CUP) [] ) >>:  teacup° y
  = ( [[(x,TEA)]]   ++:  [[(x,CUP)]]  ) >>:  teacup° y
  =   [[(x,TEA)]    ,     [(x,CUP)]]    >>:  teacup° y
  =  teacup° y [(x,TEA)]  ++:  teacup° y [(x,CUP)]  ++:  []
  =  (y ≡ TEA  ||:  y ≡ CUP) [(x,TEA)]  ++:  
      (y ≡ TEA  ||:  y ≡ CUP) [(x,CUP)]
  =  (y ≡ TEA)[(x,TEA)]  ++:  (y ≡ CUP) [(x,TEA)]  ++:  
      (y ≡ TEA) [(x,CUP)]  ++:  (y ≡ CUP) [(x,CUP)]
  =  [[(y,TEA),(x,TEA)]]  ++:  [[(y,CUP),(x,TEA)]]  ++:  
      [[(y,TEA),(x,CUP)]]  ++:  [[(y,CUP),(x,CUP)]]
  =  [[(y,TEA),(x,TEA)]    ,    [(y,CUP),(x,TEA)]   ,  
       [(y,TEA),(x,CUP)]    ,    [(y,CUP),(x,CUP)]]

All in all, four solutions, four substitutions satisfying the goal teacup° x &&: teacup° y, were produced.

A conjunction &&: of two goals will, for each of the solutions produced by the first goal, collect all the solutions produced by the second which are conformant with the solution received by the second goal. Here, since x and y are two separate variables, every new solution does not collide with the old, in other words, none of the solutions are rejected.

(4.) If we'd used the same variable twice, their interaction would mean that we must reject irreconcilable substitutions:

(teacup° x &&: teacup° x) []    -- the initial substitution is empty
  =  teacup° x []                       >>:  teacup° x
  = ( (x ≡ TEA      ||:   x ≡ CUP) [] ) >>:  teacup° x
  = ( (x ≡ TEA) []  ++:  (x ≡ CUP) [] ) >>:  teacup° x
  = ( [[(x,TEA)]]   ++:  [[(x,CUP)]]  ) >>:  teacup° x
  =   [[(x,TEA)]    ,     [(x,CUP)]]    >>:  teacup° x
  =  teacup° x [(x,TEA)]  ++:  teacup° x [(x,CUP)]  ++:  []
  =  (x ≡ TEA  ||:  x ≡ CUP) [(x,TEA)]  ++:  
      (x ≡ TEA  ||:  x ≡ CUP) [(x,CUP)]
  =  (x ≡ TEA)[(x,TEA)]  ++:  (x ≡ CUP) [(x,TEA)]  ++:  
      (x ≡ TEA) [(x,CUP)]  ++:  (x ≡ CUP) [(x,CUP)]
  =  [[(x,TEA)]]  ++:  []  ++:  []  ++:  [[(x,CUP)]]
  =  [[(x,TEA)]   ,                       [(x,CUP)]]

Here, two solutions are produced because the same logical variable can not hold two different values at once, so e.g. (x ≡ CUP) [(x,TEA)] resolves as [], the empty list containing no solutions, thus rejecting the attempted assignment (x,CUP) when (x,TEA) is already present.

(5.) (run* (x y) (teacup° x) (teacup° y)) is more or less like

[[]] >>: (teacup° x &&: teacup° y) >>: report [x, y]
==
(teacup° x &&: teacup° y) [] >>: report [x, y]
==
[[(y,TEA),(x,TEA)], [(y,CUP),(x,TEA)],  
  [(y,TEA),(x,CUP)], [(y,CUP),(x,CUP)]] >>: report [x, y]
==
report [x, y] [(y,TEA),(x,TEA)] ++:
 report [x, y] [(y,CUP),(x,TEA)] ++:
  report [x, y] [(y,TEA),(x,CUP)] ++:
   report [x, y] [(y,CUP),(x,CUP)]
==
 [ (TEA,TEA), (TEA,CUP), (CUP,TEA), (CUP,CUP) ]

for a suitably defined report <vars> goal.

(6.) And run* (x) (teacup° x) (teacup° x)) is more or less like

[[]] >>: (teacup° x &&: teacup° x) >>: report [x]
==
(teacup° x &&: teacup° x) [] >>: report [x]
==
 [[(x,TEA)], [(x,CUP)]] >>: report [x]
==
  report [x] [(x,TEA)]  ++: report [x] [(x,CUP)]
==
 [ TEA, CUP ]

I'm going to try to read this. But 1. the book neglected to explain this? 2. I don't think I have the context to understand this. — Alper, Sep 10 '22 at 17:01
I worked through the 1st edition and came up with that other answer. (well, there was a post on amazon review first, quite a few years earlier...). I was trying to understand the macro based implementation in the end of the book. the "pseudocode" in that other answer does the same thing as the book's code, more or less -- those parts that don't have anything to do with the logical variables, that is. — Will Ness, Sep 10 '22 at 17:04
the authors' method as far as I understand it, is to give some vague expositions first, and precise definitions later. have you read through the whole book yet, or did you expect that to be explained already by the time we encounter that frame? because in all likelihood it isn't, until much later in the book. perhaps the explanation is already hinted at, though. would you like to find that hint? or the precise definition that entails this behavior? (I've updated the answer BTW, give it a go, I tried to make it clearer and easier to follow... and don't hesitate to ask for clarifications :) ). — Will Ness, Sep 11 '22 at 13:54

Will Ness · Answer 2 · 2022-09-12T19:30:34.503

The frame 1-53 states:

The value of (run* q (conj₂ (≡ 'corn q) (≡ 'meal q))) is ().

In order for the conj₂ to succeed, (≡ 'corn q) and (≡ 'meal q) must both succeed. The first goal succeeds, associating corn with q. The second goal cannot then _{[emphasis mine - wn]} associate meal with q, since q is no longer_{[emphasis mine - wn]} fresh.

This means that in the binary conjunction, the knowledge about the state of association of variables and values must be passed on from the first goal to the second. Thus the "execution" of the second goal comes after that of the first, in contrast to disj₂ which "runs" them independently, "in parallel".

This also means that it is entirely plausible for the code (run* (q p) (conj₂ (≡ 'corn q) (≡ 'meal p))) to have (corn meal) as its value, because p is "still" fresh even after the the goal (≡ 'corn q) was "executed". This can, in fact, be seen in the frames 1-67 and 1-68.

Thus conj₂ "accumulates" the knowledge of the variable-value associations from its first goal to the next, also known as substitution.

But then, what if the first goal in a conjunction is a disjunction which produces more than one value?

The first relevant frame is 1-77 that shows that each of those must be passed along to the second, in turn, while collecting every result. But indeed it does not discuss this crucial point there.

Thus, schematically, ((a OR b), c) == ((a, c) OR (b, c)) (writing , for AND), and similarly (a, (b OR c)) == ((a, b) OR (a, c)), and thus

  (a OR b) , (c OR d)
==
  (a, (c OR d)) OR (b, (c OR d))
==
  (a, c) OR (a, d) OR (b, c) OR (b, d)

which is the same as reading the following matrix row-by-row:

          c     d
       -------------
   a  |  a,c   a,d
   b  |  b,c   b,d
       -------------

In other words,

  (run* q
    (conj2 (≡ 'corn q) (≡ 'meal q)))    =>  ()
  (run* q
    (conj2 (≡ 'corn q) (≡ 'corn q)))    =>  (corn)
  (run* q
    (disj2 (≡ 'corn q) (≡ 'meal q)))    =>  (corn meal)
  (run* (q p) 
    (conj2 (≡ 'corn q) (≡ 'meal p)))    =>  ((corn meal))
  (run* (q p) 
    (conj2 
      (≡ 'butter p)
      (disj2 (≡ 'corn q) (≡ 'meal q)))) =>  ((corn butter) (meal butter))
  (run* (q p) 
    (conj2 
      (disj2 (≡ 'corn q) (≡ 'meal q))
      (≡ 'butter p)))                   =>  ((corn butter) (meal butter))
  (run* (q p) 
    (conj2 
      (disj2 (≡ 'corn q) (≡ 'meal q))
      (disj2 (≡ 'butter p) (≡ 'bread p))))
                                        =>  ((corn butter) (corn bread) 
                                             (meal butter) (meal bread))

I've posted this as a separate answer, because it is based on the book, wholly different from my first answer's approach (though equivalent) . — Will Ness, Sep 12 '22 at 09:49
Thanks, it'll take me some time to trace this but this seems a lot more doable than the other answer. — Alper, Sep 12 '22 at 22:46

Frame 1:85 - Why does a conj2 of disj2 accumulate?

2 Answers2