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 : ℕ), 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 : σ), 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 : σ), x ∈ f a → ∀ (y : σ), 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.

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

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

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, 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.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.eval c ∈ C) {f : ℕ →. ℕ} {g : ℕ →. ℕ} (hf : Nat.Partrec f) (hg : Nat.Partrec g) (fC : f ∈ C) : g ∈ C

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

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

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

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.eval c n).Dom

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

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

A simplified basis for Partrec.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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