Documentation

Mathlib.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 : ), (∀ xh 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 : α), (∀ xk 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 : α), xf a, yg 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 fun (a : α) => bif c a then f a else g a
theorem Partrec.sum_casesOn {α : 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 fun (a : α) => Sum.casesOn (f a) (g a) (h a)
def ComputablePred {α : Type u_1} [Primcodable α] (p : αProp) :

A computable predicate is one whose indicator function is computable.

Equations
Instances For
    def RePred {α : Type u_1} [Primcodable α] (p : αProp) :

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

    Equations
    Instances For
      theorem RePred.of_eq {α : Type u_1} [Primcodable α] {p : αProp} {q : αProp} (hp : RePred p) (H : ∀ (a : α), p a q a) :
      theorem Partrec.dom_re {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {f : α →. β} (h : Partrec f) :
      RePred fun (a : α) => (f a).Dom
      theorem ComputablePred.of_eq {α : Type u_1} [Primcodable α] {p : αProp} {q : αProp} (hp : ComputablePred p) (H : ∀ (a : α), p a q a) :
      theorem ComputablePred.computable_iff {α : Type u_1} [Primcodable α] {p : αProp} :
      ComputablePred p ∃ (f : αBool), Computable f p = fun (a : α) => f a = true
      theorem ComputablePred.not {α : Type u_1} [Primcodable α] {p : αProp} (hp : ComputablePred p) :
      ComputablePred fun (a : α) => ¬p a
      theorem ComputablePred.ite {f₁ : } {f₂ : } (hf₁ : Computable f₁) (hf₂ : Computable f₂) {c : Prop} [DecidablePred c] (hc : ComputablePred c) :
      Computable fun (k : ) => if c k then f₁ k else f₂ k

      The computable functions are closed under if-then-else definitions with computable predicates.

      theorem ComputablePred.to_re {α : Type u_1} [Primcodable α] {p : αProp} (hp : ComputablePred p) :
      theorem ComputablePred.rice (C : Set ( →. )) (h : ComputablePred fun (c : Nat.Partrec.Code) => c.eval C) {f : →. } {g : →. } (hf : Nat.Partrec f) (hg : Nat.Partrec g) (fC : f C) :
      g C

      Rice's Theorem

      theorem ComputablePred.rice₂ (C : Set Nat.Partrec.Code) (H : ∀ (cf cg : Nat.Partrec.Code), cf.eval = cg.eval(cf C cg C)) :
      (ComputablePred fun (c : Nat.Partrec.Code) => c C) C = C = Set.univ
      theorem ComputablePred.halting_problem_re (n : ) :
      RePred fun (c : Nat.Partrec.Code) => (c.eval n).Dom

      The Halting problem is recursively enumerable

      theorem ComputablePred.halting_problem (n : ) :
      ¬ComputablePred fun (c : Nat.Partrec.Code) => (c.eval n).Dom

      The Halting problem is not computable

      theorem ComputablePred.computable_iff_re_compl_re' {α : Type u_1} [Primcodable α] {p : αProp} :
      ComputablePred p RePred p RePred fun (a : α) => ¬p a
      inductive Nat.Partrec' {n : } :

      A simplified basis for Partrec.

      Instances For
        theorem Nat.Partrec'.of_eq {n : } {f : Mathlib.Vector n →. } {g : Mathlib.Vector n →. } (hf : Nat.Partrec' f) (H : ∀ (i : Mathlib.Vector n), f i = g i) :
        theorem Nat.Partrec'.of_prim {n : } {f : Mathlib.Vector n} (hf : Primrec f) :
        theorem Nat.Partrec'.head {n : } :
        Nat.Partrec' Mathlib.Vector.head
        theorem Nat.Partrec'.tail {n : } {f : Mathlib.Vector n →. } (hf : Nat.Partrec' f) :
        Nat.Partrec' fun (v : Mathlib.Vector n.succ) => f v.tail
        theorem Nat.Partrec'.bind {n : } {f : Mathlib.Vector n →. } {g : Mathlib.Vector (n + 1) →. } (hf : Nat.Partrec' f) (hg : Nat.Partrec' g) :
        Nat.Partrec' fun (v : Mathlib.Vector n) => (f v).bind fun (a : ) => g (a ::ᵥ v)
        theorem Nat.Partrec'.map {n : } {f : Mathlib.Vector n →. } {g : Mathlib.Vector (n + 1)} (hf : Nat.Partrec' f) (hg : Nat.Partrec' g) :
        Nat.Partrec' fun (v : Mathlib.Vector n) => Part.map (fun (a : ) => g (a ::ᵥ v)) (f v)

        Analogous to Nat.Partrec' for -valued functions, a predicate for partial recursive vector-valued functions.

        Equations
        Instances For
          theorem Nat.Partrec'.nil {n : } :
          Nat.Partrec'.Vec fun (x : Mathlib.Vector n) => Mathlib.Vector.nil
          theorem Nat.Partrec'.cons {n : } {m : } {f : Mathlib.Vector n} {g : Mathlib.Vector nMathlib.Vector m} (hf : Nat.Partrec' f) (hg : Nat.Partrec'.Vec g) :
          Nat.Partrec'.Vec fun (v : Mathlib.Vector n) => f v ::ᵥ g v
          theorem Nat.Partrec'.comp' {n : } {m : } {f : Mathlib.Vector m →. } {g : Mathlib.Vector nMathlib.Vector m} (hf : Nat.Partrec' f) (hg : Nat.Partrec'.Vec g) :
          Nat.Partrec' fun (v : Mathlib.Vector n) => f (g v)
          theorem Nat.Partrec'.comp₁ {n : } (f : →. ) {g : Mathlib.Vector n} (hf : Nat.Partrec' fun (v : Mathlib.Vector 1) => f v.head) (hg : Nat.Partrec' g) :
          Nat.Partrec' fun (v : Mathlib.Vector n) => f (g v)
          theorem Nat.Partrec'.rfindOpt {n : } {f : Mathlib.Vector (n + 1)} (hf : Nat.Partrec' f) :
          theorem Nat.Partrec'.part_iff₂ {f : →. } :
          (Nat.Partrec' fun (v : Mathlib.Vector 2) => f v.head v.tail.head) Partrec₂ f