I previously asked if it's decidable whether two primitive recursive functions are equivalent: "primitive recursive functional equivalence". The answer was no.
Here is my followup. What is the most powerful class of functions where it can generally be decided if two functions are equivalent? That is, a function can be written such as
areEqual :: fun1 -> fun2 -> Bool. By equivalent I do not mean the same algorithm but the same relation between domain and codomain.
In another question I asked if lower elementary recursion was equivalent to deterministic push down automata: "Relation of deterministic push down automata and lower elementary recursion". The answer was no, and that my thought process was wrong. My hope was that this would show that polynomial time functions (lower elementary) could be proven equivalent.
This question is in relation to what class of recursion, not machine. As such deterministic pushdown automata is not what I am looking for. If I understand the answers to my second question correctly the automata do not necessarily translate to a class of recursive functions.
I have been poking at this question for a while in a round about way probing for an answer.
The problem is intuitively solvable for simple problems. For example the
even? function could be implemented in a mutual recursive manner with
odd? or from
mod 2. These two ways do the same thing. The question is in relation to the highest class of functions where this is possible.