Is finding the equivalence of two functions undecidable?

Question

Is it impossible to know if two functions are equivalent? For example, a compiler writer wants to determine if two functions that the developer has written perform the same operation, what methods can he use to figure that one out? Or can what can we do to find out that two TMs are identical? Is there a way to normalize the machines?

Edit: If the general case is undecidable, how much information do you need to have before you can correctly say that two functions are equivalent?

Answer 1

Given an arbitrary function, f, we define a function f' which returns 1 on input n if f halts on input n. Now, for some number x we define a function g which, on input n, returns 1 if n = x, and otherwise calls f'(n).

If functional equivalence were decidable, then deciding whether g is identical to f' decides whether f halts on input x. That would solve the Halting problem. Related to this discussion is Rice's theorem.

Conclusion: functional equivalence is undecidable.

---

There is some discussion going on below about the validity of this proof. So let me elaborate on what the proof does, and give some example code in Python.

1. The proof creates a function f' which on input n starts to compute f(n). When this computation finishes, f' returns 1. Thus, f'(n) = 1 iff f halts on input n, and f' doesn't halt on n iff f doesn't. Python:

   def create_f_prime(f):
       def f_prime(n):
           f(n)
           return 1
       return f_prime
   

2. Then we create a function g which takes n as input, and compares it to some value x. If n = x, then g(n) = g(x) = 1, else g(n) = f'(n). Python:

   def create_g(f_prime, x):
       def g(n):
           return 1 if n == x else f_prime(n)
       return g
   

3. Now the trick is, that for all n != x we have that g(n) = f'(n). Furthermore, we know that g(x) = 1. So, if g = f', then f'(x) = 1 and hence f(x) halts. Likewise, if g != f' then necessarily f'(x) != 1, which means that f(x) does not halt. So, deciding whether g = f' is equivalent to deciding whether f halts on input x. Using a slightly different notation for the above two functions, we can summarise all this as follows:

   def halts(f, x):
       def f_prime(n): f(n); return 1
       def g(n): return 1 if n == x else f_prime(n)
       return equiv(f_prime, g) # If only equiv would actually exist...
   

I'll also toss in an illustration of the proof in Haskell (GHC performs some loop detection, and I'm not really sure whether the use of seq is fool proof in this case, but anyway):

-- Tells whether two functions f and g are equivalent.
equiv :: (Integer -> Integer) -> (Integer -> Integer) -> Bool
equiv f g = undefined -- If only this could be implemented :)

-- Tells whether f halts on input x
halts :: (Integer -> Integer) -> Integer -> Bool
halts f x = equiv f' g
  where
    f' n = f n `seq` 1
    g  n = if n == x then 1 else f' n