Does this esoteric representation of integers have decidable equality?

Consider the following datatypes in Haskell:

data Foo = Halt | Iter Foo
newtype BigInt = BigInt {nthBit :: Foo -> Bool}

Foo is Peano numbers compactified by one limit point, namely fix Iter. BigInt represents arbitrary-length integers in two's complement. The limit point fix Iter forces the field nthBit to eventually terminate in infinite string of zeros, or infinite string of ones.

Since Foo is compact and Bool is discrete, BigInt expresses a discrete function space. But does this mean BigInt has decidable equality?

Semideciding inequality of BigInt is easy. Given two different integers, Keep evaluating their nthBit fields at Halt, Iter Halt, Iter (Iter Halt) and so on until they mismatch.

But what about semideciding equality? Given two equal integers, mathematically their equality at fix Iter should already serve as a proof that they might mismatch only at finitely many bits, but that doesn't give the range of the might-be mismatch.

Or was it my misconception that discreteness implies decidable equality?

Assuming that you intend to only count the total functions for $\mathsf{BigInt}$, then yes, equality should be decidable. Here's a sketch for how to do it for $i$ and $j$:

• First test $i$ and $j$ on $\infty$. If they differ, then they are unequal. If they both yield $1$, then run the subsequent tests with $-i$ and $-j$ obtained by flipping the output of $i$ and $j$.

• Due to continuity, we know that there are only finitely many $1$ indices remaining in $i$, so we can be sure that the following loop will complete:

• Search for $\bar{n} : \mathsf{Foo}$ such that $i\ \bar{n} = 1$. If you don't find one, the loop is complete. Otherwise check that $j\ \bar{n} = 1$. If not, then $i \neq j$. Otherwise ...

• Find $n : ℕ$ that corresponds to the above value. I believe this requires Markov's principle (unbounded search is okay as long as we know not all $n$ are $0$).

• Continue the loop with $i'$ and $j'$, which agree with $i$ and $j$, except that $i'\ \bar{n} = j'\ \bar{n} = 0$. This is accomplished by induction on $n$. In Haskell, you could just recurse on $\bar{n}$, but the reasoning that this is okay is analogous to Markov's principle ($\bar{n}$ is not $\infty$, so it is finite). Note of course that $i = j \leftrightarrow i' = j'$.

• When this process finishes, you are left with $i = \mathsf{const}\ 0$. But now you can easily test for equality with the remaining $j$ by searching for $\bar{n} : \mathsf{Foo}$ such that $j\ \bar{n} = 1$. If you find one, $i \neq j$. Otherwise $i = j$.

Here is an Agda formalization of this approach. It might look lengthy, but quite a bit of that is due to proving things about how it behaves. Just writing down the more simply typed procedure in Haskell would be considerably shorter. Markov's principle and continuity are implemented as assertions about the termination of certain recursive functions that Agda's checker would otherwise reject.

StackExchange Computer Science Q#160775, answer score: 2