bounding brokenness

Dr. Seuss and the halting problem

The unsolvability of the halting problem is a well-known fundamental result which says that it’s impossible to write an algorithm that determines if an arbitrary program halts given some input. It also implies a lot of other things – including, for example, that there’s no general way to determine whether a particular variable in a program has a particular value at a point, and famously, that every consistent formal system powerful enough to do arithmetic in will have unprovable statements.

I’m not going to talk much about it, though – instead I’m going to direct you to this extraordinary proof, written in verse, in the style of Dr. Seuss. It’s called Scooping the Loop Snooper, and it was written by Geoffrey K. Pullum, who you might also know from posts at the Language Log. Wow.