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 : →. } (hf : nat.partrec f) (hg : nat.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 : α →. σ} (hf : partrec f) (hg : partrec 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 : α →. σ} (hf : partrec f) (hg : partrec g) (H : ∀ (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 : α →. σ} (hc : computable c) (hf : partrec f) (hg : 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 : α → γ →. σ} (hf : computable f) (hg : partrec₂ g) (hh : partrec₂ h) :
partrec (λ (a : α), (f a).cases_on (g a) (h a))

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

A computable predicate is one whose indicator function is computable.

Equations
def re_pred {α : Type u_1} [primcodable α] (p : α → 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} (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) :

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)) :

@[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 →. } (pf : nat.partrec' f) :

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

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) :
nat.partrec' (λ (v : vector n), (f v).bind (λ (a : ), g (a::ᵥv)))

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))

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

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

Equations
theorem nat.partrec'.vec.prim {n m : } {f : vector nvector m} (hf : nat.primrec'.vec f) :

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

theorem nat.partrec'.cons {n m : } {f : vector n} {g : vector nvector 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 nvector 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) :

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