Impromptus

Hmm. Your ideas are intriguing to me and I wish to subscribe to your newsletter.

You already have, dude. This here is pretty much it.

Sorry, my bad; I was talking to the tautology generator.

I'm intrigued that you use the defensive “if 1 == x” construction even in Python, where “if x = 1″ is a compile-time error.

I'm trying to make it automatic, so I am using it everywhere. It's a harmless thing to do in Python, and could save my bacon in Java/C/C++/etc

I must say, this has been amusing me for days http://pastie.org/940546

Now I'm wondering if Haskell's lazy-to-the-nth-degree could do some suitably amazing memoization!

Hmmm. I have a question.

Suppose we construct the recursive thingies
t -> { and(t,t) or(t,f) or(f,t) or(t,t) not(f) }
f -> { or(f,f) and(f,t) and(t,f) and(f,f) not(t) }
Then we can construct deeper and deeper tautologies by starting with “t” and recursively expanding it. Lotsa trees!

Can we encode each tautology as a finite undirected graph? If so, are these graphs downwardly closed? If so, what are the forbidden minors of these graphs? Is the answer any different in intuitionistic logic?

I am trying to imagine the resulting graphs. I got as far as making

digraph truth {    t -> andtt;    t -> notf;    t -> ortt;    t -> ortf;    t -> orft;

    f -> nott;    f -> orff;    f -> andtf;    f -> andft;    f -> andff;

    andtt -> t;    andtt -> t;    andtf -> t;    andtf -> f;    andft -> t;    andft -> f;    andff -> f;    andff -> f;

    ortt -> t;    ortt -> t;    ortf -> t;    ortf -> f;    orft -> t;    orft -> f;    orff -> f;    orff -> f;

    notf -> f;    nott -> t;}

Which dot drew as: <img src=”http://farm4.static.flickr.com/3305/4579426976_c3d8f120bb_m.jpg”>

Now I am wondering what next?

Initially, the tricky bit is encoding these tautology trees as UNdirected UNlabeled graphs…

UNdirected UNlabeled graphs, eh?

I think I could do it if we allowed self-loops. Then, I would make a leaf with a self-loop be T and a leaf without one be F. Otherwise, I think we need some encoding scheme like T should be K_3 and F should be K_4 and AND should be K_5 and OR should be C_4 and NOT should be a C_5. I could probably do it as a tree with another mapping scheme that is slightly more imaginative. If I did that, then I might be able to make things minor closed.

If a graph property of bounded treewidth is encodable in monadic second-order logic, then there exists a graph reduction system which will return TRUE if the graph has the property and FALSE otherwise. And, for all graph reduction systems, there exists a linear time algorithm for determining whether the graph has the specified property (linear time in the input graph, often exponential in the size of the reduction system – this idea helped serve as the basis for fixed parameter tractability).

I don't know if the implication goes both ways, but if it does, then we are done because I know I can construct a graph reduction system for the encoding I specified. Time to reread a paper I spent far too much time with many years ago: “An algebraic theory of graph reduction” – http://portal.acm.org/citation.cfm?id=174147.16…

This is not right. Or, more precisely, it is correct but it does not answer your question.

I see no encoding which will record only tautologies and still be minor-closed.

Cool. To me, this is exactly the sort of thing that screams out to be done with a logic programming language, so I did and wrote a little more about it at http://lindseykuper.livejournal.com/345176.html, if you're interested.

I am very interested, and will reply more there!