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.

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.

When I walk around my neighbourhood, I am struck by the beautiful character of the houses here: the draughty Queenslanders and timber fences, the majestic external staircases, I could go on forever. But something always felt off, and I finally realise what it is. How can I admire a house with elegant stilts and sweeping verandahs when there is a bright red 2019 Ford Puma sitting in the driveway? Or appreciate a compact, postwar masterpiece when it has a Hilux poking out around the side? In the hours I’ve spent positioning myself on the street so I can bathe in the heritage of my neighbourhood, I have not found an angle without some such monstrosity in my field of view.

We’ve spent years fighting the vandals who want to destroy the heritage of our neighbourhood. Why should we make an exception for this? I see no other option: we must forbid residents from bringing any new cars into the area. This is already a compromise, as if I had my way we would ban every car newer than the house it is parked in front of. (Of course, some especially old houses would need hitching posts to be reinstalled.)

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.