
> 
> Set D : Set of decision algorithms
>  X∈D if and only if
> 
> 
> 1. X is an Turing machine algorithm with finite length
> 2. takes one input i, binary number
> 3. X(i)=0 or X(i)=1 or X(i) runs forever
> 
> 
> 


Definition: equivalent  

Algorithm X∈D and Y∈D are equivalent if and only if
 For all i  

 X(i) =1 ⇔ Y(i)=1
 and 
 X(i) =0 ⇔ Y(i)=0



> 
> Definition: equivalent checker
> 
> 
> Algorithm H is equivalent checker if and only if
>  For all X∈D, for all Y∈D  
> 
>  X and Y are not equivalent algorithms → H( X , Y) = 1  
> 
>  X and Y are equivalent algorithms → H( X , Y) = 0 
> 
> 
> 


My Question: Equivalent checker H does exist?



existence of equivalence checking algorithm
There is no computable equivalence checker. The reason is that if there were, we could solve the halting problem, as follows: given a Turing machine program $p$ and input $x$, design another program $X$ that on any input $i$ first runs $p$ on $x$, and if this halts, then outputs $1$. So $X$ is equivalent to the always-output-$1$ program if and only if $p$ halts on input $x$. So if we could compute equivalence, then we could decide the halting problem. 


But now I claim more, that the equivalence problem is actually strictly harder than the halting problem. Thus, even if you had an oracle for the halting problem, you still couldn't compute whether two programs are equivalent. 


**Theorem.** The equivalence problem is $\Pi^0\_2$-complete. Thus, it is Turing equivalent to the double jump $0''$, or in other words, to the halting problem relativized to an oracle for the halting problem. 


Proof. First, note that the equivalence of two programs $p$ and $q$ is a $\Pi^0\_2$ assertion, since they are equivalent just in case $\forall i\forall s\exists t$ (if $p(i)$ halts in $s$ steps, then $q(i)$ halts in $t$ steps, with the same output, and vice versa). This assertion has complexity $\Pi^0\_2$. One can restrict to the class of decision problems, as in the question, without increasing complexity, since it is a $\Pi^0\_1$ assertion about a program $p$ to say that it is a decision problem program, namely, assert that every halting computation according to $p$ gives output either $0$ or $1$. 


Conversely, suppose that $\forall n\exists k\varphi(n,k)$ is a given $\Pi^0\_2$ assertion, where $\varphi$ has only bounded quantifiers. Let $p$ be the program which on input $n$ searches for a value of $k$ for which $\varphi(n,k)$, and outputs $1$ when such a $k$ is found. Thus, this program is equivalent to the always-output-$1$ program just in case the given $\Pi^0\_2$ assertion is true. So we can computably reduce instances of $\Pi^0\_2$ truth to the equivalence problem, and so the equivalence problem is $\Pi^0\_2$-complete. QED


