Using Thermonuclear Pennies to Embed Complex Numbers as Types

Forget about types for now.

The Game of Thermonuclear Pennies

The game of Thermonuclear Pennies is a lot like the game of Nuclear Pennies. It's played on a semi-infinite strip of cells, extending to infinity on the right, with a bunch of pennies in each cell (and a finite number in total). Instead of a single penny fissioning into two pennies, it now splits into three adjacent pennies. And conversely, three neighbouring pennies may be fused into one.

Here are examples of legal moves:

and


Again the puzzles consist of trying to get from a start position to a target position. Here's a nice example:



Just as with Nuclear Pennies we can assign numerical values to positions in this game in such as way that if there is a legal sequence of moves from A to B then the value of A equals the value of B. In this case we assign the values very slightly differently. Each cell is assigned a value as follows:

Where i is the usual square root of -1. The value of a position is simply the sum of the values of the pennies where each penny takes on the value of the cell it sits in. So

As before, we say that moving from A to B is paralegal if A and B have the same value. Because i satisfies i=1+i+i² it should be clear that legal implies paralegal again. But here's a surprising fact: if both A and B have pennies not on the leftmost cell, then a move from A to B is legal if it is paralegal. In other words, we can tell if a sequence of moves is possible just by looking at the numerical value of the start and end points. What's more, the corresponding result also holds for Nuclear Pennies and a wide variety of related games besides. Before proving that I want to talk about the algebraic structure of these types of games. (And I just figured out how to procedurally generate diagrams with Omnigraffle using Applescript so it's an excuse to draw lots of diagrams.)

(BTW If we're allowed to have a negative number of pennies in a cell then you can simply treat a position in these games as polynomials with integer coefficients. You can then use standard theorems about polynomials to prove the result in a straightforward way. But those theorems rely on subtraction, and without negative numbers those methods fail.)

Firstly, we can add positions in Thermonuclear pennies (which I'll now call TNP). Simply add the numbers of pennies in each cell:

We can also multiply positions. We do this by making a 'multiplication table' from the original positions and then summing along the lower-left to upper-right diagonals. I hope this example makes it unambiguous:


Exercises. Convince yourself that A+B=B+A, A*(B+C) = A*B+A*C, (A+B)*C = A*C+B*C, A*(B*C) = (A*B)*C.

If you did the exercises, you've now shown that TNP positions form a commutative semiring, or rig, with the empty board serving as 0.

Now we're ready to use a proof from Objects of Categories as Complex Numbers by Fiore and Leinster. If we define

then every position is a polynomial, with non-negative integer coefficients, in x. We can also interpret the equation x=1+x+x² as saying that fission and fusion are legal moves. More generally, we consider two positions equivalent if there is a sequence of legal moves going from one to the other where each move maps f(x)+x to f(x)+1+x² or the converse. If we define p₁(x)=x and p₂(x)=1+x² then equation (3) in that paper defines exactly what we mean by a sequence of legal moves. (BTW For those wondering about the order in which I wrote this, I read that definition after inventing the game :-) So now we can apply Theorem 5.1 to find

Corollary

Let q₁(x) and q₂(x) represent TNP positions with at least one penny somewhere other than the far left, then if x^2+1=0⇒q₁(x)=q₂(x) ring-theoretically, then there is a legal sequence of moves from q₁(x) to q₁(x).

"x^2+1=0⇒q₁(x)=q₂(x)" is just another way of saying q₁(i)=q₂(i). So we have a simple way to tell whether there is a legal way of getting from one position to another. The puzzle example I gave above is soluble because i⁵=i.

Actually, the corollary isn't too hard to prove without the theorem. Here's a hint for how to do it. If we allow negative numbers of pennies the puzzle is fairly easy to solve. But we don't need negative pennies because if there is at least one penny, we can saturate as many positions as we like with as many pennies as we like simply by madly fissioning pennies all over the place in a big chain reaction. So we start by doing the chain reaction to borrow lots of pennies, then carrying out the solution using negative numbers (which won't actually ever go negative if our chain reaction was big enough) and then reversing the chain reaction to pay back what we borrowed. (It's a bit like real life. In a financial market without negative numbers there are many transactions that can't be performed. But as soon as we allow borrowing we open up many more possibilities.)

Embedding Complex Numbers as Types

So back to types. People have frequently found the need to embed the natural numbers as types. A popular scheme is something (in Haskell) like

> data Zero
> data S a = S a
> type Two = S One
> type Three = S Two

and so on. Then we can go on to define addition and multiplication. But types already have a natural addition and multiplication: the type constructors Either and (,). The problem is that, for example, Either One Three isn't the same type as (Two,Two). We could relax things a bit and allow isomorphism instead of equality. But even then, these types aren't isomorphic. Instead we could define:

> data Zero
> data Unit = Unit
> type S a = Either Unit a 
> type One = S Zero 
> type Two = S One
> type Three = S Two

Now we can use Either and (,) as addition and multiplication.

But if you're content to live with isomorphism then maybe we could embed other types. Consider the type

> data Tree = Leaf | Trunk Tree | Fork Tree Tree

It's easy to write an isomorphism Tree -> Either One (Either Tree (Tree,Tree)). In other words, up to isomorphism we have Tree=1+Tree+Tree². If you remember my earlier post it should be clear that legal sequences of moves in TNP give rise to isomorphisms of types constructed from Tree. In other words, theorems about TNP apply to Tree. Therefore given two polynomials, p₁ and p₂, p₁(Tree)=p₂(Tree) if and only if p₁(i)=p₂(i), as long as the p_i contain non-constant terms. Looked at another way, given any Gaussian integer, a+bi, we can embed this as a type in such a way that the embedding respects Either and (,). In fact the type

aTree+bTree²+cTree³+dTree⁴

embeds (d-b)+(a-c)i. For example, abusing Haskell notation,

> type Zero = Tree+Tree3

really does act like zero in that (Zero,p(Tree)) has an isomorphism with Zero for any non-constant polynomial p.

As far as I can see, this fact is completely and utterly useless...

NB When I say isomorphism above I mean "particularly nice isomorphism", which in this case means an isomorphism that takes time O(1). Otherwise all countable tree structures would trivially be isomorphic.

How can it possibly be that we can exhaustively search an infinite space in a finite time?

There has been a bit of talk recently about how it is possible to exhaustively search certain infinite spaces in a finite time. Unfortunately the explanations seem to be couched in topological language making them a little inaccessible. So I thought it'd be good to attempt a rigorous, but elementary, proof so that is possible to see exactly where the 'magic' happens.

Consider the type of infinite streams of booleans:

type Natural = Integer
Stream :: Natural -> Bool

Can we write a function search, that takes as argument a boolean predicate on Stream, and tells us whether or not there is a stream that satisfies it?

search :: (Stream -> Bool) -> Bool

This sounds like an impossible task. There are uncountable many infinite streams of booleans, so how can we hope to search them all? There's one important thing in our favour: we're restricting ourselves to predicates that are computable and total. In other words, whatever stream we pass to the predicate, they have to return a boolean in a finite time.

First, let's deal with an objection that make search seem impossible to implement. Given a 4-tuple of integers, we can encode these integers in a stream. For example, the integers (written in binary) (11,10,1,111) could be encoded as

11110011100011001111110100000000000000000...

where we code the binary digit b as 1b, we separate the integers using 00 and terminate the sequence using 01. We could then write a predicate that checks to see if the 4-tuple gives a solution to xⁿ+yⁿ=zⁿ with x,y,z>0 and n>=2. Plugging that into search we apparently have a way to decide the Fermat-Wiles theorem without doing any difficult number theory. Surely, therefore, search can't exist? But the predicate we've just described isn't total. Suppose we feed it the string 111111... as input. It's going to think that these represent an x with leading digits 111... and it's going to sit there collecting digits forever. It's never going to terminate. So the requirement that the predicate be total is such a strong condition that we can't actually implement the Fermat predicate, even though it uses nothing more than simple arithmetic. So maybe search is beginning to look a little more plausible.

Here's the key thing: any predicate on boolean streams must terminate after a finite time, meaning it only reads a finite number of booleans. So given any predicate p, there is a (mathematical) function d_p on the boolean streams with the property that d_p(s) is the index of the last bit p looks at when given s as input. d_p(s) is obviously always finite.

Now at this point you might immediately jump to the opposite conclusion that of course search is possible because you only need to check a finite number of bits. But even though d_p(s) is always finite, it might be unbounded as s varies over the infinite set of streams. So the finiteness of d_p on its own is not enough to bound our search. For example, consider predicates on 4-tuples of integers again. Each of these predicates reads only a finite number of bits, and yet we don't expect a general purpose terminating search algorithm can tell us whether or not Fermat's equation has a solution. So to prove termination for the boolean stream case we need to exploit some more structure.

Here's a first hint at what that structure might be. Suppose we try to make d_p unbounded by arranging that

d_p(00000....) = 1

d_p(10000....) = 2

d_p(01000....) = 3

d_p(11000....) = 4

and so on.

You might notice that we immediately have a contradiction. If d_p(00000...)=1 then the predicate must stop reading bits after it has read an initial 0. So actually, the sequence d_p(01000...) is also 1. Lots of streams share prefixes in this way, so the question is, does the infinitude of the set of boolean streams win out, or does the amount of sharing of prefixes eventually tame the infinity?

Consider the following infinite binary tree:



Each boolean stream corresponds to a single downward path through this tree. Fix a predicate p. Suppose, then, that this predicate, when fed the stream 011..., requires only 3 bits to be read, ie. d_p(011...) = 3. Then we can cut off everything below that point on the tree because no predicate need read that far. We've removed every infinite path passing through 011:



Every stream s has a finite cutoff after d_p(s) steps. And after we've hacked away all of the bits that our predicate never looks at what we're left with is a finitely branching tree with no infinite paths. Now comes the magic: we invoke König's Lemma which says "every tree that contains infinitely many vertices, each having finite degree, has at least one infinite simple path.". Conversely, if there are no infinite paths, the tree must be finite. In other words, for any predicate p we only need to search a finite tree.

The rest is just details, such as the precise method by which we determine when we've finished searching. In the case of Martín Escardó's paper the details are some of the most ingenious coding I've ever seen.

Update: I fixed the type of search above. Thanks to Cale for pointing this out. Unfortunately I deleted his comment by accident so I'm crediting him here.