Name: Anonymous 2016-06-23 2:47
If a machine H that can decide the halting problem is defined as
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
then the type signature would be
and so X must be of type
but we are using X in its own definition and so there is infinite recursion.
Can someone explain this?
H = (P -> X -> Y) -> X -> Booleanwhere 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.
Can someone explain this?