Log in

No account? Create an account
Lindsey Kuper [entries|archive|friends|userinfo]
Lindsey Kuper

[ website | composition.al ]
[ userinfo | livejournal userinfo ]
[ archive | journal archive ]

Generating tautologies with miniKanren [May. 15th, 2010|01:50 am]
Lindsey Kuper

I was catching up on Peter pmb's excellent blog earlier and noticed that he had written some code to generate a random tautology. Say, for instance, this one:

(and (not (and (not (or (or 1 1) (not 1))) (or (and (not 1) (and 0 0)) (or (or 1 1) (or 1 0))))) (not (and (and (or (not 1) (and 0 1)) (and (or 0 0) (or 1 1))) (or (or (and 1 0) (and 0 1)) (or (and 1 1) (or 0 0))))))

Tautologies represented as S-expressions? I couldn't help but think that this kind of thing is exactly what miniKanren is for, so I hacked up a miniKanren version. It produces tautologies in more or less the order you'd expect:

> (generate-tautologies 5)
(1 (not 0) (and 1 1) (or 1 _.0) (or _.0 1))

None of this is particularly thrilling -- it's what you learn on about Day Two of Logic School, probably. Still, it's kind of fun! In the example above, _.0 is miniKanren for "whatever". That is, miniKanren doesn't bother filling in the second disjunct in (or 1 _.0) or the first in (or _.0 1), because it doesn't matter what's there -- the expression is true regardless. So, that's cool.

My version doesn't do exactly what Peter's Python version does; rather than generating all the tautologies of a given depth, it will just give you the first n tautologies it comes up with, regardless of their depth. I think that generating all the tautologies of a given depth would require writing a deptho relation and using it to filter the results of true-expro.1

  1. Incidentally, all the -o and -e suffixes that show up in this code are a miniKanren convention1 meaning something along the lines of "hey, this is purely relational!"

  1. Or, you know, the closest thing to "convention" that there can be for a programming language that approximately nobody uses.

[User Picture]From: oniugnip
2010-05-15 06:30 am (UTC)
Is there a particular motivation for choosing 0 and 1 instead of #f and #t?

Just to say: in Scheme, 0 is a true value?

Also: \m/ !
(Reply) (Thread)
[User Picture]From: lindseykuper
2010-05-15 06:41 am (UTC)
I picked those to match what Peter had picked. Left to my own devices, I probably would've gone with #f and #t.
(Reply) (Parent) (Thread)
[User Picture]From: pmb
2010-05-15 02:27 pm (UTC)
Pretty neat! I don't understand the miniKanren very well - where and how is it recursing? What pattern is it matching? The "matche" bit is a mystery to me, and the (run n (q) (true-expro q)) uses a construct (run) that is entirely ungoogleable. "run scheme" "scheme run macro", etc all get you the most generic advice on how to run scheme.

Also, could you modify it to concretize all the _.0s? I found that generating both cases in the "don't cares" was actually surprisingly tricky, and it roughly doubled the length of the code I wrote.

Scheme! I am glad you liked the problem. I just submitted a paper on the tree visualization library I wrote to visualize eg. a tree automaton parsing a tautology and/or a lisp program executing and/or an AVL tree and/or the creation of a random tree.
(Reply) (Thread)
[User Picture]From: lindseykuper
2010-05-15 04:42 pm (UTC)

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)
(Reply) (Parent) (Thread)
[User Picture]From: pmb
2010-05-15 06:42 pm (UTC)
Thanks for the explanation! I now feel better that I was having trouble understanding stuff. It's pretty neat the the pattern matching can be run backwards that way.
(Reply) (Parent) (Thread)
[User Picture]From: lindseykuper
2010-05-17 06:07 am (UTC)
Running programs backwards is, in a nutshell, what miniKanren is all about. For instance, a relational type inferencer can do more than tell you the type of an expression; it can also generate all valid types.

A cool thing about miniKanren is that the implementation is tiny and invites hacking. It's an extremely thin layer on top of Scheme, just a couple hundred lines of code, and the really essential parts are on only a couple pages at the back of The Reasoned Schemer. (I can't in good faith recommend that people go buy the book, though, because mK has evolved a lot in the past few years, and the book's no longer really accurate.)

Edited at 2010-05-17 06:08 am (UTC)
(Reply) (Parent) (Thread)