# SICP Solutions

### Chapter 4, Metalinguistic Abstraction

#### Exercise 4.15

Let’s first see the code again:

(Knowing how to structure a proof, that I learned from book How to prove it helps)

Let’s assume that such a program halts? is possible. Thus it means that this procedure halts? can also tell whether (try try) halts or not!

Now, we evaluate (try try).

Assume that (halts? try try) returns true.

Thus (run-forever) executes and program goes into infinite loop. Thus (try try) does not terminate. But halts? says (try try) terminates by returning true! It follows that our assumption that (halts? try try) returned true is wrong.

So, let’s assume that (halts? try try) returns false.

Thus 'halted is printed and thus (try try) terminates. But halts? says (try try) does not terminate! Or our assumption is wrong again!

That means halts? can neither return true and nor it can return false for procedure try!

It follows that such program halts? that can tell weather any program halts or not is impossible.

One important thing to focus here:

This only proves that such procedure halts? is not possible for every program. There can be halts? procedure that can work for specific programs!

Since this marks the end of a sub-section and many new things have been added in the simulator as part of exercises. I think I shall put the complete code here till now:

(note that evaluator does not use data driven approach for application? procedure but apart from this every exercise is built on top of the previous changes in the evaluator as part of previous exercies).