I was just told that the equality of computable functions of type
![\{0,1\}^\omega\rightarrow\omega](/latex?n=96f29e13ce423c7944ad55bfdf52da3e2c84f3cd6653e4c09d1c77e8166b3306)
is decidable. I was a bit confused about this at first, since trivially, the equality of functions
![\omega\rightarrow\omega](/latex?n=631daa7f89f3c4adedfe6971cf0c06eb380bf2aa1ddb592e8d6a0f1531230872)
is undecidable: Let
![[.]](/latex?n=09b46f550cd3dadb8caf3fd5f4d355ddb4f344bc9e6378d65c711a805132780f)
be the a complete enumeration of all proofs in our meta-theory
![T](/latex?n=e632b7095b0bf32c260fa4c539e9fd7b852d0de454e9be26f24d0d6f91d069d3)
, then define
![g(n)=\left\{\begin{array}{l} 1 \mbox{ if } [n] \mbox{ proves }\bot \\ 0 \mbox{ otherwise}\end{array}\right.](/latex?n=e3c9910da49aff4cbdb67c8b248fc1a96a2d64f7cb803c19333713b152848c28)
, then by Gödel's second incompleteness theorem, we cannot decide whether
![g=\lambda_n0](/latex?n=b8eff3f5f6d7d8939744059f006f7972e1131c12a1de6c53b267361023acbf18)
.
However, even though the question whether two computable functions
![\{0,1\}^\omega\rightarrow\omega](/latex?n=96f29e13ce423c7944ad55bfdf52da3e2c84f3cd6653e4c09d1c77e8166b3306)
are equal seems harder than the same question for
![\omega\rightarrow\omega](/latex?n=631daa7f89f3c4adedfe6971cf0c06eb380bf2aa1ddb592e8d6a0f1531230872)
, 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](/latex?n=aacf384e5f6fc371c28700fcd377524991a3e1f5eda2cec59bb58e100b94d013)
.
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](/latex?n=b033fbb74216603b9289da39547c7e722e65a25faa1660bacc87a76ba6fef26b)
be given, and
![a=(a_i)_i\in\{0,1\}^\omega](/latex?n=f72480a22ca47a8efff79952bb6f467384bae226b1468496997785d0d6f5f326)
. Then there is some initial subsequence
![b=(b_i)_{i<n}](/latex?n=393c60e9906b5bf35bb973bf97cdf335fb07363ba1cce8a078ca9ddd12ac6d23)
of
![a](/latex?n=ca978112ca1bbdcafac231b39a23dc4da786eff8147c4e72b9807785afee48bb)
, such that for all sequences
![c](/latex?n=2e7d2c03a9507ae265ecf5b5356885a53393a2029d241394997265a1a25aefc6)
,
![f(b*c)=f(a)](/latex?n=595c85e2a932b7e8832d549cd699083621626f0b6f147723173b57ee43e2b98f)
.
Proof: A terminating turing machine can, for every given sequence
![a](/latex?n=ca978112ca1bbdcafac231b39a23dc4da786eff8147c4e72b9807785afee48bb)
, only read finitely many elements of
![a](/latex?n=ca978112ca1bbdcafac231b39a23dc4da786eff8147c4e72b9807785afee48bb)
, thus, there is an upper bound
![m\in\omega](/latex?n=96d915c997a23ae953041d11de22dc05c86d27bae61e2c7086752a29b2823656)
such that the program is only dependent of elements
![a_{j<m}](/latex?n=9bf2e134bac6d3fb129456b84c381e65130f68ba59fbf91afa912e955fdb84cc)
. Set
![n=m](/latex?n=867ceee82006baa3b0d51ff153328cf72479fd721609fd23e3a5ac6eed2bd87d)
and
![(b_i)_{i<n} = (a_i)_{i<m}](/latex?n=d8f6412116268695821e4f410d393713c5c2d6a83b76da6dc0ad8f8eb9ed9e78)
. Then
![f(b*c)=f(a)](/latex?n=595c85e2a932b7e8832d549cd699083621626f0b6f147723173b57ee43e2b98f)
for all sequences
![c](/latex?n=2e7d2c03a9507ae265ecf5b5356885a53393a2029d241394997265a1a25aefc6)
, since the program does not depend on an elements not in
![b](/latex?n=3e23e8160039594a33894f6564e1b1348bbd7a0088d42c4acb73eeaed59c009d)
.
□
We say that a computable
depends only on a
sequence
![a=(a_i)_{i<n}](/latex?n=00de35415ca918390ef9580b3f273ab57fbb222685050c0ef3ac612df6a29e10)
when for every
![c_1,c_2](/latex?n=fa2d4ad39a17681008c010772c523596bdae607c9a8fb65d3a169444fc923760)
we have
![f(a*c_1)=f(a*c_2)](/latex?n=9c474e1e6a9a010b6d767417210e3061766dc148f2fff485a7546995083ae3c5)
, and it
depends exactly on
![a=(a_i)_{i<n}](/latex?n=00de35415ca918390ef9580b3f273ab57fbb222685050c0ef3ac612df6a29e10)
when it depends only on
![(a_i)_{i<n}](/latex?n=82ee5ab001fadf8b90cf2b02dea9ee5bb9c3d84852f5cb45561ec2ace4d4bcba)
but this is not the case for subsequences
![(a_i)_{i<m},m<n](/latex?n=cf34e929d863e637d1d98428b77b19b4b2edeee87ec57e7820b2aa7c24eb36bb)
.
By Lemma 1 it is trivial to proof that two functions
![f,g](/latex?n=88fbd7979ebef5522bdd608cd5a051b9c2a3fa6a9eb541cac67044f75a5027cc)
are not equal: Just find a sequence
![a](/latex?n=ca978112ca1bbdcafac231b39a23dc4da786eff8147c4e72b9807785afee48bb)
on that both of them depend only, and for which
![f(a)\neq g(a)](/latex?n=e2f24c2b257edf0c78518b2ea56ac539f075516789da67c4ca70f2be7fb147aa)
. The more interesting part is the case when they are equal.
Using Lemma 1, we can encode such functions
![f](/latex?n=252f10c83610ebca1a059c0bae8255eba2f95be4d1d7bcfa89d7248a82d9f111)
in the following way: Let
![(A_i)_{i\in\omega}](/latex?n=1ac2243fad4abe444589d59c8e0680a1ea343b560b645a207506389c6f958973)
be predicate constants, and denote by
![PA](/latex?n=86a7f47b333770c6e85f03ee3caa6ef9dfebfe2cb3444b738cc2df5d177ce38a)
the first-order
Peano arithmetic. If
![f(a)=k](/latex?n=28abf16a425c16fb56ea6c93562cd1e60ff9a8f39d533c467025b64538abf2b5)
where
![f](/latex?n=252f10c83610ebca1a059c0bae8255eba2f95be4d1d7bcfa89d7248a82d9f111)
depends only on
![(a_i)_{i<m}](/latex?n=bb8dc2fe45da3feea38821baabd5c04c81dbab1b8b9f8847d4b5eb6ec9fe9fdd)
, 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](/latex?n=babb83b6378c9f90bd7a04829ca9bed7eba18132afbdf7f3ad700cea527f085d)
, where
![c](/latex?n=2e7d2c03a9507ae265ecf5b5356885a53393a2029d241394997265a1a25aefc6)
is a term constant, and
![k](/latex?n=8254c329a92850f6d539dd376f4816ee2764517da5e0235514af433164480d7a)
can be expressed in the form
![S(\ldots S(0))](/latex?n=cd6b77002af9559c41221d6090805d80bc09a9a5c0d8a9bb275c3cf0ef454028)
as usual. Now define
![Mod_{f,c} := PA \cup \{ M_{f,a,c} | a \in \{0,1\}^\omega\}](/latex?n=a9a534cdb15d3e475edf5f1662c48a15c2c5a375759eb7980e339ac93f3e4c76)
. Obviously,
![f(a)=k \Leftrightarrow (Mod_{f,c}[A_i:\Leftrightarrow(a_i=1)]\models c=k)](/latex?n=842a3df29c5606b5a566f616b3c4ed43e0933afd9d18719973629937a01adc9e)
. Now, if two functions
![f,g](/latex?n=88fbd7979ebef5522bdd608cd5a051b9c2a3fa6a9eb541cac67044f75a5027cc)
are equal, we know that
![PA\cup Mod_{f,c}\cup Mod_{g,d}\cup \{c\neq d\}](/latex?n=4a52f8e6fb207062f0c8ac629dbca8aa29eb174b2f21104c68a69067c8079e1f)
is not satisfiable, and therefore,
![PA\cup Mod_{f,c}\cup Mod_{g,d}\cup \{c\neq d\}\models\bot](/latex?n=4bcc31177a9556d1bfef183843b46ad1922316ce40b2725420a270069675d52a)
. By the
completeness theorem, we therefore know that
![PA\cup Mod_{f,c}\cup Mod_{g,d}\cup \{c\neq d\}\vdash\bot](/latex?n=485b231a43c8553e972966c86d13a720cd1f2577764a9273c0ed1ea031f69eb7)
, and hence, the equality
![f=g](/latex?n=263b26c3863f213442adaa4d8bffceaf652b9b0d4bd952a361905b3ffe334823)
is provable.
Nice.