Computability theory and the halting problem #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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) :
theorem
partrec.sum_cases
{α : 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 (λ (a : α), (f a).cases_on (g a) (h a))
A computable predicate is one whose indicator function is computable.
Equations
- computable_pred p = ∃ [D : decidable_pred p], computable (λ (a : α), decidable.to_bool (p a))
A recursively enumerable predicate is one which is the domain of a computable partial function.
Equations
- re_pred p = partrec (λ (a : α), part.assert (p a) (λ (_x : p a), part.some unit.star()))
theorem
re_pred.of_eq
{α : Type u_1}
[primcodable α]
{p q : α → Prop}
(hp : re_pred p)
(H : ∀ (a : α), p a ↔ q a) :
re_pred q
theorem
partrec.dom_re
{α : Type u_1}
{β : Type u_2}
[primcodable α]
[primcodable β]
{f : α →. β}
(h : partrec f) :
theorem
computable_pred.of_eq
{α : Type u_1}
[primcodable α]
{p q : α → Prop}
(hp : computable_pred p)
(H : ∀ (a : α), p a ↔ q a) :
theorem
computable_pred.computable_iff
{α : Type u_1}
[primcodable α]
{p : α → Prop} :
computable_pred p ↔ ∃ (f : α → bool), computable f ∧ p = λ (a : α), ↥(f a)
@[protected]
theorem
computable_pred.not
{α : Type u_1}
[primcodable α]
{p : α → Prop}
(hp : computable_pred p) :
computable_pred (λ (a : α), ¬p a)
theorem
computable_pred.to_re
{α : Type u_1}
[primcodable α]
{p : α → Prop}
(hp : computable_pred p) :
re_pred p
theorem
computable_pred.rice
(C : set (ℕ →. ℕ))
(h : computable_pred (λ (c : nat.partrec.code), c.eval ∈ C))
{f g : ℕ →. ℕ}
(hf : nat.partrec f)
(hg : nat.partrec g)
(fC : f ∈ C) :
g ∈ C
theorem
computable_pred.rice₂
(C : set nat.partrec.code)
(H : ∀ (cf cg : nat.partrec.code), cf.eval = cg.eval → (cf ∈ C ↔ cg ∈ C)) :
computable_pred (λ (c : nat.partrec.code), c ∈ C) ↔ C = ∅ ∨ C = set.univ
theorem
computable_pred.halting_problem_re
(n : ℕ) :
re_pred (λ (c : nat.partrec.code), (c.eval n).dom)
theorem
computable_pred.halting_problem
(n : ℕ) :
¬computable_pred (λ (c : nat.partrec.code), (c.eval n).dom)
@[nolint]
theorem
computable_pred.computable_iff_re_compl_re
{α : Type u_1}
[primcodable α]
{p : α → Prop}
[decidable_pred p] :
- 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' (λ (v : vector ℕ m), vector.m_of_fn (λ (i : fin n), g i v) >>= f)
- rfind : ∀ {n : ℕ} {f : vector ℕ (n + 1) → ℕ}, nat.partrec' ↑f → nat.partrec' (λ (v : vector ℕ n), nat.rfind (λ (n_1 : ℕ), part.some (decidable.to_bool (f (n_1 ::ᵥ v) = 0))))
A simplified basis for partrec.
theorem
nat.partrec'.tail
{n : ℕ}
{f : vector ℕ n →. ℕ}
(hf : nat.partrec' f) :
nat.partrec' (λ (v : vector ℕ n.succ), f v.tail)
@[protected]
theorem
nat.partrec'.bind
{n : ℕ}
{f : vector ℕ n →. ℕ}
{g : vector ℕ (n + 1) →. ℕ}
(hf : nat.partrec' f)
(hg : nat.partrec' g) :
@[protected]
@[protected]
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 (λ (v : vector ℕ n), 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' (λ (v : vector ℕ n), f (g v))
theorem
nat.partrec'.comp₁
{n : ℕ}
(f : ℕ →. ℕ)
{g : vector ℕ n → ℕ}
(hf : nat.partrec' (λ (v : vector ℕ 1), f v.head))
(hg : nat.partrec' ↑g) :
nat.partrec' (λ (v : vector ℕ n), f (g v))
theorem
nat.partrec'.rfind_opt
{n : ℕ}
{f : vector ℕ (n + 1) → ℕ}
(hf : nat.partrec' ↑f) :
nat.partrec' (λ (v : vector ℕ n), nat.rfind_opt (λ (a : ℕ), denumerable.of_nat (option ℕ) (f (a ::ᵥ v))))