Hacker News new | ask | show | jobs
by colanderman 3318 days ago
"Undecidability" doesn't apply to interactive systems. Inputs must be finite: https://en.wikipedia.org/wiki/Undecidable_problem In your example, the input (an infinite stream of strings not equal to "Ralph") is not finite.

Instead, think of an interactive system as a finite state machine. The question to ask then is, do any of my state transitions require a Turing-complete language to express? In 99.999% of all software ever written the answer is "no". Inability to prove termination is almost certainly a software bug or flaw in the design. The theoretical exceptions are exotic algorithms for which termination is not provable; the practical exceptions are probabilistic algorithms for which termination is not in fact guaranteed (e.g. a naïve hash table implementation).

The difference is important. A state machine, even one that represents a non-terminating system over infinite input (e.g. a web server), still can be reasoned about. This is exactly the domain of tools like TLA+, which can answer questions such as, "is my system guaranteed to always eventually take action X given input Y?" and "is my system guaranteed to never terminate?" But to be able to answer such questions, it's a prerequisite that the transitions between states do in fact terminate.

1 comments

It's not a given that the input is infinite. If the used types in "Rob" then goes away forever, the program will neither terminate nor process an infinite number of non-"Ralph" strings. It will sit just sit there waiting (possibly in a loop, possibly not) for a hardware interrupt that will never arrive.
For decidability to apply, the input needs to be known a priori in its entirety. Decidability is a mathematical statement about natural numbers (or any other countably infinite set); it has absolutely nothing to do with "paused" input or any notion of "interactivity".

The type of behavior you're concerned with does on the other hand fall squarely in the realm of temporal logics (e.g. TLA+), which do concern themselves with interactivity and indeterminate pauses. For example, the statement "so long as the user eventually inputs the string 'Ralph', the algorithm eventually terminates" is decidable for any finite state machine.

In other words, if you limit your interactivity logic to that expressible by a finite state machine with decidably halting transitions, congratulations, you are writing decidably halting programs, even though they don't "halt" in the temporal sense. It's always possible to tell whether they will halt for a given input by completely analyzing the state space.

Isn't this a question of upper-bound on input? Not specific examples that are less than the upper bound..