Projects

Introduction to Cubical Agda

David and I ran a summer course on Cubical Agda for the few years we were at NYUAD. We put together some lecture notes, which are now available here.

I like to think of them as a much-expanded and smoothed out version of The HoTT Game from a few years ago, where as much as possible is left as exercises.

at – Effective Algebraic Topology

A Haskell library for explicit constructions on simplicial sets. This is a port of Kenzo from Common Lisp. More details in this post.

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

Conway’s Game of Life Tools

I’ve written a handful of C++ search tools, most of which use a vastly expanded fork of the LifeAPI library by Michael Simkin. The first two tools in this list were central in resolving the Omniperiodicity of the Game of Life.

• Symmetric CatForce: A catalyst-placing search program. Similar to ptbsearch. Has been used to find a huge number of interesting oscillators.

  Originally based on CatForce, also originally by Micahel Simkin, but very little original code remains.

• Barrister: A cell-by-cell searcher for catalysts. Similar to Bellman by Mike Playle, but uses a more careful analysis of the neighbourhoods available to each cell. This, together with being more vectorised, makes it much faster. Barrister was used to find the catalyst appearing in the first period-19 oscillator, and many oscillators and conduits since.

  Adam P. Goucher has written a searcher in CUDA based on Barrister called Silk. Silk is much much faster still (but by nature somewhat less customisable).

• Lightcone: A catalyst-placing search program that tries much harder to take into account “lightspeed considerations” between how different parts of the pattern can interact. Details in this post. Has been used to find a handful of new elementary conduits especially “spartan” ones.

• Stomp: A port of the transfer.py script to LifeAPI, for searching for new glider syntheses. Used to pick the low-hanging fruit in the project of synthesising all 23-bit still lifes, though human ingenuity (of other people, not me) was still necessary for the last couple of hundred.

cf – Continued Fractions

A Haskell library for Gosper’s algorithms on continued fractions with possibly non-positive terms. Some tricks from Vuillemin and Lester are used to compute transcendental functions (e.g. exp, sin and cos) on rational numbers.

The novel idea is that these algorithms apply to continued fractions whose terms are also continued fractions, allowing us to also apply these transcendental functions to general continued fractions. A function cfcf flattens one of these into an ordinary continued fraction.

A nice advantage the continued fraction representation is that the precision of a result does not need to be specified in advance. If more precision is required, one can just compute more terms in the continued fraction, without throwing away the work already done. The downside is that it is very slow!

• Gosper, Ralph W. “Continued fraction arithmetic.” HAKMEM Item 101B, MIT Artificial Intelligence Memo 239 (1972).
• Vuillemin, Jean E. “Exact real computer arithmetic with continued fractions.” Computers, IEEE Transactions on 39.8 (1990): 1087-1105.
• Lester, David R. “Vuillemin’s exact real arithmetic.” Functional Programming, Glasgow 1991. Springer London, 1992. 225-238.

cgt – Combinatorial Game Theory

A Haskell library for some combinatorial game theory, based on algorithms from the Combinatorial Game Suite by Aaron Siegel. More details in this post, which describes the basic ideas.

epeen

A dumb joke that translates your Dota 2 MMR (as of 2016) into to a certain anatomical measurement. Written in Elm to try the language out, didn’t come away a fan.