[plt-scheme] Check for function equality?

OT for plt-scheme, but I actually know something about the subject for a 
change.

Bill Wood wrote:

> This brings up an interesting question.  We know that there is no
> decision procedure for First-Order Predicate with Equality, but
> Herbrand's Theorem tells us there is a semi-decision procedure, that is,
> there is a procedure that halts on any theorem saying "it's a theorem",
> but some non-theorems cause it to spin.  Is there anything analogous for
> the Halting Problem or function equivalence, or are we in a situation
> like Second-Order Predicate Calculus which has no semi-decision
> procedure because any such could be used to build a decision procedure
> for FOPC?

Having a "semi-decision procedure" is known as "recursively enumerable" 
in computability theory. The set of programs that halts is r.e., because 
the semi-decision procedure is just running the program! But the set of 
pairs of equivalent functions is not r.e., and neither is the set of 
pairs of non-equivalent functions. (See the books that Jos and I cited 
-- he pointed at a still-earlier version of the one I mentioned -- that 
provide the basic techniques for proving such results.)

To look at it another way, there are levels of uncomputability. If you 
were given a bottle containing a genie who could solve the halting 
problem, could you compute all functions? No, because the same proof 
adapted will demonstrate that the halting problem for programs with 
genies is uncomputable. There is a whole theory of classes of 
uncomputable problems and their relationships, which is still computer 
science, but somewhat removed from the concerns of this list (except to 
the extent that we naively wish at times to solve problems in such 
classes, and must learn to make do with approximations or heuristics). --PR