Andrew Birkett's blog

I bought a textbook on fluid mechanics recently, having a rough plan to learn more about weather patterns by writing a simulation. Expecting a theoretical physics text, I was a bit unsettled to read the following on the first page of the introduction:

“The theory is often frustrating”

“viscocity .. gives rise, at frustratingly small velocities .. to turbulence”

“The theory of turbulent flow is crude .. yet it can be quite serviceable as an engineering estimate”

Crude? Frustrating? “Engineering estimate”? These are not words I’ve ever read in a book about theory before. I’m a bit scared!

About fifteen years ago, I attended a talk by Roger Penrose at the Edinburgh Science Festival on the topic of Gödel’s incompleteness theorem. After Penrose finished delivering the talk, an elderly gentleman in the audience stood up and said that he didn’t really see what the fuss was about. You shouldn’t worry, he asserted, that it’s been shown that every formal system has a ‘tricky’ statement (ie. true but not provable). Chances are, it’s not a very interesting statement. And, besides, if you really cared about it, you could just extend your formal system to assert that it’s true. “Ahh”, said Penrose, “but now that new system you’ve created will have it’s own unprovable statement!”. The elderly gentlement was not impressed. “Well then”, he said, “I’d just add a new rule to that one too!”. Penrose noted that the augmented system would suffer the same incompleteness fate, but the elderly gentleman was prepare to keep adding more rules for as long as it took, and the session briefly descended into farce.

At the time, I thought the guy was missing the point. After all, it’s the incompleteness of any given formal system which matters – patching the formal systems with duct tape moves the goal posts but doesn’t let you escape the problem.

But, with a more engineering mindset on today, what he said seems quite reasonable. Most of the time, the incompleteness or undecidability of a formal system doesn’t stop you doing lots of interesting things with it. I don’t worry about the halting problem when I start up firefox, and my high school maths teacher seemed unconcerned that my homework submissions might contain a true-but-unprovable statement. I’m also reminded of a quote I read a long time ago in a paper about the dependently-typed language, Cayenne:

“So type checking Cayenne is undecidable. This is unfortunate, but unavoidable for a language like Cayenne. How bad is it in practice to have an undecidable type checker? This question can only be answered by practical experiments. The Cayenne programs we have tried to date range from ordinary Haskell style programs, to programs using dependent types, to proofs of mathematical propositions. The total size of these programs are only a few thousand lines, but so far the experience shows that it works remarkably well.

Having undecidable type checking means that the type checker might loop. This is clearly not a user friendly type checker. So instead the implemented type checker has an upper bound on the number of reduction steps that it may perform. If this limit is exceeded the type checker will report this. Most of the type errors from the Cayenne compiler are similar to those that any other language would give. Very infrequently does the type checker report that it did not terminate within the prescribed number of steps. Most often, this is the result of a type error, but sometimes the type expression is just too complicated and the number of reduction steps must be increased (the number of reduction
steps is a compiler arg).”

Anyhow, to come full circle, the reason that I remember all this tonight is that I just found out that Alan Turing’s thesis was on exactly the topic which the elderly gentleman was riffing on. In essence, what happens when you keep patching your formal system, Wily Coyote stylee, to build an ACME infinite series of formal systems, each a litle bit better that the one before? I have not read the thesis yet, but I found it amusing to note that, with hindsight, the eldery gentleman from fifteen years ago was onto something!

This weekend I built a weaving loom.

This all started because I was thinking about the recursive structure of knitting – in knitting, each loop of wool is pulled through another loop, except the first row (the base case!). Anyhow, it occurred to me that knitting is inherently sequential (and therefore slow) whereas machine knitting and weaving are parallel in the sense that, with one ‘swoosh’, you create lots of stitches. Parallel = good.

Before building a loom, I tried just stringing wool around a bit of cardboard and weaving around those. It works, but is slow because you have to go above and below each string manually. But it worked well enough to merit spending some time building a “proper” loom. The loom I built has a cunning mechanism to lift alternate sets of strings en masse, allowing you to just whoosh the wool through the middle. This makes weaving much faster. I can see lots of way to improve the loom, but given that it took less than an hour to build, at a cost of about 1UKP, I’m pretty pleased.

One thing I enjoyed about this mini-project is the rapid feedback/innovation cycle. I’d use the loom for a few minutes, learn what the limiting factor was. Then I’d get the tools out, build a different part, and try it out. Each improvement to the loom make a huge difference to weaving productivity.

Shame I’m about 250 years too late!

Lately, I’ve been working on another eclipse extension. This one generates equals/hashcode methods which use the commons-lang HashcodeBuilder and EqualsBuilder (in non-reflection) mode. So, a single keypress will provide equals/hashcode methods which cover all non-static fields, plus sort out the import’s required.

After writing this, I found commons4e, which has the same aim. Actually, I still prefer my own because it’s optimized for the common case. I don’t like fluffy dialog boxes which let you choose exactly which fields to include. Just generate the code for all the fields, and use normal editing commands to get rid of the ones you don’t like.

Writing my own has helped me learn more about the eclipse api’s (and the lack of quasiquoting), and this should hopefully lead onto more complex things being possible.

In an attempt to further harass postscript printers, I hacked the postscript l-system which I wrote, err, a long time ago, so that instead of trees it draws hilbert curves. Then it occured to me to animate it, starting from a straight-ish line, and gradually folding it in, increasing the turn angle until it reaches 90 degrees. Kinda pretty. Makes me wonder how long the piece of string gets when it’s straightened out; might hack the postscript file to tell me that later.