Maximal class for which function equivalence is decidable

Question

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.

Answer 1

There is no such maximal class.

Proof: suppose that there is a class $C$ of representations of total functions for which function equivalence is decidable. If $C$ is finite, then $C$ augmented with the constant function that returns $\max\{\overline{f_i}(0)\} + 1$ (which by construction is not in $C$) has decidable function equivalence (test the function at $0$ then apply the postulated decision algorithm). If $C$ is infinite, it is denumerable (because representations of functions are denumerable¹), so let $(f_i)_{i\in\mathbb{N}}$ be an enumeration of all function representations in $C$. Let $G(i) = \overline{f_i}(i) + 1$ (a classic diagonal construction). By construction, $G$ does not have a representation in $C$ (because $\forall i, g_i(i) \ne h(i)$). Let $g$ be a representation of a function that calculates $G$ (this is doable in any Turing-equivalent framework). The algorithm that reports that $g$ is distinct from any member of $C$, and otherwise applies the existing decision algorithm for $C$, is an equivalence decision procedure for $C \cup \{g\}$.

Any class of function representations with decidable equivalence can be augmented to a larger such class. Therefore there is no maximal class.

Intuitively speaking, if you have two classes of functions with decidable equivalence, you can apply the two decision algorithms inside each class, but it's not necessarily possible to compare two functions from different classes. And if you have an infinite set of classes, with a decision procedure for each, then even calculating which decision procedure to use is not necessarily doable.

¹ _{The set of all functions is not denumerable, but whatever representation of functions you choose (e.g. source code in some language), the set of inputs for your decision algorithm is denumerable.}