3 ms·
Define P(A, S) as the function that takes as input an algorithm A and a string S and returns true if A(S) halts, and false if A(S) does not halt. The claim is t
by Kranar 5y ago
Define P(A, S) as the function that takes as input an algorithm A and a string S and returns true if A(S) halts, and false if A(S) does not halt. The claim is that P does not exist.
Assume P exists, let Q(S) be the function that takes a string S and halts if P(Q, S) returns false, otherwise it loops forever. Q(S) is not some whacky function either, in TypeScript it could be implemented as follows:
function P(A: (S: string) => void, S: string): boolean;
function Q(S: string): void {
if(P(Q, S)) {
while(true) {}
}
}
But then you have the following contradiction:
If P(Q, S) returns false, then that implies Q(S) runs forever, but by definition Q(S) halts when P(Q, S) returns false, so P was incorrect about Q(S).
If P(Q, S) returns true, then that implies Q(S) halts, but by definition Q(S) loops forever when P(Q, S) returns true, so P was incorrect about Q(S).
This exhausts all possibilities, hence our assumption that there is such a P must be false.
- 6gvONxR4sf7o 5y agoAh, thanks for spelling it out with the typescript. That’s clearer to me now!
- 6gvONxR4sf7o 5y agoOkay, you got me thinking about this more generally, and it seems like this sort of proof can disprove all sorts of checkers: function HasPropertyX(A: (S: string) => void, S: string): boolean; function Q(S: string): void { if(HasPropertyX(Q, S)) { AvoidHavingX(); } else { HaveX(); } } For example, no program can exist that checks whether another program raises an exception on some argument (pseudocode, since I don't really know typescript): function RaisesException(A: (S: string) => void, S: string): boolean; function Q(S: string): void { if(RaisesException(Q, S)) { pass; } else { raise Exception; } } and no program can exist that determines whether a given bit of code blows up the planet: function BlowsUpThePlanet(A: (S: string) => void, S: string): boolean; function Q(S: string): void { if(BlowsUpThePlanet(Q, S)) { pass; } else { HitTheBigRedButtonAndGoKaboom(); } } and you can't even test whether f(x) is true: function ReturnsTrue(A: (S: string) => boolean, S: string): boolean; function Q(S: string): boolean { return not ReturnsTrue(Q,S); } It seems like it any property you can exhibit in HaveX cannot be checked for, leading me to think that this is a proof that you can't definitively check for pretty much anything in programs, but that seems too far. Am I getting this right? How far does this go? Is there a deeper theorem about the limitations of program checking that brings this all together?
- Kranar 5y agoYou are absolutely correct and you have discovered Rice's Theorem [1]. The fact that you generalized the halting problem on your own is a very good indication that you fundamentally understand it. [1] https://en.wikipedia.org/wiki/Rice%27s_theorem https://en.wikipedia.org/wiki/Rice%27s_theorem
- 6gvONxR4sf7o 5y agoI certainly do feel like I understand it better now. Thanks again for the pointers!