Find file
Fetching contributors…
Cannot retrieve contributors at this time
38 lines (33 sloc) 1.61 KB
***** An harder example
The logic program
(run* [q]
(fresh [a]
(membero a [1 3 7 9])
(membero a [1 3 8 q])))
returns (_.0 1 _.0 3 7 9); meaning that q can either be any value, or
1 or 3 or 7 or 9 ?! This can be understood looking more closely at
the all the values in play
(run* [q]
(fresh [a b]
(== q [a b])
(membero a [1 3 7 9])
(membero a [1 3 8 b])))
returns ([1 _.0] [1 1] [3 _.0] [3 3] [7 7] [9 9]). This is the same
logic program where the lvar b plays the role q did last time, and q
is now constrained to be the vector with lvars a and b as elements so
that we can examine them. Examining b we see it can be anything, or 1
or 3 or 7 or 9, exactly as q was in the last example. But we see that
it can only assume these values when a assumes particular values. So
breaking it down, we first specify that a can be either 1 or 3 or 7
or 9. Now the first value for q is [1 _.0], that means that if a is
1, b can be anything. This makes sense, the second constraints is
that a must be an element of [1 3 8 b], so, as 1 is already an element
of that vector, the value of b is irrelevent, so it can be anything.
The second element of q is [1 1], this means that if a is 1, b can
be 1. This is trivially true. The same logic applies for the third
and fourth elements of q. The last two elements of q are more
interesting. The fifth element of q is [7 7], and there are no other
elements of q where the a is 7. So this means that if a is 7, then b
can only be 7. The same logic applies to the last element of q, [9
9]. Together these are all the consistent solution to the set of
constraints given.