Reasoned Schemer (3.10)

[Chris Rathman]

The Reasoned Schemer 3.10 gives the example:

(run 1 (x)
(listo `(a b c . ,x)))

and goes into a reasonable explanation of why the value of x is an
empty list. But how do I get some feedback on this? How can I echo
the value of x within the run structure? My limited and naive
knowledge of scheme makes me want to use display:

(run 1 (x)
(listo `(a b c . ,x))
(display x))

but that doesn't seem acceptable to PLT scheme, as it apparently
doesn't qualify as a goal. Actually, what I really want to know is,
what is the value of x in the 3.14 example of:

(run 5 (x)
(listo `(a b c . ,x)))

I am guessing here that listo generates five possible choice points and
that x is local to each of the possible answers. But I need to be able
to peak inside to see what's happening.

Thanks,
Chris Rathman

[Michel Salim]

If you need to verify that x is bound to the empty list within the
structure, use (nullo x) or (== x '()).

For the second case, look at the definition of listo in mkprelude.scm.
It uses conde; on each subsequent run the currently succeeding goal is
made to fail.

[ol...@pobox.com]

Chris Rathman wrote:
> How can I echo the value of x within the run structure? ...

> My limited and naive knowledge of scheme makes me want to use display:
>
> (run 1 (x)
> (listo `(a b c . ,x))
> (display x))
>
> but that doesn't seem acceptable to PLT scheme, as it apparently
> doesn't qualify as a goal.

Indeed, the return value of the function display is not a goal -- in
any Scheme system. In (mini)Kanren, there are only two primitive goals:
succeed and fail. All other goals reduce to these two. So, as the
first approximation, we may try

(run 1 (x)
(listo `(a b c . ,x))

(begin (display x) succeed))

Although that works, it is not terribly useful: if the logical
variable 'x' is bound, we'd like to see what it is bound to. We'd like
to `project' the variable from the domain of Scheme and Kanren values
into the domain of just Scheme values:

(run 5 (x)
(listo `(a b c . ,x))

(project (x)
(begin (display x) (newline) succeed)))

[Chris Rathman]

Ok. That gives me the answer I was looking for. Perhaps my
terminology is not appropriate for Kanren, but I see that the fresh
variable x is local to each run. Run seems to act like a continuation,
where on each iteration of run, x is fresh anew. In the Oz convention,
run acts like solve over a set of computation spaces and x is an
unbound dataflow variable that is local to the solve function. The
local part is what I was missing.

One thing I'm not quite sure of is why the listo function only returns
the second part of the pair? It would seem to me more natural to
return the completed lists. So instead of having the solution to 3.14
be:

(()
(-0)
(-0 -1)
(-0 -1 -2)
(-0 -1 -2 -3))

It would be more along the lines of

(()
(a b c -0)
(a b c -0 -1)
(a b c -0 -1 -2)
(a b c -0 -1 -2 -3))

Perhaps it's a wrong-headed question, but I was wondering why the first
set of return values was chosen over the second?

Thanks,
Chris Rathman

[Chris Rathman]

Whoops, the second solution set that I was pontificating should have
read:

((a b c)

(a b c -0)
(a b c -0 -1)
(a b c -0 -1 -2)
(a b c -0 -1 -2 -3))

Thanks,
Chris Rathman

[Chris Rathman]

Whoops, the second solution set that I was pontificating should have
read:

((a b c)

(a b c -0)
(a b c -0 -1)
(a b c -0 -1 -2)
(a b c -0 -1 -2 -3))

Thanks,
Chris Rathman

[Chris Rathman]

Probably not good form to answer myself.... but.... :-)

I missed the most obvious thing in the call to run, which is that the
second parameter is the value returned back from the call. Which
probably means that Listo returns what I had expected, but the run call
only returns the unbound tail (x).

Thanks,
Chris Rathman

[ol...@pobox.com]

regarding (run 5 (x) (listo `(a b c . ,x))), Chris Rathman wrote:

> One thing I'm not quite sure of is why the listo function only returns
> the second part of the pair?
>

> I missed the most obvious thing in the call to run, which is that the

> second parameter is the value returned back from the call. probably
> means that Listo returns what I had expected, but the run only returns
> the unbound tail (x).

Indeed, 'listo' is a function; and its return value is of the type 'o'
(which goes back to Church: please see Church's type of
predicates). However, it is more productive _not_ to view listo as a
function and _not_ to talk about what it returns. It is more
productive to view listo as an assertion: (listo [something]) asserts
that [something] is a list. The expression
(run 5 (x) (listo `(a b c . ,x)))

is better understood as a question: is there something that we can
substitute for 'x' that makes the assertion (listo `(a b c . ,x)) hold
in the domain of Scheme values? And if there is, can I have at most
five instances of these substitutions? We can see that if we replace x
with the empty list, then '(a b c . ()) is a proper list, so the
assertion (listo `(a b c . ())) holds. The assertions
(listo `(a b c . (1))) (listo `(a b c . (#f))) etc. hold as well.
Rather than enumerate all possible Scheme values, `run' has a
`short-hand'
notation: (_.0). It means one-element list that contains any Scheme
value whatsoever. When such a value is substituted for x, the
assertion (listo `(a b c . ,x)) holds. So, '(_.0) is one of the answers
the above run expression returns. It should be noted that run is not
obliged to return answers in any pre-ordained order: it's better to
think that run chooses answers indeterministically (and different
Kanren evaluators may/have indeed chose answers in different ways).