[Kranar]

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]

Okay, 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]

You 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

[6gvONxR4sf7o]

I certainly do feel like I understand it better now. Thanks again for the pointers!

[6gvONxR4sf7o]

Ah, thanks for spelling it out with the typescript. That’s clearer to me now!