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?
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: s…
function HasPropertyX(A: (S: string) => void, S: string): boolean;
function Q(S: string): void {
if(HasPropertyX(Q, S)) {
AvoidHavingX();
} else {
HaveX();
}
}
function RaisesException(A: (S: string) => void, S: string): boolean;
function Q(S: string): void {
if(RaisesException(Q, S)) {
pass;
} else {
raise Exception;
}
}
function BlowsUpThePlanet(A: (S: string) => void, S: string): boolean;
function Q(S: string): void {
if(BlowsUpThePlanet(Q, S)) {
pass;
} else {
HitTheBigRedButtonAndGoKaboom();
}
}
function ReturnsTrue(A: (S: string) => boolean, S: string): boolean;
function Q(S: string): boolean {
return not ReturnsTrue(Q,S);
}
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?