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 code 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 far, together with my ratings using almost the simplest possible system.

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.)