mathlib documentation

computability.halting

Computability theory and the halting problem

A universal partial recursive function, Rice's theorem, and the halting problem.

References

theorem nat.partrec.merge' {f g : →. } :
nat.partrec fnat.partrec g(∃ (h : →. ), nat.partrec h ∀ (a : ), (∀ (x : ), x h ax f a x g a) ((h a).dom (f a).dom (g a).dom))

theorem partrec.merge' {α : Type u_1} {σ : Type u_4} [primcodable α] [primcodable σ] {f g : α →. σ} :
partrec fpartrec g(∃ (k : α →. σ), partrec k ∀ (a : α), (∀ (x : σ), x k ax f a x g a) ((k a).dom (f a).dom (g a).dom))

theorem partrec.merge {α : Type u_1} {σ : Type u_4} [primcodable α] [primcodable σ] {f g : α →. σ} :
partrec fpartrec g(∀ (a : α) (x : σ), x f a∀ (y : σ), y g ax = y)(∃ (k : α →. σ), partrec k ∀ (a : α) (x : σ), x k a x f a x g a)

theorem partrec.cond {α : Type u_1} {σ : Type u_4} [primcodable α] [primcodable σ] {c : α → bool} {f g : α →. σ} :
computable cpartrec fpartrec gpartrec (λ (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 fpartrec₂ gpartrec₂ hpartrec (λ (a : α), (f a).cases_on (g a) (h a))

def computable_pred {α : Type u_1} [primcodable α] :
(α → Prop) → Prop

A computable predicate is one whose indicator function is computable.

Equations
def re_pred {α : Type u_1} [primcodable α] :
(α → Prop) → Prop

A recursively enumerable predicate is one which is the domain of a computable partial function.

Equations
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 pcomputable_pred (λ (a : α), ¬p a)

theorem computable_pred.to_re {α : Type u_1} [primcodable α] {p : α → Prop} :

theorem computable_pred.rice (C : set ( →. )) (h : computable_pred (λ (c : nat.partrec.code), c.eval C)) {f g : →. } :
nat.partrec fnat.partrec gf Cg C

theorem computable_pred.rice₂ (C : set nat.partrec.code) :
(∀ (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)

@[nolint]
theorem computable_pred.computable_iff_re_compl_re {α : Type u_1} [primcodable α] {p : α → Prop} [decidable_pred p] :
computable_pred p re_pred p re_pred (λ (a : α), ¬p a)

inductive nat.partrec' {n : } :
(vector n →. ) → Prop

A simplified basis for partrec.

theorem nat.partrec'.to_part {n : } {f : vector n →. } :

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'.of_prim {n : } {f : vector n} :

theorem nat.partrec'.tail {n : } {f : vector n →. } :
nat.partrec' fnat.partrec' (λ (v : vector n.succ), f v.tail)

theorem nat.partrec'.bind {n : } {f : vector n →. } {g : vector (n + 1) →. } :
nat.partrec' fnat.partrec' gnat.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' fnat.partrec' gnat.partrec' (λ (v : vector n), roption.map (λ (a : ), g (a::ᵥv)) (f v))

def nat.partrec'.vec {n m : } :
(vector nvector m) → Prop

Analogous to nat.partrec' for -valued functions, a predicate for partial recursive vector-valued functions.

Equations
theorem nat.partrec'.nil {n : } :

theorem nat.partrec'.cons {n m : } {f : vector n} {g : vector nvector m} :

theorem nat.partrec'.comp' {n m : } {f : vector m →. } {g : vector nvector m} :
nat.partrec' fnat.partrec'.vec gnat.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' gnat.partrec' (λ (v : vector n), f (g v))

theorem nat.partrec'.rfind_opt {n : } {f : vector (n + 1)} :

theorem nat.partrec'.of_part {n : } {f : vector n →. } :