# Maximal class for which function equivalence is decidable

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.

• It may not be helpful to talk about programs. As soon as you have Turing-complete syntax/semantics, this property is not decidable by the theorem of Rice. You need weaker models of computation. Finite automata, for instance, have decidable equivalence, as do some flavors of Petri nets iirc. – Raphael Mar 9 '16 at 12:23

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\}$.