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.

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. They choose two movies that haven’t been nominated before.
3. Everybody else votes for which to watch. If the vote is a tie, the nominator breaks the vote.
4. In highly exceptional circumstances, the Benevolent Dictator For Life may declare that a specific movie 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.)