I was just told that the equality of computable functions of type <m>\{0,1\}^\omega\rightarrow\omega</m> is decidable. I was a bit confused about this at first, since trivially, the equality of functions <m>\omega\rightarrow\omega</m> is undecidable: Let <m>[.]</m> be the a complete enumeration of all proofs in our meta-theory <m>T</m>, then define <m>g(n)=\left\{\begin{array}{l} 1 \mbox{ if } [n] \mbox{ proves }\bot \\ 0 \mbox{ otherwise}\end{array}\right.</m>, then by Gödel's second incompleteness theorem, we cannot decide whether <m>g=\lambda_n0</m>.
However, even though the question whether two computable functions <m>\{0,1\}^\omega\rightarrow\omega</m> are equal seems harder than the same question for <m>\omega\rightarrow\omega</m>, 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 <m>\{0,1\}^\omega</m>.
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 <m>f:\{0,1\}^\omega\rightarrow\omega</m> be given, and <m>a=(a_i)_i\in\{0,1\}^\omega</m>. Then there is some initial subsequence <m>b=(b_i)_{i<n}</m> of <m>a</m>, such that for all sequences <m>c</m>, <m>f(b*c)=f(a)</m>.
Proof: A terminating turing machine can, for every given sequence <m>a</m>, only read finitely many elements of <m>a</m>, thus, there is an upper bound <m>m\in\omega</m> such that the program is only dependent of elements <m>a_{j<m}</m>. Set <m>n=m</m> and <m>(b_i)_{i<n} = (a_i)_{i<m}</m>. Then <m>f(b*c)=f(a)</m> for all sequences <m>c</m>, since the program does not depend on an elements not in <m>b</m>.
We say that a computable <m>f</m> depends only on a sequence <m>a=(a_i)_{i<n}</m> when for every <m>c_1,c_2</m> we have <m>f(a*c_1)=f(a*c_2)</m>, and it depends exactly on <m>a=(a_i)_{i<n}</m> when it depends only on <m>(a_i)_{i<n}</m> but this is not the case for subsequences <m>(a_i)_{i<m},m<n</m>.
By Lemma 1 it is trivial to proof that two functions <m>f,g</m> are not equal: Just find a sequence <m>a</m> on that both of them depend only, and for which <m>f(a)\neq g(a)</m>. The more interesting part is the case when they are equal.
Using Lemma 1, we can encode such functions <m>f</m> in the following way: Let <m>(A_i)_{i\in\omega}</m> be predicate constants, and denote by <m>PA</m> the first-order Peano arithmetic. If <m>f(a)=k</m> where <m>f</m> depends only on <m>(a_i)_{i<m}</m>, then let <m>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</m>, where <m>c</m> is a term constant, and <m>k</m> can be expressed in the form <m>S(\ldots S(0))</m> as usual. Now define <m>Mod_{f,c} := PA \cup \{ M_{f,a,c} | a \in \{0,1\}^\omega\}</m>. Obviously, <m>f(a)=k \Leftrightarrow (Mod_{f,c}[A_i:\Leftrightarrow(a_i=1)]\models c=k)</m>. Now, if two functions <m>f,g</m> are equal, we know that <m>PA\cup Mod_{f,c}\cup Mod_{g,d}\cup \{c\neq d\}</m> is not satisfiable, and therefore, <m>PA\cup Mod_{f,c}\cup Mod_{g,d}\cup \{c\neq d\}\models\bot</m>. By the completeness theorem, we therefore know that <m>PA\cup Mod_{f,c}\cup Mod_{g,d}\cup \{c\neq d\}\vdash\bot</m>, and hence, the equality <m>f=g</m> is provable.
Nice.
However, even though the question whether two computable functions <m>\{0,1\}^\omega\rightarrow\omega</m> are equal seems harder than the same question for <m>\omega\rightarrow\omega</m>, 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 <m>\{0,1\}^\omega</m>.
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 <m>f:\{0,1\}^\omega\rightarrow\omega</m> be given, and <m>a=(a_i)_i\in\{0,1\}^\omega</m>. Then there is some initial subsequence <m>b=(b_i)_{i<n}</m> of <m>a</m>, such that for all sequences <m>c</m>, <m>f(b*c)=f(a)</m>.
Proof: A terminating turing machine can, for every given sequence <m>a</m>, only read finitely many elements of <m>a</m>, thus, there is an upper bound <m>m\in\omega</m> such that the program is only dependent of elements <m>a_{j<m}</m>. Set <m>n=m</m> and <m>(b_i)_{i<n} = (a_i)_{i<m}</m>. Then <m>f(b*c)=f(a)</m> for all sequences <m>c</m>, since the program does not depend on an elements not in <m>b</m>.
□
We say that a computable <m>f</m> depends only on a sequence <m>a=(a_i)_{i<n}</m> when for every <m>c_1,c_2</m> we have <m>f(a*c_1)=f(a*c_2)</m>, and it depends exactly on <m>a=(a_i)_{i<n}</m> when it depends only on <m>(a_i)_{i<n}</m> but this is not the case for subsequences <m>(a_i)_{i<m},m<n</m>.
By Lemma 1 it is trivial to proof that two functions <m>f,g</m> are not equal: Just find a sequence <m>a</m> on that both of them depend only, and for which <m>f(a)\neq g(a)</m>. The more interesting part is the case when they are equal.
Using Lemma 1, we can encode such functions <m>f</m> in the following way: Let <m>(A_i)_{i\in\omega}</m> be predicate constants, and denote by <m>PA</m> the first-order Peano arithmetic. If <m>f(a)=k</m> where <m>f</m> depends only on <m>(a_i)_{i<m}</m>, then let <m>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</m>, where <m>c</m> is a term constant, and <m>k</m> can be expressed in the form <m>S(\ldots S(0))</m> as usual. Now define <m>Mod_{f,c} := PA \cup \{ M_{f,a,c} | a \in \{0,1\}^\omega\}</m>. Obviously, <m>f(a)=k \Leftrightarrow (Mod_{f,c}[A_i:\Leftrightarrow(a_i=1)]\models c=k)</m>. Now, if two functions <m>f,g</m> are equal, we know that <m>PA\cup Mod_{f,c}\cup Mod_{g,d}\cup \{c\neq d\}</m> is not satisfiable, and therefore, <m>PA\cup Mod_{f,c}\cup Mod_{g,d}\cup \{c\neq d\}\models\bot</m>. By the completeness theorem, we therefore know that <m>PA\cup Mod_{f,c}\cup Mod_{g,d}\cup \{c\neq d\}\vdash\bot</m>, and hence, the equality <m>f=g</m> is provable.
Nice.
Jetzt kommentieren