Why would total comparison of procedures solve the Halting problem?
I've read that if all procedures could be represented syntactical e.g. in Scheme, then they could be compared structurally using the predicate =, and this would in turn solve the Halting problem.
Having read the ordinary proof why the Halting problem cannot be solved by any Turing machine (by reaching a contradition if such algorithm exists), I still cannot see why the comparison of functions would imply the contrary.
The specific representation of functions doesn't really matter here, so we'll talk about the usual encoding of Turing machines. We denote the encoding of a machine $M$ by $\langle M \rangle$ (if this bothers you, think of it as the scheme code of the function).
Nothing prevents you from comparing two machines syntactically (by comparing the encoding/scheme code as strings). The problem arises when you claim that you have an operator "$=$" which checks whether the functions are equivalent semantically, i.e. give the same result for each input. In the language of Turing machines, this means you can decide the following language:
$L = \left\{\left(\langle M_1\rangle ,\langle M_2 \rangle \right) | L(M_1) = L(M_2)\right\}$
The halting problem can be reduced to the above. Given $\langle M\rangle$ and $w\in \Sigma^*$, ask whether the machine $M_w$ which disregards the input, simulates $M$ on $w$, and accepts, computes the constant $1$ function. Thus, $L$ is not decidable. In fact, it is $\Pi_2^0$ complete, so $L$ is not even semi decidable.
