In the Game of Life, which still lifes can be produced by crashing gliders together? We’ve known for a few years that the answer cannot be “all of them”, because in 2022 Ilkka Törmä and Ville Salo found a patch of still life that, if it exists in the universe, must have existed since the beginning of time. And so, there is no way we could have produced it out of empty space through glider collisions. Similar such patches have been found since, with the goal of optimising size or population, and at the time of writing the record holder is an unsynthesizable still life with population 154 produced by forum user “400spartans”.

Finding syntheses for small still lifes is easy, but at some unknown point below 154 it becomes impossible. Today, we completed our collaborative project to notch the lower bound up from 22 to 23, by giving explicit syntheses for all 1,646,147 (strict)A still life is strict when all its islands are necessary to maintain the stability of the pattern.

still lifes with population 23.

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.

Benton’s Linear/Nonlinear Logic has models in (lax) monoidal adjunctions between monoidal and cartesian categories.

The tasks performed in GPU kernels often deal with linear and nonlinear maps between real vector spaces.

I want to take this and run with it: let’s see what it looks like to define some mixed linear/nonlinear functions in a linear/nonlinear type theory. This feels to me so obvious that it must be written down somewhere already. In the literature there is work that gets close (and I’ll do some comparisons at the end), but none are quite what I want. Please let me know if I’ve missed something.

Edit: It’s been pointed out to me that the type theory I’ve put together is almost exactly the Enriched Effect Calculus, though I still haven’t seen the semantics in ordinary vector spaces discussed anywhere. And see my follow-up!

For years now I’ve been watching a movie in-person with friends every weekend that I’ve been able to. The movie selection system is perfect, crystalline, sacred, with no downsides or exploitable vulnerabilities.

1. The nominator is the person who was previously nominator the longest ago.
2. The nominator chooses two movies that haven’t been nominated before.
3. Everybody else votes for which to watch. If the vote is tied, the nominator breaks the tie.
4. In highly exceptional circumstances, the Benevolent Dictator For Life may declare a specific movie to be watched, for example, if we’re all about to go watch a sequel in-theatre and some people need to get up to speed.

Here’s what we’ve watched so farThe alternative movies from some of the early, legendary movie nights have been lost to time.

, together with my ratings using almost the simplest possible system.And take these ratings with a grain of salt, I like more of the movies that I see than the average person.