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.
On
The frame 1-53 states:
The value of
(run* q (conj2 (≡ 'corn q) (≡ 'meal q)))is().In order for the
conj2to succeed,(≡ 'corn q)and(≡ 'meal q)must both succeed. The first goal succeeds, associatingcornwithq. The second goal cannot then [emphasis mine - wn] associatemealwithq, sinceqis 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 disj2 which "runs" them independently, "in parallel".
This also means that it is entirely plausible for the code (run* (q p) (conj2 (≡ '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 conj2 "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))
The first goal in the conjunction instantiates the
x, the second instantiates they, andrun (x y)says to report both.Both
xandyget instantiated becausexis different fromy, 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.)
sis a solution, a substitution, a record of(name,value)pairs. It is extended by unification:(all the operators like
++:("append" a.k.a. "mplus"),||:("or" a.k.a. "disj2"),>>:("push-through" a.k.a. "bind"),&&:("and" a.k.a. "conj2"), 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 thatx ≡ 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 withs. 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:
(3.) A conjunction passes each solution of the first goal through the second:
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, sincexandyare 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:
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 likefor a suitably defined
report <vars>goal.(6.) And
run* (x) (teacup° x) (teacup° x))is more or less like