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 : ), (∀ (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 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.

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.

    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, 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.to_re {α : Type u_1} [Primcodable α] {p : αProp} (hp : ComputablePred p) :
      theorem ComputablePred.rice (C : Set ( →. )) (h : ComputablePred fun c => Nat.Partrec.Code.eval c C) {f : →. } {g : →. } (hf : Nat.Partrec f) (hg : Nat.Partrec g) (fC : f C) :
      g C
      theorem ComputablePred.rice₂ (C : Set Nat.Partrec.Code) (H : ∀ (cf cg : Nat.Partrec.Code), Nat.Partrec.Code.eval cf = Nat.Partrec.Code.eval cg → (cf C cg C)) :
      (ComputablePred fun c => c C) C = C = Set.univ
      inductive Nat.Partrec' {n : } :

      A simplified basis for Partrec.

      Instances For
        theorem Nat.Partrec'.of_eq {n : } {f : Vector n →. } {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'.head {n : } :
        Nat.Partrec' Vector.head
        theorem Nat.Partrec'.tail {n : } {f : Vector n →. } (hf : Nat.Partrec' f) :
        Nat.Partrec' fun v => f (Vector.tail v)
        theorem Nat.Partrec'.bind {n : } {f : Vector n →. } {g : Vector (n + 1) →. } (hf : Nat.Partrec' f) (hg : Nat.Partrec' g) :
        Nat.Partrec' fun v => Part.bind (f v) fun 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' fun v => Part.map (fun a => g (a ::ᵥ v)) (f v)
        def Nat.Partrec'.Vec {n : } {m : } (f : Vector nVector m) :

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

        Instances For
          theorem Nat.Partrec'.nil {n : } :
          Nat.Partrec'.Vec fun x => Vector.nil
          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 fun v => 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' fun v => f (g v)
          theorem Nat.Partrec'.comp₁ {n : } (f : →. ) {g : Vector n} (hf : Nat.Partrec' fun v => f (Vector.head v)) (hg : Nat.Partrec' g) :
          Nat.Partrec' fun v => f (g v)
          theorem Nat.Partrec'.rfindOpt {n : } {f : Vector (n + 1)} (hf : Nat.Partrec' f) :