# Undecidable

How can we prove results about undecidability in a setting where
everything terminates?


```
{-# OPTIONS   #-}
open import Level using (0ℓ)
open import Data.Nat
open import Data.Empty
open import Data.Nat.Properties using (≤⇒≤′; ≤′⇒≤)
open import Data.Product
open import Data.Maybe
open import Relation.Binary.PropositionalEquality
open import Relation.Unary
open import Relation.Nullary using (¬_; Dec; yes; no; contradiction; map′)
open import Function.Base
import Data.Nat.Properties as ℕ


open import Partial


module _ where
private
  variable
    A B C : Set

```

## Models of Computation
```
record model-of-computation (A : Set) : Set where
  field
    run : (code : ℕ) → (input : A) → Step-Indexed A

  T : (code : ℕ) → (input : A) → ℕ → Maybe A
  T c x k = Step-Indexed.f (run c x) k 
```
We will only use `A = ℕ` later, but keep the `A` to distinguish between
numbers "here" in the metalanguage and the encoded values.

We define enumerators of predicates `P : ℕ → Set` as functions
that yield `just x` for some input iff `x ∈ P`.
For its definition, we define the image of partial functions:
```
Im[_] : ∀ (f : A ⇀ B) → B → Set
Im[_] f b = ∃[ a ] f a ≡ just b

Enumerable : (ℕ → Set) → Set
Enumerable P = Σ[ f ∈ (ℕ → Maybe ℕ) ] P ≐ Im[ f ]

_≈im_ : (f g : A → Maybe B) → Set
f ≈im g = Im[ f ] ≐ Im[ g ]
```
The last relation describes that two functions enumerate the same predicate,
regardless of the order.

## Pairing: ℕ ≅ ℕ × ℕ
For encoding 
A record for bijections between sets
```
infix 1 _≅_
record _≅_ (A B : Set) : Set where
  field
    to : A → B
    from : B → A
    to∘from : (to ∘ from) ≗ id {_} {B}
    from∘to : (from ∘ to) ≗ id {_} {A}
```

The isomorphism `ℕ ≅ ℕ × ℕ` constructs following sequence of pairs:
```text
 0,3
     ↖
 0,2   1,2
     ↖     ↖
 0,1   1,1   2,1
     ↖     ↖     ↖
 0,0   1,0   2,0   3,0
```
The diagonal with index k contains the elements

  { (x , y) ∈ ℕ × ℕ ∣ x + k ≡ k }

Given a pair, the following function constructs the next
pair in above sequence:
```
next-pair : ℕ × ℕ → ℕ × ℕ
next-pair (zero , y) = suc y , 0
next-pair (suc x , y) = x , (suc y)

unpair : ℕ → ℕ × ℕ
unpair zero = zero , zero
unpair (suc k) = next-pair (unpair k)

-- how many elements before diagonal number k
elements-before : ℕ → ℕ
elements-before zero = 0
elements-before (suc k) = elements-before k + suc k

pair : ℕ → ℕ → ℕ
pair x y = elements-before (x + y) + y

postulate
  unpair∘pair : ∀ x y → unpair (pair x y) ≡ (x , y)
  pair∘unpair : ∀ k → (uncurry pair) (unpair k) ≡ k

ℕ≅ℕ×ℕ : ℕ ≅ ℕ × ℕ 
ℕ≅ℕ×ℕ = record
  { to = unpair
  ; from = uncurry pair
  ; to∘from = uncurry unpair∘pair
  ; from∘to = pair∘unpair
  }
```
## Maybe ℕ ≅ ℕ
```
Maybeℕ≅ℕ : Maybe ℕ ≅ ℕ 
Maybeℕ≅ℕ = record
  { to = λ { (just x) → suc x ; nothing → 0 }
  ; from = λ { zero → nothing ; (suc x) → just x }
  ; to∘from = λ { zero → refl ; (suc x) → refl }
  ; from∘to = λ { (just x) → refl ; nothing → refl}
  }
```

## Truncation
With a prefix `.`, we can describe "proof irrelevance". Intuitively, these are
statements whose value are irrelevant for the actual computation.
```
record ∥_∥ (A : Set) : Set where
  constructor ∣_∣
  field
    .proof : A

trunc : {A : Set} → A → ∥ A ∥
trunc a = ∣ a ∣

∥⊥∥→⊥ : ∥ ⊥ ∥ → ⊥
∥⊥∥→⊥ ()

∥map : (A → B) → ∥ A ∥ → ∥ B ∥
∥map f ∣ x ∣ = ∣ f x ∣

¬trunc : {A : Set} → ¬ A → ¬ ∥ A ∥
¬trunc ¬A = ∥⊥∥→⊥ ∘ ∥map ¬A

module example where
  test-g : (n : ℕ) → .(n ≥ 1) → (2 + ((1 + n) ∸ 2) ≡ (1 + n))
  test-g (suc n) _ = refl

  test-f : (n : ℕ) → ∥ n ≥ 2 ∥ → (2 + (n ∸ 2) ≡ n)
  test-f (suc zero) 1≥2 = ⊥-elim (¬trunc (λ { (s≤s ())}) 1≥2) 
  test-f (2+ n) g = refl
```
[End of lecture on 13 July 2026]

## Undecidability of the Halting Problem
Church's Thesis `CT` describes that every endofunction `f : A → A` can be computed by
some programme code `c`:
```
_↓_ : Step-Indexed B → ℕ → Maybe B
_↓_ = Step-Indexed.f

-- a machine M computes a function
_~~>_ : (A → Step-Indexed B) → (A → B) → Set
M ~~> f = ∀ x → ∃[ k ] M x ↓ k ≡ just (f x)


module Undecidable-Halting (Model : model-of-computation ℕ) where
  open model-of-computation Model
  module assume-CT (CT : (f : ℕ → ℕ) → ∥ (Σ[ c ∈ ℕ ] run c ~~> f) ∥) where
```
The halting problem decides for a code `c`, whether the machine number `c`
halts when started with input `c`.
```
    -- the property that machine number c halts on some input x
    _halts-on_ : ℕ → ℕ → Set
    c halts-on x = ∃[ v ] ∃[ k ] run c x ↓ k ≡ just v
    Halting : ℕ → Set
    Halting c = c halts-on c
```
The halting problem decides for a code `c`, whether the machine number `c`
halts when started with input `c`.
```
    Halting-undecidable : ¬ Decidable Halting
    Halting-undecidable Halting? = contradiction (CT f) (¬trunc f-has-no-code)
      where
```
In order to prove its undecidability, we define a function `f` that cannot
have any code:

```text
  f : ℕ → ℕ
        ⎧ suc(v)  if the machine c, started with input c, halts
  f c = ⎨         with output v
        ⎩ 0       otherwise
```

```
      f : ℕ → ℕ
      f c = case (Halting? c) of λ
        { (yes (v , k , _)) → suc v
        ; (no _) → 0
        }
```
If the function `f` was computed by some machine `F`, then `f F` returns
`suc(v)` where `v` is the computation result of `F` started with `F`, so `v = f
F`, a contradicton.
```
      f-prop : ∀ (G : ℕ) (g : ℕ → ℕ) → (run G) ~~> g
               → f G ≡ suc (g G)
      f-prop G g G~~>g with (Halting? G)
      ... | yes (v , k , G[G]↓k≡just[v]) =
            -- if G halts with result v
            -- then this result v must be `g G`
            cong suc (Step-Indexed-functional (refl {_} {_} {run G G})
                 G[G]↓k≡just[v] (proj₂ (G~~>g G)))
      ... | no G[G]↑ =
            -- it is impossible that G does not halt,
            -- because G computes g, so it must halt
            -- on every input, in particular on input `G`
            contradiction ((g G) , (G~~>g G)) G[G]↑

      f-has-no-code : ¬ (Σ[ F ∈ ℕ ] run F ~~> f)
      f-has-no-code (F , F~~>f) = ℕ.1+n≢n (sym (f-prop F f F~~>f))
```
The general halting problem is then also undecidable:
```
    open import Relation.Binary renaming (Decidable to Decidable₂)
    GeneralHalting-undecidable : ¬ Decidable₂ _halts-on_
    GeneralHalting-undecidable _halts-on?_ = Halting-undecidable (λ c → c halts-on? c)
```

## Untruncated Church's Thesis CTΣ
```
module Untruncated-vs-Extensionality (Model : model-of-computation ℕ) where
  open model-of-computation Model
  open import Axiom.Extensionality.Propositional using (Extensionality)
  module assume-CTΣ (CTΣ : (f : ℕ → ℕ) → (Σ[ c ∈ ℕ ] run c ~~> f)) where

    ⟪_⟫ : (ℕ → ℕ) → ℕ
    ⟪ f ⟫ = proj₁ (CTΣ f)

    ⟪_⟫[_]-correct : (f : ℕ → ℕ) → (x : ℕ) → (run ⟪ f ⟫ x ↓ _ ≡ just (f x))
    ⟪ f ⟫[ x ]-correct = proj₂ (proj₂ (CTΣ f) x)

    module assume-extensionality (functional-extensionality : Extensionality 0ℓ 0ℓ) where
      opaque
        _≗?_ : (f g : ℕ → ℕ) → Dec (f ≗ g)
        f ≗? g =
          -- we reduce their point-wise equality to equality of their codes
          map′
          -- if their codes are the same, they return the same
          -- step-indexed values, and so return the same
          -- (since both halt)
          (λ ⟪f⟫≡⟪g⟫ x →
             Step-Indexed-functional
               ((cong (λ - → run - x)) ⟪f⟫≡⟪g⟫)
               ⟪ f ⟫[ x ]-correct
               ⟪ g ⟫[ x ]-correct)
          -- if the functions are point-wise equal, then
          -- they are identical (by extensionality) and
          -- thus must have the same code.
          (λ f≗g → cong ⟪_⟫ (functional-extensionality f≗g))
          (⟪ f ⟫ ≟ ⟪ g ⟫)

      try-run : ℕ → ℕ → ℕ
      try-run c k = fromMaybe 0 (run c c ↓ k)

      to01 : {P : Set} → Dec P → ℕ
      to01 (yes _) = 1
      to01 (no _)  = 0

      zeros? : ℕ → ℕ
      zeros? c = to01 (try-run c ≗? const 0)

      Z : ℕ
      Z = ⟪ zeros? ⟫

      open ≡-Reasoning
      inconsistent : ⊥
      inconsistent with (try-run Z ≗? const 0) in dec-result
      ... | yes try-run[Z]≗const[0] =
          ℕ.0≢1+n (begin
          0                             ≡⟨ try-run[Z]≗const[0] _ ⟨
          try-run Z _                   ≡⟨⟩
          fromMaybe 0 (run Z Z ↓ _)     ≡⟨ cong (fromMaybe 0) ⟪ zeros? ⟫[ Z ]-correct ⟩
          fromMaybe 0 (just (zeros? Z)) ≡⟨⟩
          zeros? Z                      ≡⟨ cong to01 dec-result ⟩
          1
          ∎)
      ... | no try-run[Z]≢const[0] = try-run[Z]≢const[0] try-run[Z]≗const[0]
        where
          try-run[Z]≗const[0] : try-run Z ≗ const 0
          try-run[Z]≗const[0] k with (run Z Z ↓ k) in Z[Z]↓k≡just[v]
          ... | nothing = refl
          ... | just v =
                -- we need to show v ≡ 0
                (v ≡ 0) ∋ (Step-Indexed-functional
                -- run Z Z returns v in the present case:
                (refl {_} {_} {run Z Z})
                -- run Z Z returns 0 by CTΣ:
                ((run Z Z ↓ _ ≡ just v) ∋ Z[Z]↓k≡just[v])
                (begin
                  (run Z Z ↓ _)     ≡⟨ ⟪ zeros? ⟫[ Z ]-correct ⟩
                  just (zeros? Z)   ≡⟨ cong just (cong to01 dec-result) ⟩
                  just 0
                  ∎))

      real-inconsistency : ∀ {ℓ} (A : Set ℓ) → A
      real-inconsistency = ⊥-elim inconsistent
```
[End of lecture on 16 July 2026]

## Literature

* Yannick Forster: [Church’s Thesis and Related Axioms in Coq’s Type Theory.](https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.21)
  ([in Rocq](https://github.com/uds-psl/churchs-thesis-coq/tree/7b736b5d8b81be03a37f3ec9de3f538fe17c3f28)).
  The inconsistency of `CTΣ` with functional extensionality is *Lemma 29*
* Andrej Bauer: *First Steps in Synthetic Computability Theory*