Yeah, I think “computational irreducibility” is an intuitive term pointing to something which is true, important, and not-obvious-to-the-general-public. I would consider using that term even if it had been invented by Hitler and then plagiarized by Stalin :-P
Agreed!
OK, I no longer claim that. I still think it might be true
No, Rice’s theorem is really not applicable. I have a PhD in programming languages, and feel confident saying so.
Let’s be specific. Say there’s a mouse named Crumbs (this is a real mouse), and we want to predict whether Crumbs will walk into the humane mouse trap (they did). What does Rice’s theorem say about this?
There are a couple ways we could try to apply it:
We could instantiate the semantic property P with “the program will output the string ‘walks into trap’”. Then Rice’s theorem says that we can’t write a program Q that takes as input a program R and says whether R outputs ‘walks into trap’. For any Q we write, there will exist a program R that defeats it. However, this does not say anything about what the program R looks like! If R is simply print('walks into trap'), then it’s pretty easy to tell! And if R is the Crumbs algorithm running in Crumb’s brain, Rice’s theorem likewise does not claim that we’re unable tell if it outputs ‘walks into trap’. All the theorem says is that there exists a program R that Q fails on. The proof of the theorem is constructive, and does give a specific program as a counter-example, but this program is unlikely to look anything like Crumb’s algorithm. The counter-example program R runs Q on P and then does the opposite of it, while Crumbs does not know what we’ve written for Q and is probably not very good at emulating Python.
We could try to instantiate the counter-example program R with Crumb’s algorithm. But that’s illegal! It’s under an existential, not a forall. We don’t get to pick R, the theorem does.
Actually, even this kind of misses the point. When we’re talking about Crumb’s behavior, we aren’t asking what Crumbs would do in a hypothetical universe in which they lived forever, which is the world that Rice’s theorem is talking about. We mean to ask what Crumbs (and other creatures) will do today (or perhaps this year). And that’s decidable! You can easily write a program Q that takes a program R and checks if R outputs ‘walks into trap’ within the first N steps! Rice’s theorem doesn’t stand in your way even a little bit, if all you care about is behavior after a fixed finite amount of time!
Here’s what Rice’s theorem does say. It says that if you want to know whether an arbitrary critter will walk into a trap after an arbitrarily long time, including long after the heat death of the universe, and you think you have a program that can check that for any creature in finite time, then you’re wrong. But creatures aren’t arbitrary (they don’t look like the very specific, very scattered counterexample programs that are constructed in the proof of Rice’s theorem), and the duration of time we care about is finite.
If you care to have a theorem, you should try looking at Algorithmic Information Theory. It’s able to make statements about “most programs” (or at least “most bitstrings”), in a way that Rice’s theorem cannot. Though I don’t think it’s important you have a theorem for this, and I’m not even sure that there is one.
Oh sorry, when I said “it might be true” just above, I meant specifically: “it might be true that ‘computational irreducibility’ and Rice’s theorem are the same thing”. But after a bit more thought, and finding a link to a clearer statement of what “computational irreducibility” is supposed to mean, I agree with you that they’re pretty different.
Anyway, I have now deleted all mention of Rice’s theorem, and also added a link to this very short proof that computationally-irreducible programs exist at all. Thanks very much :)
Agreed!
No, Rice’s theorem is really not applicable. I have a PhD in programming languages, and feel confident saying so.
Let’s be specific. Say there’s a mouse named Crumbs (this is a real mouse), and we want to predict whether Crumbs will walk into the humane mouse trap (they did). What does Rice’s theorem say about this?
There are a couple ways we could try to apply it:
We could instantiate the semantic property P with “the program will output the string ‘walks into trap’”. Then Rice’s theorem says that we can’t write a program Q that takes as input a program R and says whether R outputs ‘walks into trap’. For any Q we write, there will exist a program R that defeats it. However, this does not say anything about what the program R looks like! If R is simply
print('walks into trap'), then it’s pretty easy to tell! And if R is the Crumbs algorithm running in Crumb’s brain, Rice’s theorem likewise does not claim that we’re unable tell if it outputs ‘walks into trap’. All the theorem says is that there exists a program R that Q fails on. The proof of the theorem is constructive, and does give a specific program as a counter-example, but this program is unlikely to look anything like Crumb’s algorithm. The counter-example program R runs Q on P and then does the opposite of it, while Crumbs does not know what we’ve written for Q and is probably not very good at emulating Python.We could try to instantiate the counter-example program R with Crumb’s algorithm. But that’s illegal! It’s under an existential, not a forall. We don’t get to pick R, the theorem does.
Actually, even this kind of misses the point. When we’re talking about Crumb’s behavior, we aren’t asking what Crumbs would do in a hypothetical universe in which they lived forever, which is the world that Rice’s theorem is talking about. We mean to ask what Crumbs (and other creatures) will do today (or perhaps this year). And that’s decidable! You can easily write a program Q that takes a program R and checks if R outputs ‘walks into trap’ within the first N steps! Rice’s theorem doesn’t stand in your way even a little bit, if all you care about is behavior after a fixed finite amount of time!
Here’s what Rice’s theorem does say. It says that if you want to know whether an arbitrary critter will walk into a trap after an arbitrarily long time, including long after the heat death of the universe, and you think you have a program that can check that for any creature in finite time, then you’re wrong. But creatures aren’t arbitrary (they don’t look like the very specific, very scattered counterexample programs that are constructed in the proof of Rice’s theorem), and the duration of time we care about is finite.
If you care to have a theorem, you should try looking at Algorithmic Information Theory. It’s able to make statements about “most programs” (or at least “most bitstrings”), in a way that Rice’s theorem cannot. Though I don’t think it’s important you have a theorem for this, and I’m not even sure that there is one.
Oh sorry, when I said “it might be true” just above, I meant specifically: “it might be true that ‘computational irreducibility’ and Rice’s theorem are the same thing”. But after a bit more thought, and finding a link to a clearer statement of what “computational irreducibility” is supposed to mean, I agree with you that they’re pretty different.
Anyway, I have now deleted all mention of Rice’s theorem, and also added a link to this very short proof that computationally-irreducible programs exist at all. Thanks very much :)