Bitte was?

Equality of computable functions from boolean sequences to natural numbers is decidable
Sun, 17 Apr 2011 13:00:00 GMT

I was just told that the equality of computable functions of type \{0,1\}^\omega\rightarrow\omega is decidable. I was a bit confused about this at first, since trivially, the equality of functions \omega\rightarrow\omega is undecidable: Let [.] be the a complete enumeration of all proofs in our meta-theory T, then define g(n)=\left\{\begin{array}{l} 1 \mbox{ if } [n] \mbox{ proves }\bot \\ 0 \mbox{ otherwise}\end{array}\right., then by Gödel's second incompleteness theorem, we cannot decide whether g=\lambda_n0.

However, even though the question whether two computable functions \{0,1\}^\omega\rightarrow\omega are equal seems harder than the same question for \omega\rightarrow\omega, it is not. A first step in understanding why is maybe that every terminating algorithm is finite, and therefore can only use finitely many elements of a sequence in \{0,1\}^\omega.

Of course, having this information without any proofs I tried to prove it myself. I noticed that this should be strongly related to the compactness theorem. And here is the outcome:

Lemma 1: Let a computable f:\{0,1\}^\omega\rightarrow\omega be given, and a=(a_i)_i\in\{0,1\}^\omega. Then there is some initial subsequence b=(b_i)_{i<n} of a, such that for all sequences c, f(b*c)=f(a).
Proof: A terminating turing machine can, for every given sequence a, only read finitely many elements of a, thus, there is an upper bound m\in\omega such that the program is only dependent of elements a_{j<m}. Set n=m and (b_i)_{i<n} = (a_i)_{i<m}. Then f(b*c)=f(a) for all sequences c, since the program does not depend on an elements not in b. ‏
□‎


We say that a computable f depends only on a sequence a=(a_i)_{i<n} when for every c_1,c_2 we have f(a*c_1)=f(a*c_2), and it depends exactly on a=(a_i)_{i<n} when it depends only on (a_i)_{i<n} but this is not the case for subsequences (a_i)_{i<m},m<n.

By Lemma 1 it is trivial to proof that two functions f,g are not equal: Just find a sequence a on that both of them depend only, and for which f(a)\neq g(a). The more interesting part is the case when they are equal.

Using Lemma 1, we can encode such functions f in the following way: Let (A_i)_{i\in\omega} be predicate constants, and denote by PA the first-order Peano arithmetic. If f(a)=k where f depends only on (a_i)_{i<m}, then let M_{f,a,c}:=(\bigwedge\limits_{a_i=1,i<m} A_i \wedge \bigwedge\limits_{a_i=0,i<m} \lnot A_i)\leftrightarrow c=k, where c is a term constant, and k can be expressed in the form S(\ldots S(0)) as usual. Now define Mod_{f,c} := PA \cup \{ M_{f,a,c} | a \in \{0,1\}^\omega\}. Obviously, f(a)=k \Leftrightarrow (Mod_{f,c}[A_i:\Leftrightarrow(a_i=1)]\models c=k). Now, if two functions f,g are equal, we know that PA\cup Mod_{f,c}\cup Mod_{g,d}\cup \{c\neq d\} is not satisfiable, and therefore, PA\cup Mod_{f,c}\cup Mod_{g,d}\cup \{c\neq d\}\models\bot. By the completeness theorem, we therefore know that PA\cup Mod_{f,c}\cup Mod_{g,d}\cup \{c\neq d\}\vdash\bot, and hence, the equality f=g is provable.

Nice.