# Computability theory and the halting problem #

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

## References #

theorem Nat.Partrec.merge' {f : } {g : } (hf : ) (hg : ) :
∃ (h : ), ∀ (a : ), (xh 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} [] [] {f : α →. σ} {g : α →. σ} (hf : ) (hg : ) :
∃ (k : α →. σ), ∀ (a : α), (xk 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} [] [] {f : α →. σ} {g : α →. σ} (hf : ) (hg : ) (H : ∀ (a : α), xf a, yg a, x = y) :
∃ (k : α →. σ), ∀ (a : α) (x : σ), x k a x f a x g a
theorem Partrec.cond {α : Type u_1} {σ : Type u_4} [] [] {c : αBool} {f : α →. σ} {g : α →. σ} (hc : ) (hf : ) (hg : ) :
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} [] [] [] [] {f : αβ γ} {g : αβ →. σ} {h : αγ →. σ} (hf : ) (hg : ) (hh : ) :
Partrec fun (a : α) => Sum.casesOn (f a) (g a) (h a)
def ComputablePred {α : Type u_1} [] (p : αProp) :

A computable predicate is one whose indicator function is computable.

Equations
Instances For
def RePred {α : Type u_1} [] (p : αProp) :

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

Equations
Instances For
theorem RePred.of_eq {α : Type u_1} [] {p : αProp} {q : αProp} (hp : ) (H : ∀ (a : α), p a q a) :
theorem Partrec.dom_re {α : Type u_1} {β : Type u_2} [] [] {f : α →. β} (h : ) :
RePred fun (a : α) => (f a).Dom
theorem ComputablePred.of_eq {α : Type u_1} [] {p : αProp} {q : αProp} (hp : ) (H : ∀ (a : α), p a q a) :
theorem ComputablePred.computable_iff {α : Type u_1} [] {p : αProp} :
∃ (f : αBool), p = fun (a : α) => f a = true
theorem ComputablePred.not {α : Type u_1} [] {p : αProp} (hp : ) :
ComputablePred fun (a : α) => ¬p a
theorem ComputablePred.to_re {α : Type u_1} [] {p : αProp} (hp : ) :
theorem ComputablePred.rice (C : Set ()) (h : ComputablePred fun (c : Nat.Partrec.Code) => c.eval C) {f : } {g : } (hf : ) (hg : ) (fC : f C) :
g C

Rice's Theorem

theorem ComputablePred.rice₂ (C : ) (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} [] {p : αProp} [] :
RePred fun (a : α) => ¬p a
theorem ComputablePred.computable_iff_re_compl_re' {α : Type u_1} [] {p : αProp} :
RePred fun (a : α) => ¬p a
inductive Nat.Partrec' {n : } :
()Prop

A simplified basis for Partrec.

Instances For
theorem Nat.Partrec'.to_part {n : } {f : } (pf : ) :
theorem Nat.Partrec'.of_eq {n : } {f : } {g : } (hf : ) (H : ∀ (i : ), f i = g i) :
theorem Nat.Partrec'.of_prim {n : } {f : } (hf : ) :
theorem Nat.Partrec'.head {n : } :
theorem Nat.Partrec'.tail {n : } {f : } (hf : ) :
Nat.Partrec' fun (v : Mathlib.Vector n.succ) => f v.tail
theorem Nat.Partrec'.bind {n : } {f : } {g : Mathlib.Vector (n + 1) →. } (hf : ) (hg : ) :
Nat.Partrec' fun (v : ) => (f v).bind fun (a : ) => g (a ::ᵥ v)
theorem Nat.Partrec'.map {n : } {f : } {g : Mathlib.Vector (n + 1)} (hf : ) (hg : ) :
Nat.Partrec' fun (v : ) => Part.map (fun (a : ) => g (a ::ᵥ v)) (f v)
def Nat.Partrec'.Vec {n : } {m : } (f : ) :

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

Equations
Instances For
theorem Nat.Partrec'.Vec.prim {n : } {m : } {f : } (hf : ) :
theorem Nat.Partrec'.nil {n : } :
Nat.Partrec'.Vec fun (x : ) => Mathlib.Vector.nil
theorem Nat.Partrec'.cons {n : } {m : } {f : } {g : } (hf : ) (hg : ) :
Nat.Partrec'.Vec fun (v : ) => f v ::ᵥ g v
theorem Nat.Partrec'.idv {n : } :
theorem Nat.Partrec'.comp' {n : } {m : } {f : } {g : } (hf : ) (hg : ) :
Nat.Partrec' fun (v : ) => f (g v)
theorem Nat.Partrec'.comp₁ {n : } (f : ) {g : } (hf : Nat.Partrec' fun (v : ) => f v.head) (hg : ) :
Nat.Partrec' fun (v : ) => f (g v)
theorem Nat.Partrec'.rfindOpt {n : } {f : Mathlib.Vector (n + 1)} (hf : ) :
Nat.Partrec' fun (v : ) => Nat.rfindOpt fun (a : ) => Denumerable.ofNat () (f (a ::ᵥ v))
theorem Nat.Partrec'.of_part {n : } {f : } :
theorem Nat.Partrec'.part_iff {n : } {f : } :
theorem Nat.Partrec'.part_iff₁ {f : } :
(Nat.Partrec' fun (v : ) => f v.head)
theorem Nat.Partrec'.part_iff₂ {f : } :