Computability theory and the halting problem

A universal partial recursive function, Rice's theorem, and the halting problem.

References

• [Mario Carneiro, Formalizing computability theory via partial recursive functions][carneiro2019]

theorem Nat.Partrec.merge' {f : ℕ →. ℕ} {g : ℕ →. ℕ} (hf : Nat.Partrec f) (hg : Nat.Partrec g) : ∃ (h : ℕ →. ℕ), Nat.Partrec h ∧ ∀ (a : ℕ), (∀ x ∈ h a, x ∈ f a ∨ x ∈ g a) ∧ ((h a).Dom ↔ (f a).Dom ∨ (g a).Dom)

theorem Partrec.merge' {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {f : α →. σ} {g : α →. σ} (hf : Partrec f) (hg : Partrec g) : ∃ (k : α →. σ), Partrec k ∧ ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)

theorem Partrec.merge {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {f : α →. σ} {g : α →. σ} (hf : Partrec f) (hg : Partrec g) (H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y) : ∃ (k : α →. σ), Partrec k ∧ ∀ (a : α) (x : σ), x ∈ k a ↔ x ∈ f a ∨ x ∈ g a

theorem Partrec.cond {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {c : α → Bool} {f : α →. σ} {g : α →. σ} (hc : Computable c) (hf : Partrec f) (hg : Partrec g) : Partrec fun (a : α) => bif c a then f a else g a

theorem Partrec.sum_casesOn {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_4} [Primcodable α] [Primcodable β] [Primcodable γ] [Primcodable σ] {f : α → β ⊕ γ} {g : α → β →. σ} {h : α → γ →. σ} (hf : Computable f) (hg : Partrec₂ g) (hh : Partrec₂ h) : Partrec fun (a : α) => Sum.casesOn (f a) (g a) (h a)

def ComputablePred {α : Type u_1} [Primcodable α] (p : α → Prop) : Prop

A computable predicate is one whose indicator function is computable.

Equations

• ComputablePred p = ∃ (x : DecidablePred p), Computable fun (a : α) => decide (p a)

def RePred {α : Type u_1} [Primcodable α] (p : α → Prop) : Prop

A recursively enumerable predicate is one which is the domain of a computable partial function.

Equations

• RePred p = Partrec fun (a : α) => Part.assert (p a) fun (x : p a) => Part.some ()

theorem RePred.of_eq {α : Type u_1} [Primcodable α] {p : α → Prop} {q : α → Prop} (hp : RePred p) (H : ∀ (a : α), p a ↔ q a) : RePred q

theorem Partrec.dom_re {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {f : α →. β} (h : Partrec f) : RePred fun (a : α) => (f a).Dom

theorem ComputablePred.of_eq {α : Type u_1} [Primcodable α] {p : α → Prop} {q : α → Prop} (hp : ComputablePred p) (H : ∀ (a : α), p a ↔ q a) : ComputablePred q

theorem ComputablePred.computable_iff {α : Type u_1} [Primcodable α] {p : α → Prop} : ComputablePred p ↔ ∃ (f : α → Bool), Computable f ∧ p = fun (a : α) => f a = true

theorem ComputablePred.not {α : Type u_1} [Primcodable α] {p : α → Prop} (hp : ComputablePred p) : ComputablePred fun (a : α) => ¬p a

theorem ComputablePred.ite {f₁ : ℕ → ℕ} {f₂ : ℕ → ℕ} (hf₁ : Computable f₁) (hf₂ : Computable f₂) {c : ℕ → Prop} [DecidablePred c] (hc : ComputablePred c) : Computable fun (k : ℕ) => if c k then f₁ k else f₂ k

The computable functions are closed under if-then-else definitions with computable predicates.

theorem ComputablePred.to_re {α : Type u_1} [Primcodable α] {p : α → Prop} (hp : ComputablePred p) : RePred p

theorem ComputablePred.rice (C : Set (ℕ →. ℕ)) (h : ComputablePred fun (c : Nat.Partrec.Code) => c.eval ∈ C) {f : ℕ →. ℕ} {g : ℕ →. ℕ} (hf : Nat.Partrec f) (hg : Nat.Partrec g) (fC : f ∈ C) : g ∈ C

Rice's Theorem

theorem ComputablePred.rice₂ (C : Set Nat.Partrec.Code) (H : ∀ (cf cg : Nat.Partrec.Code), cf.eval = cg.eval → (cf ∈ C ↔ cg ∈ C)) : (ComputablePred fun (c : Nat.Partrec.Code) => c ∈ C) ↔ C = ∅ ∨ C = Set.univ

theorem ComputablePred.halting_problem_re (n : ℕ) : RePred fun (c : Nat.Partrec.Code) => (c.eval n).Dom

The Halting problem is recursively enumerable

theorem ComputablePred.halting_problem (n : ℕ) : ¬ComputablePred fun (c : Nat.Partrec.Code) => (c.eval n).Dom

The Halting problem is not computable

theorem ComputablePred.computable_iff_re_compl_re {α : Type u_1} [Primcodable α] {p : α → Prop} [DecidablePred p] : ComputablePred p ↔ RePred p ∧ RePred fun (a : α) => ¬p a

theorem ComputablePred.computable_iff_re_compl_re' {α : Type u_1} [Primcodable α] {p : α → Prop} : ComputablePred p ↔ RePred p ∧ RePred fun (a : α) => ¬p a

theorem ComputablePred.halting_problem_not_re (n : ℕ) : ¬RePred fun (c : Nat.Partrec.Code) => ¬(c.eval n).Dom

inductive Nat.Partrec' {n : ℕ} : (Mathlib.Vector ℕ n →. ℕ) → Prop

A simplified basis for Partrec.

• prim: ∀ {n : ℕ} {f : Mathlib.Vector ℕ n → ℕ}, Nat.Primrec' f → Nat.Partrec' ↑f
• comp: ∀ {m n : ℕ} {f : Mathlib.Vector ℕ n →. ℕ} (g : Fin n → Mathlib.Vector ℕ m →. ℕ), Nat.Partrec' f → (∀ (i : Fin n), Nat.Partrec' (g i)) → Nat.Partrec' fun (v : Mathlib.Vector ℕ m) => (Mathlib.Vector.mOfFn fun (i : Fin n) => g i v) >>= f
• rfind: ∀ {n : ℕ} {f : Mathlib.Vector ℕ (n + 1) → ℕ}, Nat.Partrec' ↑f → Nat.Partrec' fun (v : Mathlib.Vector ℕ n) => Nat.rfind fun (n_1 : ℕ) => Part.some (decide (f (n_1 ::ᵥ v) = 0))

theorem Nat.Partrec'.to_part {n : ℕ} {f : Mathlib.Vector ℕ n →. ℕ} (pf : Nat.Partrec' f) : Partrec f

theorem Nat.Partrec'.of_eq {n : ℕ} {f : Mathlib.Vector ℕ n →. ℕ} {g : Mathlib.Vector ℕ n →. ℕ} (hf : Nat.Partrec' f) (H : ∀ (i : Mathlib.Vector ℕ n), f i = g i) : Nat.Partrec' g

theorem Nat.Partrec'.of_prim {n : ℕ} {f : Mathlib.Vector ℕ n → ℕ} (hf : Primrec f) : Nat.Partrec' ↑f

theorem Nat.Partrec'.head {n : ℕ} : Nat.Partrec' ↑Mathlib.Vector.head

theorem Nat.Partrec'.tail {n : ℕ} {f : Mathlib.Vector ℕ n →. ℕ} (hf : Nat.Partrec' f) : Nat.Partrec' fun (v : Mathlib.Vector ℕ n.succ) => f v.tail

theorem Nat.Partrec'.bind {n : ℕ} {f : Mathlib.Vector ℕ n →. ℕ} {g : Mathlib.Vector ℕ (n + 1) →. ℕ} (hf : Nat.Partrec' f) (hg : Nat.Partrec' g) : Nat.Partrec' fun (v : Mathlib.Vector ℕ n) => (f v).bind fun (a : ℕ) => g (a ::ᵥ v)

theorem Nat.Partrec'.map {n : ℕ} {f : Mathlib.Vector ℕ n →. ℕ} {g : Mathlib.Vector ℕ (n + 1) → ℕ} (hf : Nat.Partrec' f) (hg : Nat.Partrec' ↑g) : Nat.Partrec' fun (v : Mathlib.Vector ℕ n) => Part.map (fun (a : ℕ) => g (a ::ᵥ v)) (f v)

def Nat.Partrec'.Vec {n : ℕ} {m : ℕ} (f : Mathlib.Vector ℕ n → Mathlib.Vector ℕ m) : Prop

Analogous to Nat.Partrec' for ℕ-valued functions, a predicate for partial recursive vector-valued functions.

Equations

• Nat.Partrec'.Vec f = ∀ (i : Fin m), Nat.Partrec' fun (v : Mathlib.Vector ℕ n) => ↑(some ((f v).get i))

theorem Nat.Partrec'.Vec.prim {n : ℕ} {m : ℕ} {f : Mathlib.Vector ℕ n → Mathlib.Vector ℕ m} (hf : Nat.Primrec'.Vec f) : Nat.Partrec'.Vec f

theorem Nat.Partrec'.nil {n : ℕ} : Nat.Partrec'.Vec fun (x : Mathlib.Vector ℕ n) => Mathlib.Vector.nil

theorem Nat.Partrec'.cons {n : ℕ} {m : ℕ} {f : Mathlib.Vector ℕ n → ℕ} {g : Mathlib.Vector ℕ n → Mathlib.Vector ℕ m} (hf : Nat.Partrec' ↑f) (hg : Nat.Partrec'.Vec g) : Nat.Partrec'.Vec fun (v : Mathlib.Vector ℕ n) => f v ::ᵥ g v

theorem Nat.Partrec'.idv {n : ℕ} : Nat.Partrec'.Vec id

theorem Nat.Partrec'.comp' {n : ℕ} {m : ℕ} {f : Mathlib.Vector ℕ m →. ℕ} {g : Mathlib.Vector ℕ n → Mathlib.Vector ℕ m} (hf : Nat.Partrec' f) (hg : Nat.Partrec'.Vec g) : Nat.Partrec' fun (v : Mathlib.Vector ℕ n) => f (g v)

theorem Nat.Partrec'.comp₁ {n : ℕ} (f : ℕ →. ℕ) {g : Mathlib.Vector ℕ n → ℕ} (hf : Nat.Partrec' fun (v : Mathlib.Vector ℕ 1) => f v.head) (hg : Nat.Partrec' ↑g) : Nat.Partrec' fun (v : Mathlib.Vector ℕ n) => f (g v)

theorem Nat.Partrec'.rfindOpt {n : ℕ} {f : Mathlib.Vector ℕ (n + 1) → ℕ} (hf : Nat.Partrec' ↑f) : Nat.Partrec' fun (v : Mathlib.Vector ℕ n) => Nat.rfindOpt fun (a : ℕ) => Denumerable.ofNat (Option ℕ) (f (a ::ᵥ v))

theorem Nat.Partrec'.of_part {n : ℕ} {f : Mathlib.Vector ℕ n →. ℕ} : Partrec f → Nat.Partrec' f

theorem Nat.Partrec'.part_iff {n : ℕ} {f : Mathlib.Vector ℕ n →. ℕ} : Nat.Partrec' f ↔ Partrec f

theorem Nat.Partrec'.part_iff₁ {f : ℕ →. ℕ} : (Nat.Partrec' fun (v : Mathlib.Vector ℕ 1) => f v.head) ↔ Partrec f

theorem Nat.Partrec'.part_iff₂ {f : ℕ → ℕ →. ℕ} : (Nat.Partrec' fun (v : Mathlib.Vector ℕ 2) => f v.head v.tail.head) ↔ Partrec₂ f

theorem Nat.Partrec'.vec_iff {m : ℕ} {n : ℕ} {f : Mathlib.Vector ℕ m → Mathlib.Vector ℕ n} : Nat.Partrec'.Vec f ↔ Computable f