The code in the previous post is fairly quick, but of course we’d always prefer it to be quicker. I’ll keep a record here of things I’ve tried and whether they worked.

The No-three-in-line problem asks how many points can be placed on a n \times n grid so that no three points are on the same line, where the lines considered are of any slope and not just orthogonal and diagonal. Each row/column can contain at most 2 points, so clearly the answer is at most 2n. The real question is, can we actually achieve 2n for every grid size? It’s conjectured that the answer is “no” for grids large enough, but we don’t know where the crossover point is and there’s no indication that the number of 2n-point solutions is falling away from exponential growth, at least up to 18 \times 18!

To my eye, the configurations that work can be quite balanced and attractive. Here are some symmetrical ones for 14 \times 14 (though in general the solutions are not necessarily symmetric in this way):

The most extensive searches for configurations so far have been done by Achim Flammenkamp and later by Ben Chaffin. I’ve written some CUDA codeBy the way, the existing cuda-mode for Emacs is a bit messed up, I have a fork with some bugfixes here.

of my own with the goal of pushing things a little further, and I’ll explain it in the rest of this post.

QuFince is a CUDA tool written by apg to conduct brute-force Game of Life searches on the cartesian product of two sets of configurations. That is, each configuration from set A is combined with each configuration from set B, and run until stabilised. Not every result is reported, only those where certain criteria are met. Right now the options are either that the result has some interesting periodInteresting period here typically means period not dividing 120, to rule out blinkers, pulsars, pentadecathlons and figure eights, among other things.

(to hunt for glider syntheses of oscillators), or that the result contains a specified pattern (to hunt for synthesis components for specific still lifes).

One thing that can’t be done currently is have QuFince report any combination that results in an interesting still life, but without knowing which still life you want in advance. It’s not so obvious what “interesting still life” should mean exactly, but here are some randomly chosen examples of things that should qualify:

We can’t use a population threshold as our criterion for interestingness, because the typical result of one of these QuFince trials is a bunch of uninteresting junk. One option is to do proper object separation, like apgsearch, and then report any object that is sufficiently rare. But a QuFince search can conceivably test hundreds of billions of configurations, and full object separation is simply too slow.

Here I’ll present an alternative, a simple heuristic that works well enough.

As a second foray into CUDA, I’ve written a simple program to hunt for crawlers in the Game of Life. The kernel itself is too revolting to make public, but the supporting LifeStateCU code may be useful for others. (This could be seen as the first step in a GPU version of CatForce/LightCone…)

Officers is a two-player “take-and-break” game played with heaps of coins (or if you prefer, piles of beans, or officers and their subordinates, or groups of people who form indivisible couplesIn the equivalent game Couples-are-Forever, a move is to choose a heap and split it into two, with the proviso that you may not split a heap of size 2. An Officers heap of size n is equivalent to a Couples-are-Forever heap of size n+1.

, or …). The two players alternate turns, and every turn consists of removing a coin from a heap and leaving the remainder in either one or two heaps. In particular, taking away a lone coin is not a valid move. The winner is the last player who can make a move.

For example, a game starting with a single pile of 10 coins might proceed

[10] \xrightarrow{\mathcal{L}} [3, 6] \xrightarrow{\mathcal{R}} [3, 1, 4] \xrightarrow{\mathcal{L}} [1, 1, 1, 4] \xrightarrow{\mathcal{R}} [1, 1, 1, 1, 2] \xrightarrow{\mathcal{L}} [1, 1, 1, 1, 1]

at which point player \mathcal{R} is stuck, so player \mathcal{L} has won.In fact, he was following the winning strategy.

Although the total number of coins decreases by 1 each turn, the outcome of the game is not determined simply by the parity of the starting number of coins: the moment that the game ends also depends on how many piles are created by the players making splitting moves. As we will soon see, the winning move from any given position is extremely unpredictable.

We can solve a game of this kind by calculating the Grundy value for each position, and in this post I’m going to discuss my attempt at calculating these values for Officers as fast as possible.

Conduits are a central piece of technology in Conway’s Game of Life, especially when engineering new pieces of stable circuitry. A conduit moves an active pattern (like a Herschel or B-heptomino) from one location to another by allowing it to react with a collection of stable catalysts. Along the way, it may release some gliders, produce additional active patterns or perform some other useful interaction, and so new pieces of machinery can be constructed by chaining conduits together.

As one very famous example we have the Fx77 conduit discovered by Dave Buckingham, which moves a Herschel forwards in 77 generations, also flipping it.

Many software tools have been written to search for new conduits: ptbsearch by Paul Callahan, Catalyst by Gabriel Nivasch, catgl by Dave Greene, CatForce by Michael Simkin and LocalForce by Nico Brown, to name a few. Typically these tools are handed an active pattern and a collection of catalysts, and spit out all placements of catalysts that interact with the active pattern and recover. At this point, hundreds of conduits are known, converting to and from various active patterns. But the more the merrier!

I’ve been working on yet another search tool, called Lightcone. Lightcone is pretty speedy: it can find apg’s Spartan G-to-W on this input file in just a couple of seconds. In this post I’ll explain some of the tricks it uses to cut down the search time.

Code available on GitHub.

For a little while I have been working on this port of Kenzo from Common Lisp to Haskell. Kenzo is a collection of algorithms for explicit constructions on simplicial sets: the README in the repository gives a list of what’s implemented and what should be possible. The algorithms and implementations in Kenzo were created by Francis Sergeraert, Julio Rubio Garcia, Xavier Dousson, Ana Romero and many collaborators.

My goal was to implement just enough to compute \pi_4 S^3, and I reached it today.

...
> let x = totalSpace s3 (Wbar kz1) fibration
> putStrLn $ "π₄ S³ is: " ++ show (homology x !! 4)
π₄ S³ is: ℤ/2

A fun capability it picked up along the way is calculating the homology of Eilenberg-MacLane spaces K(ℤ/m,n), for example, here is K(ℤ/3,2).This makes my laptop get hot pretty quickly.

> homology (Wbar (WbarDiscrete (Zmod 3)))
[ℤ,0,ℤ/3,0,ℤ/3,0,ℤ/(3^2),ℤ/3,ℤ/3,ℤ/3,ℤ/3 ⊕ ℤ/3,^C

I have a lot of ideas for improvements and additional features if anybody is interested in joining in, so please email me if that’s you or you know a student for whom this would make a good project. For example, adding the construction of loop spaces and their homology would be nice, as would homotopy pushouts in general.

On the implementation side, I have not spent any time optimising the code and there are some obvious places to start, like using a proper integer matrix library instead of a homemade one. These sorts of optimisations would also make a good project for an undergraduate, with not much mathematical background required.

Below, I’ve copy-pasted a quick introduction I wrote to the ideas behind Kenzo.

Hamana describes a neat way of encoding general graphs as a GADT in Initial Algebra Semantics for Cyclic Sharing Tree Structures, a nice trick that I hadn’t seen before. The idea is that the Graph data type will have a Ptr constructor that allows us to add an edge reference other parts of the structure. The Graph type will be indexed by a ‘context’ that specifies what Ptrs are valid.

Elements of Graph won’t correspond to general graphs exactly. We are actually describing graphs that are “rooted, connected, directed and edge-ordered with each node having out-degree 2”. It is possible to choose different roots and orderings for the same graph, and these choices will lead to different representations as elements of Graph. The problem of determining whether two elements of Graph have the same underlying actual graph seems like it would be difficult in general.

{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}

module Graphs where

First, let us define a type describing the possible shapes of our data structure. We will be using this at the type-level via DataKinds. Our Graphs all have underlying binary trees.

data TreeShape where
  LeafShape    :: TreeShape
  BinShape     :: TreeShape -> TreeShape -> TreeShape

There are also special leaves that are Ptrs to other locations.

  PtrShape     :: TreeShape

And finally, we will need a way of blocking off a section of a graph so that a Ptr can’t refer to it.

  VoidShape    :: TreeShape

This won’t occur as the shape of an actual graph.

The next piece is an indexed type that, given a TreeShape, picks out the location of a node in that shape. These will be what we use to specify where in a tree a Ptr is pointing.

data TreePosition (shape :: TreeShape) where
  LeafPos  :: TreePosition LeafShape
  BinPos   :: TreePosition (BinShape s t)
  LeftPos  :: TreePosition s -> TreePosition (BinShape s s')
  RightPos :: TreePosition s' -> TreePosition (BinShape s s')

There is, of course, no constructor for TreePosition VoidShape. We also don’t allow TreePosition PtrShape, which means that Ptrs will be required to point to genuine nodes in the tree, and not other Ptrs. This avoids there being multiple ways of specifying the same tree via chains of pointers, rather than having each Ptr target the eventual node at the end of the chain.

We’ll need to be able to index type-level lists, so let’s get that out of the way:

data Elem :: k -> [k] -> * where
  Here :: Elem s (s : c)
  There :: Elem s c -> Elem s (t : c)

Now for the actual graph type. The type is indexed both by the shape of the underlying tree, and a context, a list of TreeShapes. As we build a tree, this list is collecting the shapes of all the subtrees used as a left branch of an earlier binary node.

Consider the following tree:

             a
            / \
           /   \
          a     b
         / \   / \
        a   a b   *
               \
                b

If we are currently defining the subtree to be placed at *, then the context will consist of the two shapes

                      a
         b           / \
        / \         /   \
  [    b   0  ,    a     0   ]
        \         / \
         b       a   a

In the subtree to be placed at *, we may have pointers to as or bs, but not the 0s.

data Graph (context :: [TreeShape]) (shape :: TreeShape) where
  Leaf :: Graph c LeafShape

Leaves are easy, we can have a leaf in any context.

  Ptr :: Elem s context -> TreePosition s -> Graph context PtrShape

For the pointers, we pick a shape from the context and then a position in that shape.

  Bin :: Graph (BinShape VoidShape VoidShape : c) s
      -> Graph (BinShape s VoidShape : c) t
      -> Graph c (BinShape s t)

The interesting case is a binary node. In the left and right branches, we push new trees onto the context c. When defining the left branch, we only have access to one additional node over what is already in c: the binary node we are currently defining. In the right branch, we have access to the entire left branch: note that the shape s of the left branch is what is pushed onto the context. This is why this type has to be indexed over the shape of the resulting graph, not just the context.

And that’s it! We can add labels to the nodes in the graph if we like, by adding a parameter to the Leaf and Bin constructors.

Graphs of shape s then correspond to elements of Graph '[] s. If we don’t care about having the shape as part of the type, we can existentially quantify it.

data AnyGraph = forall s. AnyGraph (Graph '[] s)

Here are some simple graphs:

graph1 :: AnyGraph
graph1 = AnyGraph $ Bin (Bin Leaf Leaf) (Bin (Ptr (There $ Here) (LeftPos $ LeftPos $ LeafPos)) Leaf)

Corresponding to

     *
    / \
   /   \
  *     *
 / \   / \
*   * /   *
 \   /
  ---

We can modify what kinds of graphs are representable by changing the way the context is extended. Note that we can currently have cycles in the graph:

graph2 :: AnyGraph
graph2 = AnyGraph $ Bin Leaf (Ptr Here BinPos)

corresponds to

    ---
   /   \
  *    /
 / \  /
*   --

It’s not hard to change this though:

data DAG (context :: [TreeShape]) (shape :: TreeShape) where
  DAGLeaf :: a -> DAG c LeafShape
  DAGPtr :: Elem s context -> TreePosition s -> DAG context PtrShape
  DAGBin :: DAG c s -> DAG (s : c) t -> DAG c (BinShape s t)

The only difference is in the DAGBin constructor. Here, when constructing the left branch, we are no longer permitted to reference the current binary node. The same is true when constructing the right branch, but we still give it access to the left branch. The result is that every Ptr points to something to the left, other than a direct ancestor of the current node. That is enough to rule out any cycles.

We have no need for VoidShape here, which is nice.