[Haskell-cafe] Why is this strict in its arguments?

Andrew Coppin andrewcoppin at btinternet.com
Wed Dec 5 06:56:57 EST 2007


Tillmann Rendel wrote:
> Andrew Coppin wrote:
>> *thinks*
>>
>> Conjecture #1: All nontrivial properties of a computer program are 
>> undecidable in general.
>
> That is the well-known Rice's theorem.

Wait - Rice's *theorem*? So Rice *proved* this?

OMG, I was *right* about something! :-D

>> Conjecture #2: Conjecture #1 is undecidable...
> *thinks more*
>
> But the question wether a nontrivial property of a computer program is 
> decidable is *not* a property of computer programs itself.

Indeed no. And, in fact, if Rice's theorem has been proved, then clearly 
it *is* decidable. And has been decided.

I was merely noting that questions of the form "is X decidable?" are 
usually undecidable. (It's as if God himself wants to tease us...)



More information about the Haskell-Cafe mailing list