Computability theory and the halting problem #
A universal partial recursive function, Rice's theorem, and the halting problem.
References #
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)
@[deprecated Partrec.sumCasesOn (since := "2025-02-21")]
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)
Alias of Partrec.sumCasesOn.
A computable predicate is one whose indicator function is computable.
Equations
- ComputablePred p = ∃ (x : DecidablePred p), Computable fun (a : α) => decide (p a)
Instances For
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)
:
theorem
ComputablePred.of_eq
{α : Type u_1}
[Primcodable α]
{p q : α → Prop}
(hp : ComputablePred p)
(H : ∀ (a : α), p a ↔ q a)
:
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)
:
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))
:
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]
:
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))
Instances For
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'.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)
:
theorem
Nat.Partrec'.map
{n : ℕ}
{f : List.Vector ℕ n →. ℕ}
{g : List.Vector ℕ (n + 1) → ℕ}
(hf : Partrec' f)
(hg : Partrec' ↑g)
:
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))
Instances For
theorem
Nat.Partrec'.Vec.prim
{n m : ℕ}
{f : List.Vector ℕ n → List.Vector ℕ m}
(hf : Primrec'.Vec f)
:
Vec f
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'.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))