[6gvONxR4sf7o]

I don’t follow this proof. If Q takes an executable program, then Q(x) is executable, but Q alone isn’t. So you can ask questions about Q(Q(x)), but Q(Q) shouldn’t type check, as the inner Q isn’t executable without an argument. Am I being dumb? How would you do this proof with types?

[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!

[enedil]

Well, if you know anonymous function, it should be easy to understand what happens. Functions are first-class objects here. Q is a procedure that takes an arbitrary procedure. It's not that you run the procedure. In fact, it's another way around, you want to say something about the source code of the function, not the result of applying it.