Langton's ant

I've been thinking on and off about Langton's Ant. It bugs me that nobody's resolved the conjecture about the ant eventually building a highway (I'm going to assume you looked at the wikipedia page, and not explain things again here!). I thought it'd be a fun recreational math problem to poke at, and I can now at least say that it is fun!

Today, I started out wanting to implement Langton's Ant in javascript, just to have something to play with. Implementing things like this is always interesting, because there are typically a lot of ways to write the program that are kind of annoying and painful; for example, in this case, you could encode the 2D grid the ant lives on as an array, but arrays in javascript have finite size, and so you'd have to watch closely to make sure the ant doesn't run off the edge of the array and then resize it... ugh.

Instead, I thought I'd just keep a list of locations that the ant has visited. Then, you can calculate the color of the ant's current location by checking how many times the ant's been there before. However, since the ant's rules are written from the perspective of which way the ant is facing ("turn left" or "turn right"), deciding whether the ant moves up, down, left, or right depends on the last two moves and also the color of the square. This is only mildly annoying to code, but I'm very lazy, so I kept trying to cut down the complexity.

Next, I thought I'd keep a list of move directions, like "uldrurdrd...". This would make calculating the next step easier. Interestingly, with this representation, you don't need to keep a list of positions at all -- all of the information about which squares the ant has visited is encoded in the sequence of moves! To know the color of the current square, count the number of times it has been visited before, which is equal to the number of prefixes of the move sequences where (number of up moves minus number of down moves) and (number of right moves minus number of left moves) are the same as these properties of the whole string. I wrote a (probably buggy) program based on this idea (see end of post).

This got me thinking, though, about the overall problem of the highway conjecture. In this representation, the highway appears as a repeating sequence of (up, down, left, right) moves. This is kind of nice, because it makes it easier to see when the ant has hit the highway; this sequence is kind of like an attractor, or something.

We now have, instead of an ant on a grid, a system for generating the next letter in a sequence. Given a list of letters, the next letter is determined by:
- The last letter
- The parity of the number of substrings with the same properties (u - d) and (r - l) as the overall letter sequence

This system could be generalized in a variety of ways. Using e.g. modulo 3 or 4 instead of parity would add more colors, and it's interesting to me that we could use properties other than (u - d) and (r - l) -- for example, ratios or more complex expressions.

I'm not sure, but I feel like this is incremental progress toward solving the conjecture, which makes the whole thing feel worthwhile :) If I can make more progress, you'll hear about it in a future post.

A final note: Langton's Ant is reversible, so theorems that hold into the future also hold into the past. For example, not only will the ant get arbitrarily far away from its starting point (see wikipedia), it also came from arbitrarily far away if you assume it's been running forever. If the highway conjecture is correct, ants not only eventually build highways, they came from highways, unwinding them from the infinite distance until they got to their starting point! That's kind of neat.

⁂

The program:

function move(ms) {
 possible = ({u:"lr", d:"rl", l:"du", r:"ud", "":"ud"})[ms.slice(-1)];
 x = ms.split("r").length - ms.split("l").length;
 y = ms.split("u").length - ms.split("d").length;
 console.debug(x+", "+y);
 color = 0;
 ms.split("").forEach(function (c) {
  x = x - (c=="r"?1:c=="l"?-1:0);
  y = y - (c=="u"?1:c=="d"?-1:0);
  if (x == 0 && y == 0) color = -color+1; // wrong here to include last character? Does this just invert?
 });
 return ms + possible.charAt(color);
}

Projecting maps by travel time

Maps where something else is used instead of distance or area (e.g. population, GDP, travel time) are called cartograms. Apparently maps where distances correspond to travel times are called linear cartograms, but this seems like kind of a bad name. I'll call them travel-time cartograms instead.

You could think about different parts of the 2D surface of the Earth as having different speeds when you cross them by some mode of travel (trails are easy to walk on, mountains are hard to walk up but easy to walk down, and water can't be walked on at all), and try to make a map that way. The mountain case tells us that when travel time depends on direction, a travel-time cartogram can't be made, i.e. the distance between the top and bottom of a mountain must be two things at once. I guess you could take an average, but I don't like that much -- it seems to destroy or hide a lot of information. Instead, I'll consider different modes of travel, and assume that direction doesn't matter.

I think three modes of travel (plane, car, walking) might be the sweet spot in terms of accuracy vs. difficulty, but two modes of travel is complicated enough to bring out the conceptual issues, and airplanes change our travel time around the world much more than cars do. Airplanes are pretty weird -- do you consider the points along the plane's trajectory to be quickly reachable, or do you imagine the plane disappearing from one airport and then reappearing at the other end? I'll use the time-delayed teleportation model, since I can't really get places by parachuting out of a plane. So, my first-approximation travel-time cartogram should have this property:

The distance between any two points is the minimum travel time by a combination of air travel and "land travel" (a continuous form of travel at 30 miles per hour, a rough average of car and foot travel)

What happens when I try to build this map?

• Major cities and their neighborhoods should be near each other.
• Far from airports, the map should approximate a globe (since only land travel is relevant there).
• Any shortest line between two points (along the surface) should correspond to the shortest trip between them (i.e. it should point-for-point cover the same route as the shortest trip).
• There are points on the surface between the major cities that don't correspond to points on the globe, so that travel between airports isn't immediate, but you also can't parachute out of the planes.

Instead of working with a globe, let's start with a circle (a slice of the sphere, where travellers can move only along the circle between points) and add two airports that can be moved between quickly. What we need to do, it seems to me, is bend the circle through the third dimension until the airports are near one another in 3D space, then add a line between them of length equal to the travel time. It's important to note that distance on this cartogram isn't measured in raw Euclidean terms, but instead by distance along the surface itself (just like on a globe, you measure distance along the surface instead of tunneling through the earth). If you add more airports, then it's like folding the circle up so that many points on its circumference nearly meet.

In fact, if we assume that airplanes all travel at the same speed along this circle, then you can make a separate surface corresponding only to air-travel, with points corresponding to airports and edges corresponding to flights, and this surface will be curved overall like a circle. So, we have a large "land-travel circle" and a smaller, nodes-and-edges "air-travel sphere", and we can make the final map by folding the larger circle through 3D space so that its airports meet the smaller circle's airports.

To get back to the real world, "all you have to do" is make a land-travel globe (which looks like a normal globe), an air-travel "globe" (a smaller web of connections between airports that is overall curved like a sphere), then fold the land-travel globe through the fourth dimension so that its airports meet up with the air-travel globe's points. That's pretty awkward, because now we have a 4D map that is going to be really hard for humans to read and get intuitions about!

To flatten a globe into a map in a way that lets humans understand distances, we sometimes put a grid on the sphere as guidelines for humans. Can we do a similar thing here -- put a grid on our 4D map, cut and flatten it, and then print it out? Not sure, but that seems like what we want to do!

Counterpossibles and contradictory consequences

In a previous post, I proposed formalizing counterpossible reasoning with respect to a deductive system. To counterpossibly assume statement S, we'd add S to the axioms of the proof system P, and modify the inference rules so that any inference yielding not-S yields S instead, giving a modified system PS. I've found a possible issue with this, which I think has implications for counterpossibles more generally, or maybe just torpedoes this specific proposal.

Let's suppose that S is not "really true" -- that we can actually prove not-S in P (which is the interesting case for counterpossibles anyway). S would have some counterpossible consequences -- statements S' that are provable in PS, where not-S' is provable in P. If the only way to prove not-S' is via not-S, then there's no problem, since PS will just prove S instead of not-S, and proceed to prove S' instead of not-S'.

However, if there's another way to prove not-S' in P, a way that doesn't go through S, we have a conflict. P will prove not-S' either via not-S, or via this second path; PS, on the other hand, will prove S' if it goes via S, and will prove not-S' if it goes via the second proof path. (Maybe this would be easier to understand with an example, but I don't have one right now.) So, PS will be able to prove both S' and not-S'. Whoops!

There seem to be at least two options, if we want to stick with the deductive-system view of counterpossibles:

1. A precedence rule: if PS can prove some statement via S or via some other path, then the S-path takes precedence, and the other path is ignored. This has the unfortunate effect of making PS's inference rules "non-local", since conclusions don't just depend on premises, but also on everything else the system can prove.
2. Paraconsistent logic: we can allow PS to prove some statements both true and false, and somehow limit the explosion to make sure that the result isn't a world where every statement besides S isn't both true and false.

Of these two, the second is somehow more appealing to me; it really does seem like counterpossibly assuming S is not "enough" to flip not-S' to S' if there is a way to prove not-S' independent of S. This makes these kind of contradictions seem more like a desirable feature of the deductive-system formalization of counterpossibles than a bug. I would be unsatisfied with this, however, if every counterpossible consequence S' of S became both true and false. I'm not sure, generally, whether most statements in deductive proof systems have many proof pathways (which would be bad news for this method), or whether some systems have some statements that can only be proved in one way.

There seem to be a bunch of paraconsistent logics that I could use, and I don't know anything about the pros and cons, thought I like the idea of rejecting disjunctive syllogism and reductio ad absurdum. Intuitively, I don't think I want to completely limit the explosion; it seems to me that statements "downstream" of S' and not-S' should also be both true and false, but statements "upstream" shouldn't be affected, but I can't say precisely what that means.

⁂

Incidentally, it feels to me like this kind of problem shouldn't affect decision-making programs that need to use counterpossible reasoning. My feeling is that a decision-making system shouldn't be able to figure out that some decision it could make would cause a contradiction, since it "should be in a position" to make any decision it would "like" to. This smells to me a little like free will -- the consequences of a decision-maker's actions irreducibly depend on the action itself, and there aren't proof pathways that circumvent the decision entirely. Maybe that provides a lead on how decision-making programs should use counterpossible reasoning, though I don't know how to cash it out formally.

However, the thoughts above certainly seem to me to be applicable to mathematical counterpossibles, like what "would be true" if 2 = 3 or if root 2 were rational -- in those cases, I think we need to use some paraconsistent logic.

Counterpossibles

I'm casually interested in counterpossible reasoning (or "logical counterfactuals"), asking what would be true if something logically impossible were true. Here's an example due to Carrie Jenkins:

1. If the square root of 2 were rational, it could be expressed as n/m, with n, m integers.
2. If the square root of 2 were rational, it couldn't be so expressed.

It sure seems to me, and to her, that 1 is true and 2 is false. However, most logics don't deal with this sort of thing naturally, i.e. with normal conditionals; if we assume that root 2 is rational, then prove that it is irrational, then we can prove any other statement from this contradiction -- if you build counterpossible worlds this way, they all turn out to be worlds where everything is both true and false.

I'd especially like to know about counterpossible reasoning because it seems like it could be part of a theory of reasonable decision-making. Suppose that a computer program is making a decision; it should evaluate what would happen if it chose option 1, 2, or 3. However, since it is a program, it actually only chooses one of these options, so all but one of these choices are logically false (or maybe they are all false, if the program fails to halt). The program should be using counterpossible reasoning to figure out what would happen if it made each choice.

It seems suggestive to me that the program "doesn't yet know" which choice it will make while it's reasoning, and so it will reason the same way for the choices it will choose and the choices it won't. Maybe this gives us some clue, or limits the ways that it can do counterpossible reasoning? On the other hand, this kind of counterpossible reasoning might be specific to decision-makers, and be unsuitable for e.g. imagining counterpossible mathematical systems like Carrie's root-2-rational world I gave above.

⁂

I have a few desiderata for counterpossible reasoning (which I really haven't done serious reading on, so for all I know these are well-known proposals):

1. There should be exactly one world W defined by counterpossibly assuming S. (A world is a set of assignments of truth values to all statements.)
2. W should assign each statement either "true" or "false", not both or neither.
3. S should be true in W.
4. If S is actually true, then W should just be the normal assignment of truth values to statements.
5. If S is not actually true, then in most cases W should assign other statements S', S'', etc. the opposite of their normal truth values. These are the "counterpossible consequences" of S. All other statements are "counterpossibly independent" of S.

5 is interesting, because it means that we can't go for a W that is minimally different from the actual world in its truth assignments; this would be the world where only S is different, which is not very satisfying. These desiderata clearly aren't enough to pin down a particular way of reasoning; defining 5 better is an obvious next step, but I'm not sure how to do it.

⁂

One possibility that is tempting to me is to work in a proof system P instead of a complete world W (which are different because of incompleteness).  To counterpossibly assume S, add S as an axiom of P, and add a rule to P that says something like "whenever a rule in P says you could conclude not-S, conclude S instead". I think this satisfies 2, since we can never conclude not-S and the proof system is otherwise unchanged. I'm somewhat worried about 4; the mangled proof system seems like it could have trouble with proofs by contradiction, since it can't assume Q and conclude not-S to get a contradiction. This construction would also make statements not provable in P counterpossibly independent of S relative to P, which seems OK to me. Is this construction satisfactory overall? I'm not sure, and I'm out of blogging time for today! Maybe I'll come back to it -- writing this post makes me more excited about the possibility.

I'll leave you with something that seems to me like a nice application of counterpossible mathematical reasoning: