Decidability in the One-Point Compactification of ℕ

:TODO: More narrative here.

From a recent Agda mailing list post by Martin Escardo.

We can write the following unlikely functional program in Agda (and in Martin-Loef Type Theory of any variety):

(1) Consider the type of decreasing infinite sequences of digits 0 and 1.

Call this type ℕ∞, because

• The sequence of n-many ones followed by infinitely many zeros encodes the natural number n.
• The sequence of infinitely many ones encodes ∞,

So we have an embedding ℕ → ℕ∞ and a new point ∞ in ℕ∞.

(2) There is an Agda program that decides, for a given p : ℕ∞ → Bool, whether or not there is x : ℕ∞ with p x ≡ True.

Clearly such a program does not exist if we replace ℕ∞ by ℕ. This non-existence is a theorem of computability theory.

But it does exist with ℕ∞.

These I found useful at least at some stage of development though I did not end up using all of them. They may already be implemented in the standard library, just not where I looked; I'd have to double check.

nothing≢just : {A : Set} → (a : A) → ¬ (nothing ≡ just a)
nothing≢just a ()

Is-nothing? : {A : Set} → (x : Maybe A) → Dec (Is-nothing x)
Is-nothing? nothing = yes All.nothing
Is-nothing? (just _) = no λ { (All.just ()) }

Is-just? : {A : Set} → (x : Maybe A) → Dec (Is-just x)
Is-just? nothing = no λ ()
Is-just? (just _) = yes (Any.just tt)

First, let us use the name ℕ*, rather than ℕ∞. This leads us to naturally append * to the standard names for elements of or functions on ℕ*, which is far more readable than appending ∞ everywhere. We will still call the “new point” of ℕ* ∞.

Rather than decreasing infinite sequences of 0's and 1's, I choose to represent ℕ* as a potentially infinite string of unary constructors; specifically, the constructor just of the Maybe type.

record ℕ* : Set where
  coinductive
  field
    c : Maybe ℕ*
open ℕ*

We need to define bisimilarity of elements of ℕ* in order to be able to compare them.

record _≈_ (m n : ℕ*) : Set where
  coinductive
  field
    c-≈ : ℕ*.c m ≡ ℕ*.c n
open _≈_

Symmetry and transitivity follow easily.

≈-sym : {m n : ℕ*} → m ≈ n → n ≈ m
c-≈ (≈-sym m≈n) = sym (c-≈ m≈n)

≈-trans : {m n o : ℕ*} → m ≈ n → n ≈ o → m ≈ o
c-≈ (≈-trans m≈n n≈o) = trans (c-≈ m≈n) (c-≈ n≈o)

It's convenient to refer to the elements of ℕ* by these more familiar names.

0* : ℕ*
c 0* = nothing

suc* : ℕ* → ℕ*
c (suc* n) = just n

∞ : ℕ*
c ∞ = just ∞

Now we provide a series of proofs that these names refer to the numbers we have in mind; namely, we want to prove that

• zero is not a successor¹
• successors is an injecive function,
• infinity is a fix-point of successor, and
• infinity is the only fix-point of successor.

¬[0*≈suc*-n] : (n : ℕ*) → ¬ 0* ≈ suc* n
¬[0*≈suc*-n] n 0*≈suc*-n = nothing≢just n (c-≈ 0*≈suc*-n)

¬[0*≈∞] : ¬ (0* ≈ ∞)
¬[0*≈∞] 0*≈∞ = nothing≢just ∞ (c-≈ 0*≈∞)

suc*-∞≈∞ : suc* ∞ ≈ ∞
c-≈ (suc*-∞≈∞) = refl

suc*-injective : {m n : ℕ*}
      → suc* m ≈ suc* n → m ≈ n
c-≈ (suc*-injective m≈n) = cong c (just-injective (c-≈ m≈n))

¬[n≈∞]⇒¬[suc*-n≈∞] : (n : ℕ*) → ¬ (n ≈ ∞) → ¬ (suc* n ≈ ∞)
¬[n≈∞]⇒¬[suc*-n≈∞] n ¬[n≈∞] suc*-n≈∞ =
  ¬[n≈∞] (suc*-injective (≈-trans suc*-n≈∞
                                  (≈-sym suc*-∞≈∞)))

Now the embedding of a natural number n into ℕ produces a string of just's of length n, followed by a nothing. We could have used our constants here, but we define it directly instead.

embed : ℕ → ℕ*
embed zero = 0*
embed (suc n) = suc* (embed n)

There is no way that we can obtain the fix-point infinity by embedding.

¬[embed-n≈∞] : (n : ℕ) → ¬ (embed n ≈ ∞)
¬[embed-n≈∞] zero = ¬[0*≈∞]
¬[embed-n≈∞] (suc n) = ¬[n≈∞]⇒¬[suc*-n≈∞] (embed n) (¬[embed-n≈∞] n)

It may be useful for us to be able to distinguish values of ℕ*, because we cannot pattern match on elements. Decidable Is-zero* and Is-suc* predicates allow us to work around that limitation.

Is-zero* : ℕ* → Set
Is-zero* = _≈ 0*

Is-suc* : ℕ* → Set
Is-suc* n = Σ[ m ∈ ℕ* ] n ≈ suc* m

We can define an Is-∞ predicate, but unless I miss my mark, this cannot be decidable.

Is-∞ : ℕ* → Set
Is-∞ = _≈ ∞

I cannot see a way around using inspect to define the deciders for these. In the no cases, we must somewhat carefully constuct the contradictory value.

Is-zero*? : (n : ℕ*) → Dec (Is-zero* n)
Is-zero*? n with c n | inspect c n
... | nothing | [ c-n≡nothing ] = yes (record { c-≈ = c-n≡nothing })
... | just predn | [ c-n≡just-predn ]  =
  no λ n≈0* → ¬[0*≈suc*-n] predn (≈-sym (≈-trans (record { c-≈ = sym c-n≡just-predn }) n≈0*))

:TODO: commentary; I needed these for the approach to Is-suc*? which uses Is-zero*?, in order to translate the proofs.

pred* : (n : ℕ*) → ¬ (Is-zero* n) → ℕ*
pred* n ¬Is-zero*-n with c n | inspect c n
… | nothing | [ c-n≡nothing ] = ⊥-elim (¬Is-zero*-n (record { c-≈ = c-n≡nothing }))
… | just predn | [ _ ] = predn

suc*-pred* : (n : ℕ*) → (¬Is-zero*-n : ¬ (Is-zero* n))
           → suc* (pred* n ¬Is-zero*-n) ≈ n
suc*-pred* n ¬Is-zero*-n with c n | inspect c n
… | nothing | [ c-n≡nothing ] = ⊥-elim (¬Is-zero*-n (record { c-≈ = c-n≡nothing }))
… | just predn | [ c-n≡just-predn ] = ≈-sym (record { c-≈ = c-n≡just-predn })

¬[Is-zero*-n]⇒Is-suc*-n : (n : ℕ*) → ¬ (Is-zero* n) → Is-suc* n
¬[Is-zero*-n]⇒Is-suc*-n n ¬Is-zero*-n = pred* n ¬Is-zero*-n
                                       , ≈-sym (suc*-pred* n ¬Is-zero*-n)

It seems natural to decide if a ℕ* is a successor by first deciding if it is zero.

Is-suc*? : (m : ℕ*) → Dec (Is-suc* m)
Is-suc*? m = case Is-zero*? m of
  λ { (yes Is-zero*-m)
        → no λ { (n , m≈suc*-n) → ¬[0*≈suc*-n] n (≈-trans (≈-sym Is-zero*-m)
                                                          m≈suc*-n) }
    ; (no ¬Is-zero*-m) → yes (¬[Is-zero*-n]⇒Is-suc*-n m ¬Is-zero*-m)
    }

:TODO: 😀

I had begun a naive approach before I began using bisimilarity above, but it quickly got rejected by the termination checker.

Specifically, it begins by checking p 0*, then if that fails it moves on with a modified predicate I called Suc p. That works fine, until we examine the result of running decide on that predicate.

All the same, I will likely return to it next, unless I suddenly see the correct way forward. The current source code is commented out in the Org source of this document. It needs refactoring, so I don't want to show it yet.