If a machine H that can decide the halting problem is defined as H = (P -> X -> Y) -> X -> Boolean where P is the type of the program, X is the type of the input that the program accepts, and Y is the type of the output of the program, and then we define H' to be H but if the result is true we loop forever and if the result is false we return false, then feed H' into itself like so H' H' H' then the type signature would be ((P -> X -> Y) -> X -> Boolean) ((P -> X -> Y) -> X -> Boolean) and so X must be of type ((P -> X -> Y) -> X -> Boolean) but we are using X in its own definition and so there is infinite recursion.
You made a small mistake. We need quote or eval to move between levels.
Halts : Prg -> Bool "Halts" : Prg Liar : Prg -> Bool Liar x = If halts x rhen loop else halt Para = liar "liar"
Name:
Anonymous2016-06-23 4:04
>>3 But you are missing the input. The decision is whether the program will halt on a given input, not whether the program will halt without any input.