|
|
|
|
|
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. |
|