Turing machine program states are conventionally represented with letters: A, B, C, etc. The starting state is A.
Now suppose you are running a Turing machine program from the beginning. The only state it has visited so far is state A. It runs until it reaches a state that has not been visited yet. What state is it? B? C? D? According to "tree normal form", the name for that next state just is the earliest unused state name, which in this case is B.
Visited states so far are A and B. Run until an unvisited state is reached again. What is its name? C? D? E? Tree normal form says that the state will be called C. And the next newly visited state will be D, etc. In general, the canonical form for a Turing machine program will be the one that puts initial state visits in alphabetical order. (This concept also applies to the multi-color case.)
It's not possible to tell of an arbitrary TM program whether or not that program is in tree normal form. But this proof doesn't look at arbitrary programs. It generates candidate programs by tracing out the normal tree starting from the root, thereby bypassing non-normal programs altogether.
> The most insane python feature is that for loops keep their intermediate variable.
"Insane feature" is a generous way of describing this behavior. I would say it is just a stupid bug that has managed to persist. Probably it is impossible to fix now because of https://xkcd.com/1172/
How typecheckers and linters should deal with this is a tricky question. There is how the language ought to work, and then there is how the language actually does in fact work, and unfortunately they are not the same.
Great post. Some general takeaways for people who want Knuth checks:
1. You are unlikely to find errors in the algorithms themselves, especially if they've been officially published. You might find some infelicities, but these are not counted as full errors. For example, the author here found some confusing-but-not-wrong comments about local variables and unused registers. These are counted as "suggestions" (worth 0x20¢) rather than "errors" (worth 0x$1.00).
2. Knuth is pretty generous with credit -- if your suggestion leads him to find an error, you get credit for the error. The author here said that some defined variables went unused. Knuth pointed out that those variables were in fact used in an exercise. However, in looking this up he noticed a variable-related error in that exercise. Author is credited with 0x$1.00!
3. Exercises are more likely to contain errors and infelicities than the main text. And there are an awful lot of exercises.
4. Knuth includes a whole bunch of stuff in his books that is not related to CS. Lots of weird trivia and references. This stuff is more likely to be wrong than the main text. For example, Knuth mentions "icosahedral objects inscribed with Greek letters" and includes a reference to an article in the Bulletin de l’Institut français du Caire. But the author points out that the article is actually in the Bulletin de l’Institut français d’archéologie orientale. Whoops! 0x$1.00 for you!
> You never understand other people's code as well as your own. No matter how thoroughly you've read it, you've only read it, not written it.
There is certainly some truth to this. On the other hand, it's possible to become blinded to defects in code you've written yourself. You see what you intended for the code to do rather than what it actually does. Reading someone else's code, it can be easier to see what's really going on, since you just see what's there.
For anyone who finds this sort of discussion interesting, I highly recommend reading Chapter 3 of The Structure and Interpretation of Computer Programs. There is quite a bit of philosophical musing about the connection between time and state. For example:
> The basic phenomenon here is that synchronizing different processes, establishing shared state, or imposing an order on events requires communication among the processes. In essence, any notion of time in concurrency control must be intimately tied to communication. It is intriguing that a similar connection between time and communication also arises in the Theory of Relativity, where the speed of light (the fastest signal that can be used to synchronize events) is a fundamental constant relating time and space. The complexities we encounter in dealing with time and state in our computational models may in fact mirror a fundamental complexity of the physical universe.
Looking at some of these screenshots, this is such a fantastic idea that it is surprising it wasn't done earlier. Magit has the perfect interface, why shouldn't everything be like that? Who wants to read the Info manual anyway? Info, Dired, Calc, obviously. Org mode, of course.
Maybe other people have been working separately on similar ideas? Really it is extremely obvious in retrospect that everything should have a Magit style interface. Ultimately, it would be great if that were the default, generally assumed style throughout Emacs. It would be great if all that effort could be coordinated and merged into the main distribution. Built-in, no external packages.
Well said. The Magit interface is such a pleasure to use, sometimes I will modify and rearrange commits just for fun. A Magit-style interface for Calc seems like a great idea.
> We are selecting for the maximally pathological machines.
This is not quite right. We're selecting for maximally long-running (or mark-producing, etc) programs. Whether those programs turn out to be "pathological" in some sense is an open question, and a question that can only be answered (to a limited extent) by observing and analyzing actual champion machines. Apriori, there's nothing we can say about what a champion program will do or what its code will be like. The Spaghetti Code Conjecture says that these champion programs will tend to be complicated. I have argued in the past that this may not be the case. It's entirely possible that the code of a champion program will be written more or less straightforwardly, and its long-running-ness comes from executing some bizarre and exotic mathematical function.
Actually, I think the more likely outcome is that some champions will be spaghetti and some will be clean. If they were all spaghetti or all clean, then that fact could be exploited to speed up the search process by discarding all programs not matching the property. And that sounds too good to be true, so it probably isn't. Maybe BB(8) champion is clean, BB(9) is spaghetti, etc, and there are no reliable trends.
Busy Beaver champion programs are said to run for super-exponentially many steps. But nobody has actually run their simulators for that many steps. Instead, simulators can prove tape fast-forwarding rules. Basically, you look for repeating tape patterns. If you can prove the pattern is correct, then you can apply that transformation again if some tape circumstance shows up again.
For example (using run-length encoding),
1^n 0 1^m
might become
1^(n-1) 0 1^(m+2)
When the rule is applied, the transformation is applied directly to the tape, generally by manipulating some count variables.
Now, how many machine steps does it take to apply this transformation? Well, TBH I'm not really sure. It seems kinda complicated, especially when the rules get more elaborate. If you are trying to run your simulator as fast as possible, you probably don't want to bother calculating it at all anyway, since you can always rerun the analysis at a more leisurely pace later.
So when I say that marks are "more practically important", I mean that marks are central to the operation of advanced simulators, whereas steps are a derived afterthought value.
Logically, the steps are more important, since they give you an easy method for solving the halting problem for the state/color class.
So far, the markiest programs are also the steppiest. My conjecture is that they will turn out to be different in infinitely many classes. If they were always the same, you would be able to get the logical primacy of steps just from working with marks. And that sounds too good to be true.
> They have used a proof generator based on a logical theory...
I don't understand your scenario. If they're using a proof generator, that sounds like the opposite of intuiting or using the human mind. Maybe they used "intuition" to come up with new axioms for a logical theory, but that is not the same as determining of some particular concrete TM program whether or not it halts.
> past BB(3), there isn't any known size where the champion machines for Σ(n) and S(n) are different.
My feeling is that this trend cannot continue forever, and for infinitely many N they are different. If they are always the same, then you could find the steps champion just by finding the marks champion. This would be convenient, because as you pointed out, steps are more logically important, while marks are more practically important. But this feels too good to be true, and so it probably isn't.
Congratulations to the team! So the (blank tape) halting problem is solved for 5-state 2-color Turing machine programs. Has anyone tried applying these same techniques to the 2-state 4-color case? That seems like it would probably be tractable, although generally speaking colors are more powerful than states, so there might be some surprises there. (6-state 2-color and 2-state 5-color both seem intractable, perhaps even provably so.)
By the way, there is an extremely stupid but disturbingly widespread idea that humans are able to just intuit solutions to the halting problem, using the mind's eye or quantum mechanics in the brain or whatever. Needless to say, this did not factor into the proof.
> Let me state that without my notes Shade's text simply has no human reality at all, since the human reality of such a poem as his ... has to depend entirely on the reality of its author and his surroundings, attachments and so forth, a reality that only my notes can provide. To this statement my dear poet would probably not have subscribed, but, for better or worse, it is the commentator who has the last word.
Final exam questions:
1. To what extent did Nabokov agree or disagree with this approach to literary criticism?
2. Did Nabokov personally identify more with Shade or with Kinbote?
I agree completely, all of these kinds of conjectures are shaped by what is detectable. If there are any "dark matter" programs out there, they by definition will be difficult to find. That said, I find it entirely plausible that the champions will win by exploiting complex and exotic mathematical facts, while the implementations of the math do not themselves need to be complex or exotic at the code level.
Invoke with:
Possibly relies too much on awk + sed. So maybe not A+, but better than nothing.