sicp-ex-4.15

meteorgan

  
  
  
 assuming procedure try can halt, when execute (try try), (halt? try try) will be true, but the procedure will run forever. if procedure try can't halt. (halt? try try) will be false, but the procedure will halt.

Iain

This is proof by contradiction, where we assume the opposite of what we want to prove and show that it is logically inconsistent.

If we call (try try) then we get the following (with try substituted in for p)

 (define (try try) 
   (if (halts? try try) 
       (run-forever) 
       'halted))

We observe that if (halts? try try) is True then (try try) will run forever, which is a contradiction. The converse, if (halts? try try) if False then (try try) returns 'halted, could also be used to reach a contradiction.