Lindsey Kuper (lindseykuper) wrote,
Lindsey Kuper

Generating tautologies with miniKanren

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.
Tags: programming

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded