where and how is it recursing?
true-expro takes a Boolean expression expr, and matche does pattern matching against the four things that can be a true Boolean expression. matche contains several sets of square brackets called clauses, and the first thing that appears inside a clause is a match pattern. So, in line 21, the match pattern is just 1. I could have followed that by the word "succeed", meaning the goal that always succeeds, but it would be redundant. Likewise, I could have added a clause [0 fail], which would match the expression 0 and always fail since 0 can never be true, but there's no point in adding a clause that will never produce any answers. The (and ,expr1 ,expr2) and (or ,expr1 ,expr2) cases just recur on the sub-parts of the expression. The fun part, in the (not ,expr1), case, is that we call false-expro on ,expr1. So true-expro and false-expro are mutually recursive.
run is miniKanren syntax, and you're right that it's ungoogleable. (The best documentation, for the time being, is Will Byrd's thesis.) run provides an interface between miniKanren and regular Scheme. (run n (q) (true-expro q)) says that I want to produce a list of at most n answers. Here q is a fresh logic variable, so we're running true-expro "backwards" until we get n answers out of it. What we get back is a normal Scheme list containing what we call the "reified values" of q.
Also, could you modify it to concretize all the _.0s?
Yes! As far as I can tell, you can do that by explicitly writing out each way in which or could be true and each way in which and could be false. I just added that. It's more verbose, but you can do things like
> (generate-tautologies-concretized 10)
(1 (and 1 1) (or 1 0) (not 0) (or 0 1) (and 1 (and 1 1))
(and (and 1 1) 1) (or 1 1) (and 1 (or 1 0))
(or 1 (and 0 0)))
I hadn't tried making mK do something like that before. Thanks for the nerdsnipe!
Edited at 2010-05-15 04:51 pm (UTC)
