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 : Partrec f) (hg : Partrec g) : ∃ (h : ℕ →. ℕ), 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.sumCasesOn {α : 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)

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

theorem Computable.computablePred {α : Type u_1} [Primcodable α] {p : α → Prop} [DecidablePred p] (hp : Computable fun (a : α) => decide (p a)) : ComputablePred p

theorem computablePred_iff_computable_decide {α : Type u_1} [Primcodable α] {p : α → Prop} [DecidablePred p] : ComputablePred p ↔ Computable fun (a : α) => decide (p a)

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

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 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 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 : ℕ} : (List.Vector ℕ n →. ℕ) → Prop

A simplified basis for Partrec.

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

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

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

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

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

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

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

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

def Nat.Partrec'.Vec {n m : ℕ} (f : List.Vector ℕ n → List.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 : List.Vector ℕ n) => ↑(some ((f v).get i))

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

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

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

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

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

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

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

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

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

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

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

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