This is basically the explanation I came up with by the end of the post; that I wouldn’t necessarily know if I just hadn’t simulated the billiard balls far enough. It’s much easier for me to understand that there’s no way to prove in general for all programs that the billiard balls find themselves in a particular state ever; at least, that sounds like a much harder problem so I’m much more comfortable writing it off as unsolvable.
Watching the video now. Interesting turns of phrase this speaker’s got.
Also, a “nontrivial semantic property” is captured by testing membership in a set of partial computable functions (which isn’t the empty set or the set of all computable functions). Note that testing what function the Turing machine is implementing automatically sidesteps syntactic checks. For example, I could just want to check whether the program implements the constant-zero function, but Rice’s theorem says I can’t check this for all programs!
Because if I could, then I could find out whether machine M halts on input x. Do you see how? Do you see how the proof fails if the property in question is trivial?
This is basically the explanation I came up with by the end of the post; that I wouldn’t necessarily know if I just hadn’t simulated the billiard balls far enough. It’s much easier for me to understand that there’s no way to prove in general for all programs that the billiard balls find themselves in a particular state ever; at least, that sounds like a much harder problem so I’m much more comfortable writing it off as unsolvable.
Watching the video now. Interesting turns of phrase this speaker’s got.
Also, a “nontrivial semantic property” is captured by testing membership in a set of partial computable functions (which isn’t the empty set or the set of all computable functions). Note that testing what function the Turing machine is implementing automatically sidesteps syntactic checks. For example, I could just want to check whether the program implements the constant-zero function, but Rice’s theorem says I can’t check this for all programs!
Because if I could, then I could find out whether machine M halts on input x. Do you see how? Do you see how the proof fails if the property in question is trivial?