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) :
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))
Equations
- computable_pred p = ∃ [D : decidable_pred p], computable (λ (a : α), to_bool (p a))
Equations
- re_pred p = partrec (λ (a : α), roption.assert (p a) (λ (_x : p a), roption.some ()))
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)
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
(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 : ℕ), roption.some (to_bool (f (n_1 :: v) = 0))))
A simplified basis for partrec.
theorem
nat.partrec'.of_eq
{n : ℕ}
{f g : vector ℕ n →. ℕ}
(hf : nat.partrec' f)
(H : ∀ (i : vector ℕ n), f i = g i) :
theorem
nat.partrec'.tail
{n : ℕ}
{f : vector ℕ n →. ℕ}
(hf : nat.partrec' f) :
nat.partrec' (λ (v : vector ℕ n.succ), f v.tail)
theorem
nat.partrec'.bind
{n : ℕ}
{f : vector ℕ n →. ℕ}
{g : vector ℕ (n + 1) →. ℕ}
(hf : nat.partrec' f)
(hg : nat.partrec' g) :
theorem
nat.partrec'.map
{n : ℕ}
{f : vector ℕ n →. ℕ}
{g : vector ℕ (n + 1) → ℕ}
(hf : nat.partrec' f)
(hg : nat.partrec' ↑g) :
nat.partrec' (λ (v : vector ℕ n), roption.map (λ (a : ℕ), g (a :: v)) (f v))
Equations
- nat.partrec'.vec f = ∀ (i : fin m), nat.partrec' ↑(λ (v : vector ℕ n), (f v).nth i)
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))))