# [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