mathlib3 documentation

computability.halting

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 nat.partrec.merge' {f g : →. } (hf : nat.partrec f) (hg : nat.partrec g) :
(h : →. ), nat.partrec h (a : ), ( (x : ), x h a x 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 a x 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 a x = 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 re_pred.of_eq {α : Type u_1} [primcodable α] {p q : α Prop} (hp : re_pred p) (H : (a : α), p a q a) :
theorem partrec.dom_re {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] {f : α →. β} (h : partrec f) :
re_pred (λ (a : α), (f a).dom)
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) :
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)
theorem computable_pred.computable_iff_re_compl_re' {α : Type u_1} [primcodable α] {p : α Prop} :
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)
@[protected]
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)))
@[protected]
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), part.map (λ (a : ), g (a ::ᵥ v)) (f v))
def nat.partrec'.vec {n m : } (f : vector n vector m) :
Prop

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

Equations
@[protected]
theorem nat.partrec'.nil {n : } :
@[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))))