Skip to main content

Brain Dump

I have a bunch of ideas that I don't have time to follow up on but I'd like to retain in some fashion so here goes.


A long time ago I had a question about the shortest assembly program (parameterised by the instruction set of course!) that could encode the generators of the quaternions under multiplication. It is a very easy thing to program this, but as I was doing it, I found myself being highly doubtful that I was choosing the "right" encoding. In fact I almost certainly wasn't. Would there not be some very tight encoding in terms of "normal" assembly language operators? This has been a persistent question in my mind that comes up frequently in different and often more general forms. If you want to make a fast compiler, how do you know what instructions to output? If you have a highlevel specification, how can you avoid the ridiculously high overhead usually associated with extremely high level languages?

Today I found this fabulous paper (from 1987!) that deals with some of the basic issues involved in finding the shortest program for a given problem. It's called "Superoptimizer -- A look at the smallest program". I'd link to it, but I got it off ACM so if you are one of the few people that has a subscription you'll know where to find it and otherwise I don't want to give the money grubbers the link-love.

Some other thoughts that are in this region of my thought-space. Can you take a given specification with a proof and systematically transform it to enumerate the space of satisfying programs? If not, why not? Even if you can't, might it not be interesting to just perform large searches of this space? Are there methods of using the transformation operators such that programs are only decreasing or minimally increasing? If so then perhaps we can call the search good at some size threshold since very large programs are unlikely to be good because of locality issues. Also Automatic Design of Algorithms Through Evolution is in a very similar vein.


Concurrency is a nasty problem. It doesn't have a nice formalism that everyone in the CS world can agree on. There must be like 500 different formalisms. All of them better (easier, not neccessarily faster) than the ones that we actually use (locking, threads, condition variables) but none of them stand out as "the right thing".

I recently found a paper called:
Socially Responsive and Environmentally Friendly Logic
. I love the title :) But aside from that, the formalism is very nice. It is something that I've contemplated a bit but never had the drive to actually try to work out formally. The basic idea comes from the knowledge that Classical Logic and Intuisionistic Logic can be viewed as 2 player games. This game is pretty simple. If I have a proof phi then to win I have to prove it. If I have a proof ¬φ, then to win my oponent has to fail to prove it. If I have φ ∧ ψ then my partern gets to pick a formula and I have to prove it. If I have ∀x then my oponent gets to pick any stand-in for x that he would like. You can probably guess the rest (or look it up). This alternate logic breaks the essential two person nature of the logic. One interesting practical feature of negation in the traditional logics, is that they give rise to Continuations in the Curry-Howard Correspondance. So what does this give rise to in the N-player games defined by Abramsky? I'm not sure, but I suspect it might give process migration! Something worth looking in to.


Popular posts from this blog

Decidable Equality in Agda

So I've been playing with typing various things in System-F which previously I had left with auxiliary well-formedness conditions. This includes substitutions and contexts, both of which are interesting to have well typed versions of. Since I've been learning Agda, it seemed sensible to carry out this work in that language, as there is nothing like a problem to help you learn a language.

In the course of proving properties, I ran into the age old problem of showing that equivalence is decidable between two objects. In this particular case, I need to be able to show the decidability of equality over types in System F in order to have formation rules for variable contexts. We'd like a context Γ to have (x:A) only if (x:B) does not occur in Γ when (A ≠ B). For us to have statements about whether two types are equal or not, we're going to need to be able to decide if that's true using a terminating procedure.

And so we arrive at our story. In Coq, equality is som…

Formalisation of Tables in a Dependent Language

I've had an idea kicking about in my head for a while of making query plans explicit in SQL in such a way that one can be assured that the query plan corresponds to the SQL statement desired. The idea is something like a Curry-Howard in a relational setting. One could infer the plan from the SQL, the SQL from the plan, or do a sort of "type-checking" to make sure that the plan corresponds to the SQL.

The devil is always in the details however. When I started looking at the primitives that I would need, it turns out that the low level table joining operations are actually not that far from primitive SQL statement themselves. I decided to go ahead and formalise some of what would be necessary in Agda in order get a better feel for the types of objects I would need and the laws which would be required to demonstrate that a plan corresponded with a statement.

Dependent types are very powerful and give you plenty of rope to hang yourself. It's always something of…

Plotkin, the LGG and the MGU

Legend has it that a million years ago Plotkin was talking to his professor Popplestone, who said that unification (finding the most general unifier or the MGU) might have an interesting dual, and that Plotkin should find it. It turns out that the dual *is* interesting and it is known as the Least General Generalisation (LGG). Plotkin apparently described both the LGG for terms, and for clauses. I say apparently because I can't find his paper on-line.

The LGG for clauses is more complicated so we'll get back to it after we look at the LGG of terms. We can see how the MGU is related to the LGG by looking at a couple of examples and the above image. We use the prolog convention that function symbols start with lower case, and variables start with uppercase. The image above is organised as a DAG (Directed Acyclic Graph). DAGs are a very important structure in mathematics since DAGs are lattices.

Essentially what we have done is drawn an (incomplete) Hasse diagram f…