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
- Incidentally, all the -
oand -esuffixes that show up in this code are a miniKanren convention1 meaning something along the lines of "hey, this is purely relational!"
- Or, you know, the closest thing to "convention" that there can be for a programming language that approximately nobody uses.
