(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
- Incidentally, all the -
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.