E-Graphs trivially in PSPACE

Some people pointed me at E-graphs, a manner for representing and then heuristically minimizing terms. Of course, Boolean circuits are terms too and minimizing circuits is PSPACE. Very much so, even.

So, it's unclear how much minimization you can actually achieve with E-graphs.

Control Flow Revisited

Two forms (b?f:g)(x) and f(b?x:y), should be enough for all (functional) control flow analysis. In a very abstract sense, application and choice are all you need.

After I commented that contification just equals hoisting on a small example someone on the interwebs made a smart comment that 'f' cannot be hoisted in the following example but can be contified.

let f = fun arg -> body in 

match thingy with 

| A -> f x 

| B -> f y 

| C -> g foo

Of course, you just need a rewrite to a term that uses b0? f(b1?x:y) : g foo to see that 'f' is still hoisted. But it won't be pretty so that's an issue.

NAND rewriting

I think somewhere between '01 and '04 I was interested in SAT problems. At that point in time there was an unoutspoken vibrance in the field that NP problems might be tackled.

At that time I concentrated on NAND, or Sheffer stroke, rewriting. I figured if people were close to breaking some barrier then there should be some rewrite strategy to a solution that didn't suffer from exponential blowup during the path.

NAND terms are beautiful little mathematical expressions and the rewrites I came up with had pleasant forms so I wrote several small programs.

One of the things I stumbled upon was a 3SAT formula after I looked for a while at the truth table for NAND.

x y z
0 0 1
0 1 1
1 0 1
1 1 0

Every row has at least one zero (-x+-y+-z), and certain pairs have at least one one (x+z) and (y+z).

I checked the conjunction and realized I had a linear translation from circuits to 3SAT.

Meanwhile, I was reading satlive.org and noticed that people were unaware of that and posted the solution there thinking Armin Biere would at least pick it up.

Years later I learned I had rediscovered a solution from Tseitin from the sixties or something, years before SAT solvers became relevant. Nowadays I think everyone who studies the problem a bit would've come up with it.

The NAND rewriting strategy never panned out, stuff kept exploding. Moreover, rewriting is extremely slow in comparison to cheaply manipulating arrays in what is very fast (learning) local search.

I can still somewhat rewrite NAND terms in my head or play pebble games on them, but that doesn't seem to be a marketable skill.

But, ah well, I comfort myself that I was in the good company of Knuth who, for at least a while, thought that P=NP.