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
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)
A computable predicate is one whose indicator function is computable.
Instances For
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)
:
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))
:
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]
:
theorem
ComputablePred.halting_problem_not_re
(n : ℕ)
:
¬RePred fun c => ¬(Nat.Partrec.Code.eval c n).Dom
- 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
.
Instances For
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)
Analogous to Nat.Partrec'
for ℕ
-valued functions, a predicate for partial recursive
vector-valued functions.
Instances For
theorem
Nat.Partrec'.Vec.prim
{n : ℕ}
{m : ℕ}
{f : Vector ℕ n → Vector ℕ m}
(hf : Nat.Primrec'.Vec f)
:
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'.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'.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