Exceptional Objects

One of my favourite topics in mathematics is the existence of exceptional objects. There have been many articles written on the web about this subject - particularly by John Baez. But I recently came across this article by John Stillwell, in American Mathematical Monthly, that also gives a historical perspective. The connection with classical geometry - Desargue's theorem and Pappus's hexagonal theorem - was also new to me.

Very briefly: mathematics is full of classification theorems. What frequently happens is that objects of a certain type are classified into a bunch of series with a handful of exceptional objects left over. For example the simple finite groups have all been classified and besides the series (such as the cyclic groups of prime order) there are 26 'sporadic' simple groups such as the Monster. The classification of compact Lie groups gives a similar pattern and even the classification of regular polyhedra is similar. Bizarrely, exceptional objects from different branches of mathematics are often related to each other. In fact, the entire classifications from different branches of mathematics are often closely related. And for some reason Dynkin diagrams and octonions seem to play a special role in many of these classifications. The article suggests that the octonions are the "mother of all exceptional objetcs". Anyway, read the article for more information.

I also found this article by the same author on the history of the 120-cell, one of those exceptional regular polyhedra.

Quantum Mechanics and Probability Theory

I've been spending a bit of time thinking about quantum mechanics as an 'exotic' probability theory. It's actually very easy to view quantum mechanics this way and what interests me more is figuring out exactly how quantum mechanics differs from conventional probability theory.

Quantum mechanics looks just like probability theory with a slight twist. Instead of assigning probabilities to events you assign 'amplitudes' which are complex numbers. Computations with these amplitudes are carried out very similarly to computations with probabilitites. If we use a() to mean 'amplitude' a(A or B)=a(A)+a(B) and a(A and B)=a(A)a(B) under similar conditions to those in which P(A or B)=P(A)+P(B) and P(A and B)=P(A)P(B) in conventional probability theory. But these rules for a() only apply when the events A or B remain 'unobserved'. When we actually make observations we switch to a different rule where we now assign probabilities using the rule P(A)=|a(A)|² and these probabilities can be given your favourite probabilistic interpretation.

One interesting thing we can do is recast conventional probability theory so that it looks more like quantum mechanics. For example, consider coin tossing with two outcomes, H and T. We can use these states as the basis for a 2D vector space and write them as |H> and |T>. The outcome of a fair coin toss can be written as 0.5|H>+0.5|T>. When we come to 'observe' the coin its state vector 'collapses' to |H> or |T>. Suppose we have two such coins. Then the joint state space is the tensor product of the state spaces for individual coins. The rule for combining two independent coins into a joint state is the ordinary tensor product. So combining two fair coins gives the state (0.5|H>+0.5|T>)⊗(0.5|H>+0.5|T>)=0.25|H>|H>+0.25|H>|T>+0.25|T>|H>+0.25|T>|T> which can be interpreted as giving the usual probability assigments for fair coin tossing. If we couple the coins together on some way then the joint state might not be a product of individual coin states, ie. we might no longer have independence and their states would be 'entangled'.

Consider a physical process applied to the tossed coin. For example suppose we have a machine that always turns a head over to reveal a tail but only has a 50% chance of turning over a tail. We can think of this as a linear operator mapping |H>→|T> and |T>→0.5|H>+0.5|T>. In this formalism any physical process must be a linear operator given by a stochastic matrix.

Anyone who has studied a little quantum mechanics will recognise many of the phenomena above: the tensorial nature of joint systems, the linearity, the entanglement, the 'collapse' of the state on observation and so on as being nearly identical to features of quantum mechanics. So contrary to popular opinion I think I believe that whatever is interesting about quantum mechanics has nothing to do with any of these features. You can even shoe-horn a variant of the many worlds 'interpretation' of quantum mechanics into probability theory by insisting on the primacy of the state vector and pointing out that when a coin is observed the observation is described by a linear map defined by |H>→|H>|Observer sees H> and |H>→|T>|Observer sees T>.

But almost everyone agrees that quantum mechanics is weird. So how does it really differ from probability theory?

The biggest one is the feature called 'destructive interference'. In conventional probability theory we can combine two states together to make a new state. For example suppose process A generates state |A> and process B generates state |B>. Then we can choose to run either A or B with 50% probability resulting in a new state |C>=p|A>+(1-p)|B>. Suppose A and B are coin states. Then the probability of getting a head when observing state |C> is bounded between the probabilities of getting a head in states A and B. This is a kind of convexity condition. If processes A and B are both roughly fair there's no way of choosing p to 'refine' these states to make another one that's more unfair. And here's the big difference from quantum mechanics. In QM we can choose p to be negative (or any other complex number) and escape from this convexity condition. If we have a quantum coin toss, say |A>=0.6|H>+0.8|T> and |B>=0.8|H>+0.6|T> (in QM the sums of the squares of the moduli are one, not the sums themselves, that's why I chose 0.6 and 0.8), then we can combine them into |C>=-12/7|A>+16/7|B> and get a pure |H> state. We have made the |T> terms cancel out. This is an example of destructive interference. (How do we actually carry out this linear map for arbitrary complex numbers? It's actually very easy - see below.)

One very curious consequence of the above is that we can't ignore low amplitude outcomes. Classicaly, suppose |A>=sqrt(1-e)|H>+e|T> and |B>=sqrt(1-f)|H>+f|T>. If e and f are small enough then no matter what linear combination of |A> and |B> we use to make |C> we can choose to ignore the possibility that we have a head. But in QM, suppose |A>=sqrt(1-|e|²)|H>+e|T> and |B>=sqrt(1-|f|²)|H>+f|T>. Then be carefully crafting |C> from |A> and |B> we can make the probability of getting heads as high as we like.

It's destructive interference that underlies many of the interesting phenomena of QM. For example Shor's factorisation algorithm exploits destructive interference to remove those parts of the quantum computer state that give the wrong answer leaving us with an output that represents a factor.

Non-convexity also leads to other significant consequences. In conventional probability the basis elements |H> and |T> are 'special'. They lie at the extreme 'corners' of the space of possible states and can't be written as stochastic combinations of any other states. But for a quantum coin toss we've shown above that there is no special basis. The state |H> can be written as a linear combination of |A> and |B> just as easily as |A> can be written in terms of |H> and |T> and this is reflected in the fact that we can make a machine that combines |A> and |B> states to make an |H> state. In fact, this is straightforward to observe in the lab. Instead of considering |H> and |T> consider |+> and |-> which correspond to spin up or down states for an electron. Amazingly, if you rotate this state through 90 degrees to make a "spin left" state might get something like (|+>-i|->)/√2. (That answers the question I asked above, just rotate the system.) There is no conventional analogue of this. It is this that is the central problem with Schrödinger's cat. Many people think the problem is that the cat's state becomes something like (|alive>+|dead>)/√2 and can't figure out how to assign meaning to this. But this isn't an issue for QM at all, you can formalise conventional probability so that the cat is described by such a vector and nobody has any difficulty with that. The issue with the Cat is that when the cat is observed it appears to 'collapse' into either the state |dead> or |alive>. Why these two basis elements? In conventional probability these vectors are special. But in QM they are no more special than other vectors.

So in summary - I think that entanglement, wave function collapse and a whole host of other phenomena that are presented as specifically quantum phenomena are nothing but irrelevant distractions and aren't specific to QM at all. The interest value in QM comes from non-convexity and the important problem to solve is the preferred basis problem. (There's also the possibly unanswerable philosophical question of why in Heaven's name the universe looks like a stochastic system with complex numbers for probabilities? And if you're a Bayesian, in what way can a complex number possibly be interpreted as a degree of uncertainty?)

Two Kinds of Mathematics

A recent comment by augustss made me realise that I mentally classify mathematics into two different kinds. I wonder if other mathematicians do the same - so here's your chance to post a comment saying whether or not you agree.

It seems to me that mathematical theorems are either structural theorems or content. By structural I mean that they set up some machinery and show that the machinery does what we expected it to do, and content refers to 'surprising' facts about the mathematical universe. (I think 'structural' is a good choice of word here. 'Content' doesn't feel quite right but the best I could come up with.)

For example, think about a subject like algebraic topology. We start by learning about point set topology. We might define the product topology and then from that show that the projections from the product space to the original space are continuous. These are structural results. They simply tell us that we've defined the product topology in the right way, and the reason why they are the right way is that someone wanted to do topology on the cartesian product of sets and thought hard until they found a way to make this work. They (probably) didn't make a discovery like - hey, there's this amazing topology on the cartesian product that gives continuous projections. They set out to make the product topology in order to prove other stuff, like the way a silversmith or a computer scientist might make tools for themselves for a particular application.

On the other hand, people later started discovering bizarre properties of homotopy groups of spheres. Consider the Hopf fibration which is a beautiful way of building the 3-sphere out of 1-spheres. This was a genuine discovery. It's not just a trivial consequence of the topological machinery but a new result that wasn't plugged in from the beginning. That's what I mean by content.

You invent mathematical machinery, prove structural theorems about it which shows that it does what you want, and then you start discovering interesting results with the machinery. Most branches of mathematics have a mixture of both types of result. In group theory you might prove structural results like the isomorphism theorems which really just show that quotients are what you think they should be. And then you start discovering content like the fact that A_n is simple for n≥5.

Structural theorems tend to be more universal and feel more 'invented'. Content theorems are more specific and feel more 'discovered'. And I'm really talking about a spectrum rather than a binary classification.

Most branches of mathematics have a mixture of the two types of theorem. Typically the structure theorems are used as a tool to discover content. In some sense the content is the end and the structure is the means. But category theory seems different in this regard - it seems to be mainly about structure. Every time I read category theory I see ever more ingenious and abstract tools but I don't really see what I think of as content. What's hard in category theory is getting your head around the definitions and often the theorems are trivial consequences of these. For example consider the Yoneda lemma as described here. This is a pretty challenging result for beginning category theorists. And yet these notes say: "once you have thoroughly understood the statement, you should find the proof straightforward". This exactly fits with what I'm getting at: the theorem is an immediate consequence of the definitions and the proof essentially shows that the machinery does what you'd expect it to do.

Computer science (at least the more formal parts) is a lot like structural mathemtics. It's about inventing machinery (lambdas, coalgebras, state machines) and then proving that machinery does what you expect (diamond property of reductions in lambda calculus etc.). If we compare with group theory the differences become apparent. A mathematician might consider groups in general (general machinery), specialisations of groups such as rings and fields (more machinery) and then specific groups like the Monster or the alternating groups (content). A computer scientist will look at things like untyped lambda calculus, untyped lambda calculus, lambda calculus with this or that extension, but they tend not to look at specific instances in the way that there are specific groups.

Very rarely there is a content theorem that follows from the structural theorems about the tools of computer science. Here's one. 7 binary trees are isomorphic to one. This is a really neat bit of content. This isn't a direct consequence of the definition of trees. When trees were invented nobody thought "what structure can I invent that captures the notion that 7 of them is isomorphic to just one?". This is a discovery, a new result that wasn't plugged in from the beginning.

I guess there is another way to view category theory. As it is the mathematics of structure then in a sense the structure of other branches of mathematics is the content of category theory. It's probably fair to say that one person's content may be another person's content. But it's not unusual for a lecturer to say of their course "the first few weeks will be spent setting up the definitions and machinery and then we'll get onto the real content..."

And now I can reply to augustss. "Real mathematics" is mathematics where from time to time you prove content. And the reason why I said "it's time to get back to some real mathematics" is that much as I've been enjoying computer science lately, I need to see some non-structural content from time to time.

Monads Without Types

People who have just implemented interpreters and compilers are like people who've just had babies - they become monomaniacs incapable of talking about anything else, and showing you their latest pictures at any available opportunity. But I'm going to spare you the pictures. (Hmmm...does blogger.com support the classification of posts by type?)

My typeless pure functional lazy call-by-name language seems to be working out quite well so I thought I'd talk about two aspects of it:

Firstly: my goal has been to construct something as simple as possible that is as powerful as possible. I've basically got it down to just five instructions: push an integer onto the stack, push a pointer to a function, push a duplicate of the nth item down on the stack, push a closure and tidy up a stack frame. Those 5 instructions are then translated into C. Everything else is provided by libraries (eg. plus, minus, seq) or is part of the runtime (ie. garbage collector and the loop that decides which reduction to perform next). The core compiler is basically ten lines of code - the other 300 lines are mainly the parser that has to deal with the quirkiness of any Haskell-like syntax. Yet with this tiny compiler that compiles to just these five operations I've found it possible to write things like a monadic parser, implement monad transformers, and do simple logic programming using the list monad. I'm astonished by how far you can get with so little programming. The moral is, starting from next to nothing you get a lot more bang for your buck with functional programming. (Sometimes it even competes tolerably, performancewise, with Hugs).

Secondly: I thought I'd mention my handling of monads. The compiler only supports three types - integers, pairs and functions so we have no type inferencing tricks to generate the glue to make monads as easy to use as they are in Haskell. Nonetheless I eventually figured out a way to make monads almost as painless as in Haskell. There were two things I needed to do:

(A) Redefine the semantics of " {" and "}". In Haskell anything between "do {" and "}" is glued together using the bind function where bind is overloaded. What I did was similar. Anything between "{" and "}" is glued together using a function. But I don't use the bind function. Instead I define "{ <statements> }" to be a function that uses its argument to bind the statements together. It's then easy to define something like:

do f = f bind.

and we end up with code that looks like Haskell's again. Unfortunately this definition is only useful in the presence of polymorphism because it commits us to using the global 'bind' function. So the way to deal with this is to

(B) Reify monads. I simply define a monad to be the pair (bind:return) where bind and return are the bind and return funtions for the monad. (I use ':' to define pairs as in my language non-null lists are simply pairs constructed form the head and tail of the list.) I can then define do as

do monad f = f (head monad).
return monad = tail monad.

So now the price I have to pay for the lack of types is just that I have to parameterise uses of do and return with the monad. This isn't too onerous, for example you get code looking like:

putLine l = if l then
                    doIO {
                        putChar (head l);
                        putLine (tail l)
                    }
                else
                    returnIO 0.

where I've defined doIO = do IO etc.

It gets a little more complex with monad transformers. As monads are reified, a monad transformer in my language is an actual function that maps a monad to a monad. For example, here's part of the definition of the StateT monad transformer:

returnStateT monad x s = return monad (x:s).
bindStateT monad m k s = bind monad (m s) (\as -> k (head as) (tail as)).
doStateT monad f = f (bindStateT monad).
-- Actually construct the transformed monad.
StateT monad = bindStateT monad : returnStateT monad.

In some ways these definitions are actually simpler than the corresponding Haskell definitions. In Haskell you communicate information to the compiler about which bind and return to use by your choice of type. So you find yourself repeatedly wrapping and unwrapping objects (eg. using runStateT). No such issue here, a sequence of statements in the state monad can simply be applied immediately to the input state.

Anyway, the monad transformer examples I came up with earlier now carry over to my new language like so:

prog = do (StateT State) {
            liftStateT State (modify (plus 1));
            a <- liftStateT State get;
            modifyT State (plus 10);
            b <- getT State;
            liftStateT State $ put (a+b);
            c <- getT State;
            return (StateT State) $ c+1
       }.

Note that I chose to make everything explicit. I could easily have made local definitions like lift = liftStateT State to make things look more like Haskell.

Anyway, I'm pretty pleased. With a few hours of coding here and there over a period of two weeks I've written my first compiler of standalone executables in 20 years and it's already at the stage where it wouldn't be hard to port its own compiler to itself. (My previous compiler was an adventure game DSL written in BASIC and based on the one here (though I don't think the acronym 'DSL' existed then). I also implemented Forth on a Psion II a bit later but it's debatable whether you'd call indirect threading by the name 'compilation'.)

I'll probably put a release on my web site some time in the next week. Not that it's actually useful for anything...

And all this computer science is too much. I really must get back to some real mathematics some time soon...

Writing a pure functional lazy call-by-name compiler

There are lots of minimal functional language/lambda expression evaluators out there, so instead I thought I'd write one that actually compiled to standalone C. But by accident it seems to have grown and I now have a 'typeless' Haskell, or at least a language with ML type grammar, lazy evaluation and call-by-name, primitive monad support and only two types - integers and lists. I'm now at the stage where I can compile pieces of code like this:

return a s = a : s.
bind x f s = let vs = x s in seq vs ((f (head vs) (tail vs))).
bind' x f s = bind x (\a b -> f b) s.

contains x = if x
               (if (head x==81) 1 (contains (tail x)))
               0.

getLine = do {
           c <- getChar;
           if (c==10)
                 (return 0)
                 do {
                   l <- getLine;
                   return (c : l)
                 }

          }.

putLine l = if l
               do {
                   putChar (head l);
                   putLine (tail l)
               }
               (return 0).

prog = do {
           a <- getLine;
           if (contains a) ( do { putLine a; putChar 10 }) (return 0);
           prog
       }.

start = prog 666.

This piece of code does the same as "grep Q" and amazingly doesn't leak memory and could probably outrun a snail (just). When I tidy it up and fix the bugs I'll release the compiler on my web page.

It's been one hell of a learning experience. The main thing I've learnt is that those compiler writers are damn clever people. But I also learnt other things like: even the most innocent looking expressions can gobble up vast amounts of memory in a lazy language, it's really heard to debug lazy programs even when you have complete freedom to make your compiler emit whatever 'instrumentation' you want, garbage collection is more subtle than I thought and Haskell has a weird grammar. On the other hand, some things were easier than I expected. Dealing with lambda expressions looks hard at first - but lambda lifting is very easy to implement so that once you have a way of compiling equations, lambdas come for free. And ultimately it's incredible how much stuff you can get for nothing. The core compiler is miniscule - it knows how to compile one operation - function application. The rest is syntactic sugar or part of the library that the C code links to.

My ultimate goal is to get my compiler to emit self-contained C programs that are as small as possible. I'd like to take these programs and make them run on a microcontroller like the one in this robot I built last year. It has 1K of RAM, 8K of program space and runs at 8MHz, which may be enough for a simple light following algorithm. (In assembler it'd be about 100 bytes long and use 2 or 3 bytes of RAM.) I don't want to actually achieve anything useful - I'm too much of a mathematician to want to do that. I just want to construct an example of what I see as an extreme form of computational perversity: a pure language with no side effects having actual side effects in the physical world.

Grok Haskell Monad Transformers

Another literate Haskell post:

I've tried a few times to read various documents on the web about
Monad Transformers in Haskell. I think that in almost every case the
authors are trying to show how clever they are rather than explaining
their use. If I had just seen the simplest possible examples of Monad
Transformers at work I would have been able to figure out what was going
on and that would have given me enough information to bootstrap myself
into Monad Transforming enlightenment.

So to save other people the trouble I went through I'm providing you
with examples of Monad Transformers at work. I'm not even going to
explain in detail how they work, they're close to self-evident once the
main features are pointed out.

> import Control.Monad.State
> import Control.Monad.Identity

Firstly here are two examples of the use of the State Monad. This
code isn't intended as a tutorial on the State Monad so I won't
explain how they work.

> test1 = do
>             a <- get
>             modify (+1)
>             b <- get
>             return (a,b)

> test2 = do
>             a <- get
>             modify (++"1")
>             b <- get
>             return (a,b)

> go1 = evalState test1 0
> go2 = evalState test2 "0" 

Note how evalState 'unwraps' the State Monad and gives you back the
answer at the end.

So the question is: how do I combine both of these states into one
so that I can update or read either the integer or the string state
at will? I could cheat and make a new state of type (Int,String)
but that isn't a general solution.

The idea is that you use a Monad Transformer. A Monad Transformer
if like a layer of onion peel. You start with the Identity monad
and then use Monad Transformers to add layers of functionality.
So to get a two-state monad you take the Identity and add two
layers of stateness to it. To get the answer at the end you need
to unwrap the State layers and then unwrap the Identity layer too.

When you're inside your 'do' expression you need a way to choose
which Monad you're talking to. Ordinary Monad commands will
talk to the outermost layer and you can use 'lift' to send your
commands inwards by one layer.

The following should now be self-evident:

> test3 = do
>     modify (+ 1)
>     lift $ modify (++ "1")
>     a <- get
>     b <- lift get
>     return (a,b)

> go3 = runIdentity $ evalStateT (evalStateT test3 0) "0"

Note that we use evalStateT to unwrap the State layer instead
of evalState. evalStateT is what you use to unwrap one layer
of the Monad. evalState is what you use when your entire Monad
is just the State monad. When State is a layer, rather than
the whole thing, it's called StateT. (Try :type go3 in ghci.)

What if you want to combine IO and State? For various reasons
the IO monad must form the innermost core of your onion so
there's no need to wrap an IO layer around the Identity,
you can just start with IO. And when you unwrap you don't
need to unwrap the IO layer because the Haskell compiler does
that for you. (Now you can see why you can't layer IO, you're
not supposed to unwrap IO as it's the job of the code that
calls main at the top level to do that.)

So here we go:

> test5 = do
>     modify (+ 1)
>     a <- get
>     lift (print a)
>     modify (+ 1)
>     b <- get
>     lift (print b)

> go5 = evalStateT test5 0

At this point you might be suspicious that IO is being handled
slightly differently from State. So here's a StateT layer
wrapped around State:

> test7 = do
>     modify (+ 1)
>     lift $ modify (++ "1")
>     a <- get
>     b <- lift get
>     return (a,b)

> go7 = evalState (evalStateT test7 0) "0"

You can probably safely ignore my comments and crib the code above
directly for your own use.

And credit where credit's due: I found the following link to be
more helpful than any other in trying to figure this stuff out
http://www.cs.nott.ac.uk/~nhn/MGS2006/LectureNotes/lecture03-9up.pdf
(But I still felt that this link was obfuscating.)

You may now be wondering where test4 and test6 are. So am I.

Update: I just figured out that you don't always need to use the
'lift' operation. Some of the Monad Transformers have been defined
so that the commands will automatically be passed into the inner
Monad (and further) if needed. I think it's slightly confusing to
write code this way, however.

The Most Amazing Development Environment Ever

The latest version of Graham Nelson's Inform compiler for writing interactive fiction (aka text adventure games). By strange coincidence I was just getting back into Trinity (almost finished it) and was toying with playing with interactive fiction myself. This environment seems like a real pleasure to use and to get an idea of why this is so amazing, here is some actual compilable code:

The Dining Car is a room. Lord Peter is a man in the Dining Car. Sherlock Holmes is a man in the Dining Car. Miss Marple is a woman in the Dining Car. Adam Dalgliesh is a man in the Dining Car.

Suspecting relates various people to one person.

The verb to suspect (he suspects, they suspect, he suspected, it is suspected) implies the suspecting relation.

Dalgliesh suspects Holmes. Holmes suspects Lord Peter. Lord Peter suspects Holmes. Miss Marple suspects the player.

Exculpating relates one thing to various people.

The verb to exculpate (it exculpates, they exculpate, it exculpated, he is exculpated) implies the exculpating relation.

The silver bullet exculpates the player. The pipe ash exculpates Holmes. The poison pen letter exculpates Lord Peter. The poison pen letter exculpates Miss Marple. [Poor Dalgliesh. I guess he did it.]

The pipe ash, the letter and the silver bullet are carried.

and here is some more

The Oval Office is a room. Josh and Toby are men in the Oval. A height is a kind of value. 5 foot 11 specifies a height. A person has a height. Josh is 5 foot 8. Toby is 5 foot 10.

Height guessing is an action applying to one thing and one height. Understand "guess [someone] is [height]" as height guessing.

Check height guessing: if the noun is not a person, say "You can only guess the height of people." instead. Carry out height guessing: if the height of the noun is the height understood, say "Spot on!"; if the height of the noun is greater than the height understood, say "No, [the noun] is taller than that."; if the height of the noun is less than the height understood, say "No, [the noun] is shorter than that."

Test me with "guess josh is 6 foot 3 / guess josh is 5 foot 9 / guess josh is 5 foot 3 / guess josh is 5 foot 8".

As one might expect from Graham Nelson, it is fully (dare I say, literarily) documented and the error messages are the most verbose (as in useful and readable) error messages I have ever seen from any compiler.

The Solar Corona Problem

It's all been a bit abstract a bit lately. So I thought I'd bring things down to Earth a bit. But only metaphorically speaking.

I've decided to volunteer some time at the Chabot Space and Science Center. I'll mainly be manning their 20" reflector pictured here:



Basically I'll be something like a tour guide for visitors, answering any questions they may have. Only during daylight hours for now. It's a good excuse to read up a little on astronomy and if I stick at it then one day I'll be qualified enough to work the telescope at night, and maybe even catch a few photos through it with my own camera.

Anyway, one of the visitors was asking about the temperature of the Sun. As any photographer can tell you, the surface of the Sun has at a temperature of 5800K. But observations during eclipses show that the corona has some pretty weird spectral emission lines that correspond to atoms at very high temperatures, of the order of a few million K. Strangely, this is a bit of a mystery. At first you might think what's the problem? There's a gigantic fusion reactor with something like 2×10³⁰kg of fuel burning right next to it. But the problem is this - how is that energy getting to the corona when the surface of the sun is at 5800K. As everyone knows, heat doesn't generally flow from a cooler region to a hotter one. To me this is much more interesting than the Solar neutrino problem. Neutrinos don't play a large part in anyone's lives and all of the evidence that there is even a problem rests on indirect evidence and theoretical work. But the solar corona problem is pretty immediate. You can literally see the temperature of the sun's surface and the anomalous high temperature emission lines require nothing more abstract than spectrography. When a visitor asked about this I had no answer so I decided to read up on the issue.

Turns out there are a few possible explanations, though none of the corresponding predicted physical proceses have been directly observed yet. My money is on Alfvén waves. These are essentially waves that form solutions to the combined Maxwell and Navier-Stokes equations. If you imagine wave travelling down a whip when it is cracked, all that enerfy gets to the end of the whip and gets concentrated in the tip resulting in it moving at supersonic speeds. Something similar may be happening with these waves. They proceed out from the sun but when they get to the corona there's nowhere for the energy to go except into heating it to incredible temperatures.

Anyway, next time someone asks about the corona I won't be telling them this. Most people don't want this much detail and even if they did, they have impatient kids with them. But it's good to have people prodding me to read up on interesting physics.

Zog, The Devil and Me.

Zog runs a casino on the planet of Vega Sals. Like his competitors on the galaxy-famous Landing Strip he's been using probability to estimate his earnings based on the odds that he offers in his games. It needs quite a bit of care - offer odds that are too good and he'll lose the games, offer stingy odds and his competitors undercut him.

Anyway, Zog decided to attend some adult education classes at the local university and learnt about the concept of falsifiable propositions. The effect was disastrous, he found that he couldn't attach a meaning to the statement "this coin has a 50% probability of turning up left-head". (Note that the inhabitants of Vega Sals have two heads.) Whether it turns up left-head or right-head it's consistent with the original statement which can never be falsified. Yet surely it has a meaning of some sort.

Zog wrestled and wrestled with this problem, suffering nights of insomnia, when suddenly in a flash of smoke the Devil appeared in front of him.

"I'll do a deal with you," he said. "You're struggling because you can't get a falsifiable proposition from a probabilistic one. So here's what I'll do for you. Whenever you want, I'll let you convert a probabilistic statement into a falsifiable one with probability one.". "

"Sounds great," replied Zog, "but what's the catch?"

"Hmmm...I see my reputation precedes me. Anyway, it's just a small catch. For every proposition that I convert you'll have to suffer the fires of Hell. If it's an unlikely proposition you might suffer for trillions of years. But if it's 90% likely you'll only have to suffer, oh, let's say a billion years. If you can make it 99.99% likely you might only suffer for a million years but if you make it something like 99.9999999% likely you'll only have to suffer a short while. I have a brochure here that explains the details."

"Sign me up right away," said Zog, and he slept well that night.

But the next day when Zog was doing the weekly profit and loss forecast he found he had a problem. If he had a thousand people play space-roulette that day then it'd cost him trillions of years of sufffering to make the outcomes of these games certain. In the cold light of day he seemed no better off than before. But then he had an idea. Why not batch together the days takings? Instead of predicting the outcome of one game he would predict the outcome for the entire day. By using a suitable variant of the central limit theorem he found that he could predict the day's winnings to within 10 galactic credits with 99.9999% certainty. "Great!" he thought looking this up in the brochure. "99.9999% - 3 days of Hellfire." As the Astro-Priest had told him that even one second in Hell was worse than a lifetime of suffering it didn't seem such a good idea after all.

So Zog decided to consult a mathematician to buy a theorem. "I can construct just the thing you need," the mathematician said, "for only 1000 galactic credits." So the mathematician sold him a theorem a bit like this: "if, over the course of your lifetime, you make your decisions based on probability theory, then you have a 99.999999999% chance that you won't make a total loss at your casino tables and that nobody else will undercut you." The cunning mathematician had taken Zog's batching trick and batched together the entirety of Zog's future transactions to make this prediction. It was a perfectly valid theorem and Zog thought it was money well spent. He also no longer needed to worry about the meaning of probabilistic statements. He knew that if he just used probability theory, instead of thinking about its meaning, he would be guaranteed to succeed in the casino business.

And Zog lived happily ever after. When he died, the hundredth of a second that he suffered in Hell was pretty bad, but the everlasting happiness that came afterwards more than made up for it.

Of course you're probably getting suspicious by now. There isn't really such a place as Vega Sals. And I just made up Zog. This is of course a fable. The truth of the matter is that it was me who made the deal with the Devil, not Zog. And it wasn't exactly this deal. The deal I made is based on the theorem that I got for free from here. The Devil said that any time there was a system whose wavefunction was ψ he could make it φ where the amount of suffering I would have to endure was computed from |ψ-φ|. Using that theorem I was able to get the devil to remove from the universal wavefunction that part in which the probabilities of the Copenhagen interpretation didn't work. It was a pretty small part so I should suffer even less than Zog did. And the Devil offered me a 50% discount if I blogged aobut how good my deal was.

But I'm not the only person who's made such a deal with the Devil. Another person is David Deutsch in this paper. But I feel a little sorry for David. You see he claims "we have proved that a rational decision maker will maximise the expectation value of his utility." Well, yes, this is true. But only because of how he's defined 'rational'. But by using sleight of hand he's made it appear as if this statement is true for people who are rational in the usual sense of the word and of course people who read this paper will be less inclined to deal with the Devil. The Devil really doesn't like it when people deny they have had dealings with him, it makes him feel sordid and shady. So even as we speak the Devil is warming a very special place in Hell for David.

Oh...and maybe you can now see why I've been thinking about "almost certainty" a bit recently. I should also add that S4 doesn't quite do the job I want. I think ◊¬(◊p∧◊¬p) really ought to be a theorem of my logic but it's provably not a theorem of S4. (Where I now use ◊ to mean "almost certainly".) I think I need some more axioms in addition to S4...

S4 and Partial Evaluation

I never cease to be amazed by the ubiquity of mathematical ideas. I'm still not entirely certain that S4 captures what I mean by "almost certain" but it's neat that S4 does a half-decent job of representing what we mean when we say "I know that X". It also has another application that relates back to partial evaluation.

Under the Curry-Howard isomorphism we have an isomorphism between (intuitionistic) propositional calculus and 'types' in a programming language. If A and B are types then A∧B is the cartesian product type, A∨B is the disjoint union type and A→B is the type of functions that take an A as input and return a B. That's all standard stuff. But now we can augment these types with a new type □A which means a piece of data whose value can be worked out by the compiler. For example we normally think of 1.0 as an object of type Float, but it's really of type □Float because the compiler can do stuff with 1.0 during compilation. The meaning of that should become apparent in the next paragraph.

The function sin is of type □(Float->Float) because, like 1.0, sin is just a constant so the compiler knows its value. If the compiler knows the value of something that is a function, and it knows the value of its argument, then the compiler is in a position to perform the computation at compile time. In this case, the compiler could compute sin 1.0 during compilation rather than defer the computation to the final executable. In other words we have a function □(a→b)->(□a→□b). But this is just the axiom K of S4. It's also, essentially, the same as partial evaluation as a described here.

If the compiler knows the value of something, it's still at liberty to delay the evaluation until runtime. In other words, we have a map □a→a. This is the axiom of S4 known as T. Notice that we don't have the reverse. A value of type a might be computed from an input from the user. As the compiler is presumed to have run before the user gets to input anything to the program there's no way the compiler can have a general way to promote an object of type a to □a. This axiom might be used if we chose to write code to add a number of type □Float to one of type Float. The compiler could cast the one of type □Float to type Float in order to allow the addition be performed in the executable at runtime.

Though we don't have a→□a we do have □a→□□a. This is more or less by fiat. It just says the trivial thing that if you say it's known at compile time twice over then that's the same as knowing it once. So we have axiom 4 of S4.

So intuitionistic S4 can be viewed as the logic we need to annotate types with information that tells the compiler what it can compute at compile time and what should be left until runtime. In a sense it's a form of macro evaluation providing some of the features that the C/C++ preprocessor provides when it runs just before compilation. But what's nice is that it's expressed in the language itself by extending the type system rather than as a separate language (which the C/C++ preprocessor essentially is.)

Anyway, this description is very rough and there are a few gotchas with this interpretation. So I suggest reading a real paper on the subject. My summary doesn't correspond exactly to any one paper I looked at so rather than reference one I can use the great universal qualifier known as Google to express them all in one go. Apparently there does exist an implementation of a subset of ML that supports these modal types.

By the way, I thought I'd revisit self-reproducing code armed with this modal logic to see if I could produce a typed version of the theorem that a language with partial evaluation always has a fixed point. But the axioms of S4 seem to rule out this kind of self-reference because I can't construct a function whose type allows it to accept inputs of its own type.

There seems to also be a connection with temporal logic with □ saying something about the time when a piece of data is available.

A Modal Logic of Near Certainty?

If this "□" isn't a square then the following will be unreadable for you. For some reason □ is less standard than ◊ and may be absent from a font when the latter is present, especially when printing.

So having read some stuff on modal logic (basically just what the Stanford Encyclopedia of Philosophy has to say) I was trying to make up a modal logic of my own. So what follows is just brainstorming. It might not make any sense at all if you try to work out the details. But as I was stuck in trying to figure out those details I thought I'd mention it here.

Usually □ is used to mean things like "it is necessarily the case that", "I know that" or "it ought to be the case that" but I thought I'd see if it could be used to mean "it is almost certainly the case that". Here's the intuition I'm trying to capture: □p would be roughly like saying p holds with probability 1-O(ε). So □□p would mean that we expect it holds with probability (1-O(ε))² which is the same as 1-O(ε). So we'd have □□p⇒□p. I intend "almost certainty" to mean so close to certainty that if A almost certainly tells the truth, and so do B, C, D up to Z, then if Z tells you that Y says that X claimed....that A said p then you could still be nearly certain that p is true.

Other examples of things that I'd expect to hold would be "continuity" conditions like

□A∧B⇒□(A∧B)⇒□A∧□B

and I'm nearly certain that

□A⇒◊A (where ◊A=¬□¬A by definition).

Anyway, it seems like a perfectly good modal logic to me. But when I tried to work out the possible world semantics I got nowhere, mainly because p⇒□p upsets things. I was also toying with the idea that "almost certain" is a bit like the strict mathematical sense of "almost always" and that there might be some kind of semantics that involves sets dense in some topology. But I couldn't work out the details of that either.

So can anyone who is knowledgable about these things tell me if what I'm trying to do is sensible? If I fill in more details can I use possible worlds to prove completeness and soundness?

The really wacky idea I had (and remember, I'm just brainstorming) is that you might be able to set up a differential calculus of logic. Just as you compute derivatives of a function w.r.t. x by perturbing x slightly and looking at how f(x) varies, □A might be seen as a slight deformation of A, hence my use of the term "continuity" above. I'd then expect to see a version of the Leibniz rule appear somewhere in the theorems of this modal logic.

Anyway, this might be going nowhere, so brainstorming over.

Update

Ordinary propositional calculus can be viewed as being set theory in disguise. Pick a set X. Now translate a logical proposition to a statement of set theory by 'atomic' propositions to subsets of X, ∧ to ∩, ∨ to ∪, ⊤ to X; ⊥ to ∅ and ¬ to the complementation in X operator. A proposition is true if and only if its translation always equals X. For example ¬p∨p translates to P∪(X\P) which is clearly X.

For my proposed modal logic put a topology on X. Then □ translates to the Cl operator where Cl(A) is the smallest closed set containing A. The things I want to be true again correspond to propositions whose traslations are all of X.

I think this modal logic captures exactly what I want. You can get a feel for it by thinking about propositions like x=3 on the real line. This is false "almost everywhere" (ie. on a dense subset of the real line, ie. a subset whose closure is the entire real line) so it makes some kind of sense to want to say □¬(x=3).

With some keywords to search on I was now able to find this paper. Page 29 (following the document's own page numbering) essentially describes what I have except that they have swapped □ and ◊. Essentially they're saying that this is the standard modal logic known as S4. This topological interpretation of S4 goes back to work by Tarski and McKinsey in 1944.

And now I can reason about almost-certainty with certainty.

Mongruences

Before saying anything I'd be interested in feedback on whether the mathematical symbols below are visible in your browser. Things like right arrow ⇒, infinity ∞ and union ∪.

Anyway, I've been trying to understand exactly what coindunction is all about. In particular I've been trying to figure out exactly what the duality is between induction and coinduction. The problem I was having was that induction and coinduction seemed not to be dual to each other at all, and weirder still, almost every discussion of coindunction that I looked at seemed to completely ignore the issue.

So here's my problem: in order to carry out an induction argument over the naturals, say, we find a predicate on the naturals, P, such that

P(0) and P(n) ⇒ P(s(n))

We can then conclude that P holds for all naturals.

In order to carry out a coindunction argument over the set of streams over A, say, we find a binary relation R (called a bisimulation) such that

R(a,b) ⇒ head(a)=head(b) and R(tail(a),tail(b)).

I can point out a certain amount of duality: The naturals form an initial F-algebra which is a fancy way of saying that they form a least fixed point to some equation, in this case N≅1+N. Here '1' means the type with one element called '*' and '+' is the disjoint union. We have a map s:1+N→N where s(*) = 0 and s(n) = n+1. s can
be thought of as a 'constructor'. Given something of type 1+N it shows how to construct an object of type N from it. Loosely speaking we can now see that induction is about forming a predicate that still holds after we apply a constructor.

Now consider the coinduction over all streams. A stream is a final F-coalgebra which is a fancy way of saying it's a greatest fixed point of the equation S≅A×S. We have a map (head,tail):S→A×S which maps a stream to its head (an element of A) and its tail (another stream). We can think of these as 'destructors' which reduce a stream back down to its component parts. And now we can see that coinduction is essentially about finding a binary predicate that still holds after applying a destructor.

But to my eyes, despite the duality there is a glaring difference: induction is about a unary predicate and coindunction is about a binary predicate. And through no amount of messing about with categories and their opposites was I able to find a way to see a unary predicate to be dual to a binary predicate.

So I gave in and tried to find something on the web about this subject and eventually was led to Bart Jacobs' paper Mongruences and Cofree Coalgebras. Inductive predicates aren't dual to bisimulations at all, rather inductive predicates are dual to what Jacobs calls mongruences. Unsurprisingly, this horrible neologism was dropped in favour of the term τ-invariant or just invariant in later papers. But I'm going to use the term out of sheer perversity.

But this paper still doesn't explicitly talk about coinduction over the naturals leaving me to work out the details. After chasing round the diagrams, including a nice demonstration of left and right adjoint functors (about which I seem to have managed to develop a crude intuition, who said you can't teach an old dog new tricks?) I managed to figure out what I think is the fairly simple definition of a congruence predicate for the naturals.

So instead of working over the naturals we actually work over N'=N∪{∞}, the set of 'conaturals'. The reason is that we are now looking at the final F-coalgebra that is the greatest fixed point to the equation X≅X+1, not the least fixed point. N' is equipped with a map p:N'→1+N' where p(0)=*, p(∞)=&infin and p(n)=n-1 otherwise. With this in mind a coinductive predicate for the conaturals (ie. a mongruence or invariant) turns out to be a P such that

P(n) ⇒ n=0 or n=∞ or P(n-1).

At least I think so. (This could be embarassing.) And now I can see why coinduction talks about bisimulations - mongruences aren't very interesting for the conaturals. Bit of a letdown really!

On the other hand there are some mongruences that are of mild interest in a more general setting. For example consider a finite state automaton with some terminal states. You can define a state to be safe if at no future point it's possible to reach the terminal state. So a state is safe if it isn't terminal and if all of its successor states are safe. If you think of a finite state automaton as a function f:X→(X×O)^I, where X is the set of states, I is the set of inputs and O is the set of outputs, then f is a 'destructor' and you can see that this definition fits into the same general pattern for coinductive definitions. So safety is a mongruence.

The obvious next question is: what is the dual of a bisimulation? These are called congruences but I haven't yet worked through the details of what these are.

My next question is this: given an inductive predicate you get to apply "proof by induction". What is the corresponding "proof by coinduction" for the conaturals? I'm not sure there is one. I have a vague sense of what proof by coinduction might look like for a more general mongruence but haven't figured out a non-trivial example yet.

But despite having learned about a concept that was uninteresting, and a proof method that I can't figure out how to apply, I have picked up something useful. The standard notions of proof by induction and proof by coinduction aren't straightforwardly dual to each other. So now I can stop worrying about it and get on with reading Vicious Circles.

The Minority Game

The El Farol restaurant in Santa Fe has "one of the best bars on earth" according to the New York Times. Unfortunately, on the days when it becomes too crowded it's more fun to stay at home. This can be modelled by a game known as the El Farol Bar Game or its simpler cousin, the Minority Game.

In the Minority Game, N players (with N odd) get to cast a secret vote either for A or for B. When all the votes have been cast the winners are the members of the minority group and they receive a payoff. But what is surprising about this game isn't just the game itself but the people who are studying it - physicists. The idea is that for large N the game looks like certain types of system from statistical thermodynamics. For example, consider the Ising model. In this we have an array of atoms, each of which can be spin up or spin down. Depending on the parameters of the model atoms either want to be aligned like their neighbours or aligned in the opposite direction. In the latter case we have a situation similar to the Minority Game. The Minority Game looks a lot like a 'frustrated' physical system with no obvious ground state. Just as a group start moving towards what seems like the optimum it ceases to be an optimum.

The game has been studied by many people using computer simulations. Typically the simulations result in the number of winners in each round hovering around one value. But the feature that many researchers have found interesting is the way that over multiple plays, independent players seem to spontaneously cooperate, despite the lack of communication. The result is that they reduce the variance, and hence risk, of the outcome below what you would expect from a purely randomised strategy.

MG can be used to model a wide variety of phenomena besides Saturday night drinking - including financial markets, traffic congestion, network congestion and even the ebb and flow of fashion.

The original paper by Mallet and Zhang may be found here but a web search will reveal that there are in fact hundreds of papers on the subject. It seems to be the in thing.

Anti-Foundation and Strong Extensionality

Barwise and Moss's Vicious Circles is about the Anti-Foundation axiom, an alternative to the usual axiom of foundation in set theory. I had a look at various online introductions to this subject and they all seem a bit long winded. So here's my own quick summary pared down to the bare minimum. (I sacrifice a bit of accuracy along the way but it should be enough to give a feel for the subject.)

Firstly: the whole point of the Axiom of Foundation is to eliminate infinite chains of membership. So the Axiom of Foundation says that there are no infinite descending chains:

...∈A₃∈A₂∈A₁∈A

(I hope you can read that, I'm using this list.)

The kind of thing that the Axiom of Foundation eliminates are sets x such that x∈x. It means we can define functions inductively over sets as we're always guaranteed to have a base case to start the induction. More generally imagine a system of equations such as

x = {x,y,z,4}
y = {x,z,2}
z = {{3},x,y}

The Axiom of Foundation rules out any solution to this. The Axiom of Anti-Foundation, on the other hand, says that any set of equations like this, with unknowns on the left, and sets containing those unknowns on the right, has a unique solution. (Note that the containing in that sentence is essential, x = x doesn't have a unique solution.)

And that's it, the Axiom of Anti-Foundation.

But there's a slight problem. Consider the equation x = {x} and the equation pair y = {z}, z = {y}. The solution to the first equation seems like it ought to be the solution to the second as well. But we have no way of telling this. In fact, there are issues just telling whether or not the sets x = {x} and y = {y} are equal. Normally in set theory we'd use the Axiom of Extension. Two sets are equal iff their elements are equal. So in this case we have x = y iff their elements are equal, ie. iff x = y. So the Axiom of Extension tells us nothing here. We need a new kind of Extension.

The idea is to find something like an isomorphism between two sets. For example, define f(x) = y for our last example above. Notice that for every element x' of x, there is an element y' of y such that f(x') = y'. f also has an inverse. It's a bit trivial in this case but it's a start. But suppose we compare the set x defined by x={x} with y defined by y={z} and z = {y}. We want some kind of isomorphism that maps x to both y and z. And with more complex sets of equations there might be any number of elements of one set that we need to map to any number of elements in the other. So what we need isn't a function but a relation connecting elements in one set to the other. The relation R is said to be a bisimulation between sets a and b if

aRb
for all a'∈a there exists a b'∈b such that a'Rb'
for all b'∈b there exists an a'∈a such that a'Rb'

If two sets are related by a bisimilarity then it can be shown that they satisfy the same equation and hence by the uniqueness of solutions they must be the same set. This property is known as Strong Extension. (I've paraphrased this from the original but I think it's essentially correct.)

And that's it - you can now go off and make your own non-well founded sets and compare them for equality.

I should add some interesting connections with computer science. Bisimulations are more familiar as a relation holding between automata. The usual Axiom of Extension gives a recursive definition of equality. Recursive definitions require a base case and with a base case we can get inductin proofs started. Without base cases we have corecursion instead and have to use a different proof technique, coindunction, whose main tool is bisimilarity.

Another interesting link with computer science is through F-algebras and F-coalgebras. I mentioned that F-algebras and F-coalgebras may have initial and final objects so that there is an isomorphism X≅F(X). The Axiom of Anti-Foundation often allows us to make the isomorphism equality. For example it's not hard to see that for a finite state automaton we can make a state simply equal to the set of transitions available from that state. In fact, that gives a nice way to answer the question I was originally asking in that earlier posting - how can I remove the labelling of the states and leave just the bare information about what transitions take me where?

And one important thing I should add - you can make a model in ZF for set theory with Anti-Foundation and Strong Extensionality. So it's consistent if ZF is. Additionally, Barwise and Moss also work with urelements, elements of sets that are not the empty set and yet contain no elements. I'm not sure, but I don't think these are essential to making sense of Anti-Foundation. Anti-Foundation, as described by Barwise and Moss, does make use of urelements in the definition of an equation (in particular to label the 'unknowns') but I think Anti-Foundation can be rewritten so as not to use urelements.

Update: I originally stated that Strong Extension was an axiom which it isn't. Just to add to the confusion, the Axiom of Anti-Foundation that I described above is called "The Solution Lemma" in Vicious Circles, even though it is an axiom.

SIGFPE's Law

I've decided it's time to stake my claim to the law that will ever be remembered and linked with my name. If Moore can get a law named after him, or even Murphy, then so can I.

SIGFPE's Law
This law is the prediction that the rate of growth of the number of bits on the best available quantum computers is going to grow linearly with time.

My reason for saying this is essentially the same as the reason that many people are sceptical of quantum computers - decoherence. It seems obvious to me that even with the cleverest of error correction schemes we're going to see the coherence of states decay exponentially fast. I'm bored of reading papers on quantum error correction and seeing that every one makes some assumption or other about the Hamiltonian that is not going to hold in practice. And any little deviation from that assumption becomes the coefficient in an exponential describing that decay.

On the other hand people are ingenious. As time goes by people will find ever more ingenious ways to fix the errors caused by decoherence. But the difficulty is going to grow exponentially and the solutions won't scale. So just as classical computing has seen an exponential growth in power I expect to see the logarithm of this and hence a linear growth. Maybe, just maybe, there'll be polynomial growth. But definitely not exponential growth. In fact, I expect it to be linear with a pretty shallow gradient, just a couple of qubits a year at most, and probably less. Humans will, one day in the distant future, crack large RSA keys using quantum computers - but when that day is reached humans will be well beyond caring about such trivial matters.

I also have nothing to lose by saying this. If I turn out to be wrong, and I sincerely hope I am, I can look forward to a world full of wonderful computing machines whose interest value will far outweigh the ignominy of being forever linked with an incorrect law.

BTW When I say n-bit quantum computer I mean a computer whose total memory is n qubits, not a computer with the qubits addressable by an n-bit word.

:-)

Quantum Probability

I took part in a brief discussion over at antimeta which reminded me that I ought to get back to a document I started writing on quantum mechanics for dummies. One of my pet peeves is that I believe there to be a little bit of a conspiracy to make quantum mechanics seem less accessible to people. Not a deliberate conspiracy - but people maintaining an aura of mystery about it that puts people off the subject. All of the fuzzy talk about quantum mechanics in the popular science press does nothing to help the situation. In particular, there is a core of quantum mechanics that I believe requires few prerequisites beyond elementary probability theory, vector spaces and complex numbers.

Anyway, I did some more digging on the web and found this course by Greg Kuperberg. The opening paragraphs almost take the words I wanted to say out of my mouth. In particular, despite the mystical mumbo-jumbo that is often written on the subject, the rules of quantum mechanics are "rigorous and clear" and "The precepts of quantum mechanics are neither a set of physical forces nor a geometrical model for physical objects. Rather, they are a variant, and ultimately a generalization, of classical probability theory." Most of all "...more mathematicians could and should learn quantum mechanics...". You don't even have to understand F=ma to get started with quantum mechanics and get to the point where you can really and truly get to grips, directly, with the so-called paradoxes of quantum mechanics such as the Bell Paradox. The strange thing is that you won't find words like this in most of the quantum mechanics textbooks. They throw you into physical situations that require finding tricky solutions to the Schrödinger equation while completely failing to give any insight into the real subject matter of quantum mechanics. Most QM books I know are really introductions to solving partial differential equations. (Remark to physicists: I bet you didn't know you could get the simultaneous eigenvalues for the energy and angular momentum operators for the hydrogen atom by a beautifully simple method that doesn't require even looking at a differential equation...) The best thing about the newly appearing field of quantum computing is that it's slowly forcing people to thing about quantum mechanics separately from the mechanics.

So even though I haven't read that course myself yet, I'm recommending that everyone read it :-) And some time I might get back to the even more elementary introduction I hope to put together.

A Neat Proof Technique

Last night I read this paper. There wasn't really anything in the paper I wanted, I was more interesting in flexing my newly developing computer science muscles. Anyway, like with all computer science papers I've managed to finish, I felt like I understood the paper but had no idea what the punch line was. Still, it was worthwhile because part way through there was a neat mathematical proof technique used that I think is worthy of a mention.

The paper is about the generalisations of 'fold' and 'unfold' that I played with recently. The usual fold function acts on a list like

[4,8,15,16,23,42].

Imagine it written as

cons(4,cons(8,cons(15,cons(16,cons(23,cons(42,[]))))))

where the cons function is a 'constructor' that constructs a list from a list element and another list. [] is the empty list. The fold function takes three arguments, a binary function f, a constant g, and a list. It then replaces cons by f and [] by g. For example

fold (+) 0 [4,8,15,16,23,42]

becomes

4+(8+(15+(16+(23+(42+0)))))

and so is 108, the sum of the numbers. An obvious theorem is that

fold cons [] x = x.

fold also generalises to structures such as trees. In this case there is another constructor that builds a tree from a node and its children. I'll stick with lists as the proof technique is much the same. The authors prove a bunch of theorems about the fold function. But now they want to prove something is true of all of the elements in a list (actually, a tree, but I use a list). Suppose the list is as above and you want to prove the property P holds for all elements in that list. Then you want to prove

P(4) && P(8) && P(15) && P(16) && P(23) && P(42) = True.

(I'm using Haskell's && to mean 'and'.) In other words you want to prove that

fold (&&) True [P(4),P(8),P(15),P(16),P(23),P(42)] = True.

The authors then proceed to show their theorem is true using the theorems about fold they just proved. Neat eh? But Maybe I haven't explained very well so I'll try to spell it out differently.

The authors want to prove theorems about all elements of a certain datastructure. So what they do is take the logical proposition that expresses what they want and rewrite the proposition so that the proposition itself in the same 'shape' as the datastructure. The statement of the truth of the proposition is an application of fold to the datastructure. So they can now use the theory of datastructures they develop to prove something about the structure of the logical proposition itself - namely that it's true. You need to read the actual paper (top left, page 5) to see the actual details of the proof technique.

In the particular case of lists the proof technique turns out to be standard induction. If you can prove P of an an element of the list, and you can prove "if P is true of an element it must be true of the next element", then P holds for every element of the list. Every time you generalise fold to a different datastructure there is a new induction principle that goes with it.

I suppose what they have actually done is prove a metatheorem about certain types of logical proposition and then used that to prove specific propositions.

Well, I hope that makes some kind of sense. I think it's quite a neat trick and that many of the paper's readers might miss the cool bit of self-reference that's going on here.

The General Theory of Self-Reproducing Programs

I'm guessing that anyone reading this is already familiar with the idea of programs that output themselves. If you're not there's a great list of such programs here. But what I was surprised to discover at the weekend was that there is in fact a bit of general theory about this. In particular, what do we need in a computer language to guarantee we can write a self-replicator?

Consider the following in Haskell:

let p x = x ++ show x in putStrLn $ p"let p x = x ++ show x in putStrLn $ p"

Evaluate this expression in an interactive Haskell session and it prints itself out. But there's a nice little cheat that made this easy: the Haskell 'show' function conveniently wraps a string in quotation marks. So we simply have two copies of once piece of code: one without quotes followed by one in quotes. In C, on the other hand, there is a bit of a gotcha. You need to explicitly write code to print those extra quotation marks. And of course, just like in Haskell, this code needs to appear twice, once out of quotes and once in. But the version in quotes needs the quotation marks to be 'escaped' using backslash so it's notactually the same as the first version. And that means we can't use exactly the same method as with Haskell. The standard workaround is not to represent the quotation marks directly in the strings, but instead to use the ASCII code for this character and use C's convenient %c mechanism to print at. For example:


main(a){printf(a="main(a){printf(a=%c%s%c,34,a,34);}",34,a,34);}


Again we were lucky, C provides this great %c mechanism. What do you need in a language to be sure you can write a self-replicator?

It turns out there is a very general approach to writing self-replicators that's described in Vicious Circles. What follows is essentially from there except that I've simplified the proofs by reducing generality.

We'll use capital letters to represent programs. Typically these mean 'inert' strings of characters. I'll use square brackets to indicate the function that the program evaluates. So if P is a program to compute the mathematical function p, we write [P](x) = p(x). P is a program and [P] is a function. We'll consider both programs that take arguments like the P I just mentioned, and also programs, R, that take no arguments, so [R] is simply the output or return value of the program R.

Now we come to an important operation. We've defined [P](x) to be the result of running P with input x. Now we define P(x) to be the program P modified so that it no longer takes an argument or input but instead substitutes the 'hard-coded' value of x instead. In other words [P(x)] = [P](x). P(x) is, of course, another program. There are also many ways of implementing P(x). We could simply evaluate [P](x) and write a program to simply print this out or return it. On the other hand, we could do the absolute minimum and write a new piece of code that simply calls P and supplies it with a hard-coded argument. Whatever we choose is irrelevant to the following discussion. So here's the demand that we make of our programming language: that it's powerful enough for us to write a program that can compute P(x) from inputs P and x. This might not be a trivial program to write, but it's not conceptually hard either. It doesn't have gotchas like the quotation mark issue above. Typically we can compute P(x) by some kind of textual substitution on P.

With that assumption in mind, here's a theorem: any program P that takes one argument or input has a fixed point, X, in the sense that running P with input X gives the same result as just running X. Given an input X, P acts just like an interpreter for the programming language as it outputs the same thing as an
interpreter would given input X.

So here's a proof:
Define the function f(Q) = [P](Q(Q)). We've assumed that we can write a program that computes P(x) from P and x so we know we can write a program to compute Q(Q) for any Q. We can then feed this as an input to [P]. So f is obviously computable by some program which we call Q₀. So [Q₀](Q) = [P](Q(Q)).

Now the fun starts:

[P](Q0(Q0)) = [Q0](Q0) (by definition of Q0)
            = [Q0(Q0)] (by definition of P(x))

In other words Q₀(Q₀) is our fixed point.

So now take P to compute the identity function. Then [Q₀(Q₀)] = [P](Q₀(Q₀)) = Q₀(Q₀). So Q₀(Q₀) outputs itself when run! What's more, this also tells us how to do other fun stuff like write a program to print itself out backwards. And it tells us how to do this in any reasonably powerful programming language. We don't need to worry about having to work around problems like 'escaping' quotation marks - we can always find a way to replicate the escape mechanism too.

So does it work in practice? Well it does for Haskell - I derived the Haskell fragment above by applying this theorem directly, and then simplifying a bit. For C++, however, it might give you a piece of code that is longer than you want. In fact, you can go one step further and write a program that automatically generates a self-replicator. Check out Samuel Moelius's kpp. It is a preprocessor that converts an ordinary C++ program into one that can access its own source code by including the code to generate its own source within it.

Another example of an application of these methods is Futamura's theorem which states that there exists a program that can take as input an interpreter for a language and output a compiler. I personally think this is a little bogus.

Stanislaw Lem has Passed Away

He has an obituary in The Times. If you haven't read any of his science fiction you really should read some. For lovers of mathematical poetry out there, here is a translation of a passage from his Cyberiad:

Come, let us hasten to a higher plane,
Where dyads tread the fairy fields of Venn,
Their indices bedecked from one to n,
Comingled in an endless Markov chain!

Come, every frustrum longs to be a cone,
And every vector dreams of matrices.
Hark to the gentle gradient of the breeze
It whispers of a more ergodic zone.

In Riemann, Hilbert or in Banach space
Let superscripts and subscripts go their ways.
Our asymptotes no longer out of phase,
We shall encounter, counting, face to face.

I'll grant thee random access to my heart,
Thou'lt tell me all the constants of thy love;
And so we two shall all love's lemmas prove,
And in our bound partition never part.

For what did Cauchy know, or Christoffel,
Or Fourier, or any Boole or Euler,
Wielding their compasses, their pens and rulers,
Of thy supernal sinusoidal spell?

Cancel me not--for what then shall remain?
Abscissas, some mantissas, modules, modes,
A root or two, a torus and a node:
The inverse of my verse, a null domain.

Ellipse of bliss, converge, O lips divine!
The product of our scalars is defined!
Cyberiad draws nigh, and the skew mind
Cuts capers like a happy haversine.

I see the eigenvalue in thine eye,
I hear the tender tensor in thy sigh.
Bernoulli would have been content to die,
Had he known such a²cos(2φ) !

The Most Amazing and Mysterious Thing in All of Mathematics

I think that a good candidate is the table of the Homotopy Groups of Spheres.

For those not familiar with algebraic topology, π_m(Sⁿ) is the set of equivalence classes of continuous functions from the m-dimensional sphere to the n-dimensional sphere where two functions are considered equivalent if they are homotopic. An easy way to visualise this is that two functions are homotopic if you can interpolate a continuous animation between them. (Can you guess what industry I work in?) This set also has a group structure which is straightforward to define but which I won't go into here (unless someone requests it). That's all there is to it. How can such simplicity generate such complexity?

Monstrous Moonshine is pretty mysterious too - but it takes a lot of work to state it for a non-expert. So this wins by default.

Like John Baez I also wonder about the curious appearance of 24 on row 3.

And an aside I discovered on Anarchaia: foldr.com related to an earlier post.