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 : α →. σ} :
computable c → partrec f → partrec g → partrec (λ (a : α), cond (c a) (f a) (g a))
theorem
partrec.sum_cases
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{σ : Type u_4}
[primcodable α]
[primcodable β]
[primcodable γ]
[primcodable σ]
{f : α → β ⊕ γ}
{g : α → β →. σ}
{h : α → γ →. σ} :
computable f → partrec₂ g → partrec₂ h → partrec (λ (a : α), (f a).cases_on (g a) (h a))
Equations
- computable_pred p = ∃ [D : decidable_pred p], computable (λ (a : α), decidable.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} :
computable_pred p → (∀ (a : α), p a ↔ q a) → computable_pred q
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} :
computable_pred p → computable_pred (λ (a : α), ¬p a)
theorem
computable_pred.to_re
{α : Type u_1}
[primcodable α]
{p : α → Prop} :
computable_pred p → re_pred p
theorem
computable_pred.rice
(C : set (ℕ →. ℕ))
(h : computable_pred (λ (c : nat.partrec.code), c.eval ∈ C))
{f g : ℕ →. ℕ} :
nat.partrec f → nat.partrec g → f ∈ C → g ∈ C
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 (decidable.to_bool (f (n_1 :: v) = 0))))
A simplified basis for partrec.
theorem
nat.partrec'.of_eq
{n : ℕ}
{f g : vector ℕ n →. ℕ} :
nat.partrec' f → (∀ (i : vector ℕ n), f i = g i) → nat.partrec' g
theorem
nat.partrec'.tail
{n : ℕ}
{f : vector ℕ n →. ℕ} :
nat.partrec' f → nat.partrec' (λ (v : vector ℕ n.succ), f v.tail)
theorem
nat.partrec'.bind
{n : ℕ}
{f : vector ℕ n →. ℕ}
{g : vector ℕ (n + 1) →. ℕ} :
nat.partrec' f → nat.partrec' g → nat.partrec' (λ (v : vector ℕ n), (f v).bind (λ (a : ℕ), g (a :: v)))
theorem
nat.partrec'.map
{n : ℕ}
{f : vector ℕ n →. ℕ}
{g : vector ℕ (n + 1) → ℕ} :
nat.partrec' f → 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} :
nat.partrec' ↑f → 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} :
nat.partrec' f → nat.partrec'.vec g → nat.partrec' (λ (v : vector ℕ n), f (g v))
theorem
nat.partrec'.comp₁
{n : ℕ}
(f : ℕ →. ℕ)
{g : vector ℕ n → ℕ} :
nat.partrec' (λ (v : vector ℕ 1), f v.head) → nat.partrec' ↑g → nat.partrec' (λ (v : vector ℕ n), f (g v))
theorem
nat.partrec'.rfind_opt
{n : ℕ}
{f : vector ℕ (n + 1) → ℕ} :
nat.partrec' ↑f → nat.partrec' (λ (v : vector ℕ n), nat.rfind_opt (λ (a : ℕ), denumerable.of_nat (option ℕ) (f (a :: v))))