Documentation

Mathlib.Computability.Partrec

The partial recursive functions #

The partial recursive functions are defined similarly to the primitive recursive functions, but now all functions are partial, implemented using the Part monad, and there is an additional operation, called μ-recursion, which performs unbounded minimization.

References #

def Nat.rfindX (p : →. Bool) (H : ∃ (n : ), true p n k < n, (p k).Dom) :
{ n : // true p n m < n, false p m }
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    Equations
    Instances For
      theorem Nat.rfind_spec {p : →. Bool} {n : } (h : n Nat.rfind p) :
      true p n
      theorem Nat.rfind_min {p : →. Bool} {n : } (h : n Nat.rfind p) {m : } :
      m < nfalse p m
      @[simp]
      theorem Nat.rfind_dom {p : →. Bool} :
      (Nat.rfind p).Dom ∃ (n : ), true p n ∀ {m : }, m < n(p m).Dom
      theorem Nat.rfind_dom' {p : →. Bool} :
      (Nat.rfind p).Dom ∃ (n : ), true p n ∀ {m : }, m n(p m).Dom
      @[simp]
      theorem Nat.mem_rfind {p : →. Bool} {n : } :
      n Nat.rfind p true p n ∀ {m : }, m < nfalse p m
      theorem Nat.rfind_min' {p : Bool} {m : } (pm : p m = true) :
      nNat.rfind p, n m
      theorem Nat.rfind_zero_none (p : →. Bool) (p0 : p 0 = Part.none) :
      Nat.rfind p = Part.none
      def Nat.rfindOpt {α : Type u_1} (f : Option α) :
      Part α
      Equations
      Instances For
        theorem Nat.rfindOpt_spec {α : Type u_1} {f : Option α} {a : α} (h : a Nat.rfindOpt f) :
        ∃ (n : ), a f n
        theorem Nat.rfindOpt_dom {α : Type u_1} {f : Option α} :
        (Nat.rfindOpt f).Dom ∃ (n : ) (a : α), a f n
        theorem Nat.rfindOpt_mono {α : Type u_1} {f : Option α} (H : ∀ {a : α} {m n : }, m na f ma f n) {a : α} :
        a Nat.rfindOpt f ∃ (n : ), a f n
        inductive Nat.Partrec :

        PartRec f means that the partial function f : ℕ → ℕ is partially recursive.

        Instances For
          theorem Nat.Partrec.of_eq {f : →. } {g : →. } (hf : Nat.Partrec f) (H : ∀ (n : ), f n = g n) :
          theorem Nat.Partrec.of_eq_tot {f : →. } {g : } (hf : Nat.Partrec f) (H : ∀ (n : ), g n f n) :
          theorem Nat.Partrec.none :
          Nat.Partrec fun (x : ) => Part.none
          theorem Nat.Partrec.prec' {f : →. } {g : →. } {h : →. } (hf : Nat.Partrec f) (hg : Nat.Partrec g) (hh : Nat.Partrec h) :
          Nat.Partrec fun (a : ) => (f a).bind fun (n : ) => Nat.rec (g a) (fun (y : ) (IH : Part ) => do let iIH h (Nat.pair a (Nat.pair y i))) n
          theorem Nat.Partrec.ppred :
          Nat.Partrec fun (n : ) => n.ppred
          def Partrec {α : Type u_1} {σ : Type u_2} [Primcodable α] [Primcodable σ] (f : α →. σ) :

          Partially recursive partial functions α → σ between Primcodable types

          Equations
          Instances For
            def Partrec₂ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable σ] (f : αβ →. σ) :

            Partially recursive partial functions α → β → σ between Primcodable types

            Equations
            Instances For
              def Computable {α : Type u_1} {σ : Type u_2} [Primcodable α] [Primcodable σ] (f : ασ) :

              Computable functions α → σ between Primcodable types: a function is computable if and only if it is partially recursive (as a partial function)

              Equations
              Instances For
                def Computable₂ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable σ] (f : αβσ) :

                Computable functions α → β → σ between Primcodable types

                Equations
                Instances For
                  theorem Primrec.to_comp {α : Type u_1} {σ : Type u_2} [Primcodable α] [Primcodable σ] {f : ασ} (hf : Primrec f) :
                  theorem Primrec₂.to_comp {α : Type u_1} {β : Type u_2} {σ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable σ] {f : αβσ} (hf : Primrec₂ f) :
                  theorem Computable.partrec {α : Type u_1} {σ : Type u_2} [Primcodable α] [Primcodable σ] {f : ασ} (hf : Computable f) :
                  Partrec f
                  theorem Computable₂.partrec₂ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable σ] {f : αβσ} (hf : Computable₂ f) :
                  Partrec₂ fun (a : α) => (f a)
                  theorem Computable.of_eq {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {f : ασ} {g : ασ} (hf : Computable f) (H : ∀ (n : α), f n = g n) :
                  theorem Computable.const {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] (s : σ) :
                  Computable fun (x : α) => s
                  theorem Computable.ofOption {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {f : αOption β} (hf : Computable f) :
                  Partrec fun (a : α) => (f a)
                  theorem Computable.to₂ {α : Type u_1} {β : Type u_2} {σ : Type u_4} [Primcodable α] [Primcodable β] [Primcodable σ] {f : α × βσ} (hf : Computable f) :
                  Computable₂ fun (a : α) (b : β) => f (a, b)
                  theorem Computable.id {α : Type u_1} [Primcodable α] :
                  theorem Computable.fst {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] :
                  Computable Prod.fst
                  theorem Computable.snd {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] :
                  Computable Prod.snd
                  theorem Computable.pair {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable γ] {f : αβ} {g : αγ} (hf : Computable f) (hg : Computable g) :
                  Computable fun (a : α) => (f a, g a)
                  theorem Computable.sum_inl {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] :
                  Computable Sum.inl
                  theorem Computable.sum_inr {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] :
                  Computable Sum.inr
                  theorem Computable.list_cons {α : Type u_1} [Primcodable α] :
                  Computable₂ List.cons
                  theorem Computable.list_reverse {α : Type u_1} [Primcodable α] :
                  Computable List.reverse
                  theorem Computable.list_get? {α : Type u_1} [Primcodable α] :
                  Computable₂ List.get?
                  theorem Computable.list_append {α : Type u_1} [Primcodable α] :
                  Computable₂ fun (x1 x2 : List α) => x1 ++ x2
                  theorem Computable.list_concat {α : Type u_1} [Primcodable α] :
                  Computable₂ fun (l : List α) (a : α) => l ++ [a]
                  theorem Computable.list_length {α : Type u_1} [Primcodable α] :
                  Computable List.length
                  theorem Computable.vector_cons {α : Type u_1} [Primcodable α] {n : } :
                  Computable₂ Mathlib.Vector.cons
                  theorem Computable.vector_toList {α : Type u_1} [Primcodable α] {n : } :
                  Computable Mathlib.Vector.toList
                  theorem Computable.vector_length {α : Type u_1} [Primcodable α] {n : } :
                  Computable Mathlib.Vector.length
                  theorem Computable.vector_head {α : Type u_1} [Primcodable α] {n : } :
                  Computable Mathlib.Vector.head
                  theorem Computable.vector_tail {α : Type u_1} [Primcodable α] {n : } :
                  Computable Mathlib.Vector.tail
                  theorem Computable.vector_get {α : Type u_1} [Primcodable α] {n : } :
                  Computable₂ Mathlib.Vector.get
                  theorem Computable.vector_ofFn' {α : Type u_1} [Primcodable α] {n : } :
                  Computable Mathlib.Vector.ofFn
                  theorem Computable.fin_app {σ : Type u_4} [Primcodable σ] {n : } :
                  theorem Computable.encode {α : Type u_1} [Primcodable α] :
                  Computable Encodable.encode
                  theorem Computable.decode {α : Type u_1} [Primcodable α] :
                  Computable Encodable.decode
                  theorem Computable.encode_iff {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {f : ασ} :
                  (Computable fun (a : α) => Encodable.encode (f a)) Computable f
                  theorem Partrec.of_eq {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {f : α →. σ} {g : α →. σ} (hf : Partrec f) (H : ∀ (n : α), f n = g n) :
                  theorem Partrec.of_eq_tot {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {f : α →. σ} {g : ασ} (hf : Partrec f) (H : ∀ (n : α), g n f n) :
                  theorem Partrec.none {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] :
                  Partrec fun (x : α) => Part.none
                  theorem Partrec.some {α : Type u_1} [Primcodable α] :
                  Partrec Part.some
                  theorem Decidable.Partrec.const' {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] (s : Part σ) [Decidable s.Dom] :
                  Partrec fun (x : α) => s
                  theorem Partrec.const' {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] (s : Part σ) :
                  Partrec fun (x : α) => s
                  theorem Partrec.bind {α : Type u_1} {β : Type u_2} {σ : Type u_4} [Primcodable α] [Primcodable β] [Primcodable σ] {f : α →. β} {g : αβ →. σ} (hf : Partrec f) (hg : Partrec₂ g) :
                  Partrec fun (a : α) => (f a).bind (g a)
                  theorem Partrec.map {α : Type u_1} {β : Type u_2} {σ : Type u_4} [Primcodable α] [Primcodable β] [Primcodable σ] {f : α →. β} {g : αβσ} (hf : Partrec f) (hg : Computable₂ g) :
                  Partrec fun (a : α) => Part.map (g a) (f a)
                  theorem Partrec.to₂ {α : Type u_1} {β : Type u_2} {σ : Type u_4} [Primcodable α] [Primcodable β] [Primcodable σ] {f : α × β →. σ} (hf : Partrec f) :
                  Partrec₂ fun (a : α) (b : β) => f (a, b)
                  theorem Partrec.nat_rec {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {f : α} {g : α →. σ} {h : α × σ →. σ} (hf : Computable f) (hg : Partrec g) (hh : Partrec₂ h) :
                  Partrec fun (a : α) => Nat.rec (g a) (fun (y : ) (IH : Part σ) => IH.bind fun (i : σ) => h a (y, i)) (f a)
                  theorem Partrec.comp {α : Type u_1} {β : Type u_2} {σ : Type u_4} [Primcodable α] [Primcodable β] [Primcodable σ] {f : β →. σ} {g : αβ} (hf : Partrec f) (hg : Computable g) :
                  Partrec fun (a : α) => f (g a)
                  theorem Partrec.map_encode_iff {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {f : α →. σ} :
                  (Partrec fun (a : α) => Part.map Encodable.encode (f a)) Partrec f
                  theorem Partrec₂.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_5} [Primcodable α] [Primcodable β] [Primcodable γ] [Primcodable σ] {f : βγ →. σ} {g : αβ} {h : αγ} (hf : Partrec₂ f) (hg : Computable g) (hh : Computable h) :
                  Partrec fun (a : α) => f (g a) (h a)
                  theorem Partrec₂.comp₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {σ : Type u_5} [Primcodable α] [Primcodable β] [Primcodable γ] [Primcodable δ] [Primcodable σ] {f : γδ →. σ} {g : αβγ} {h : αβδ} (hf : Partrec₂ f) (hg : Computable₂ g) (hh : Computable₂ h) :
                  Partrec₂ fun (a : α) (b : β) => f (g a b) (h a b)
                  theorem Computable.comp {α : Type u_1} {β : Type u_2} {σ : Type u_4} [Primcodable α] [Primcodable β] [Primcodable σ] {f : βσ} {g : αβ} (hf : Computable f) (hg : Computable g) :
                  Computable fun (a : α) => f (g a)
                  theorem Computable.comp₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_4} [Primcodable α] [Primcodable β] [Primcodable γ] [Primcodable σ] {f : γσ} {g : αβγ} (hf : Computable f) (hg : Computable₂ g) :
                  Computable₂ fun (a : α) (b : β) => f (g a b)
                  theorem Computable₂.mk {α : Type u_1} {β : Type u_2} {σ : Type u_5} [Primcodable α] [Primcodable β] [Primcodable σ] {f : αβσ} (hf : Computable fun (p : α × β) => f p.1 p.2) :
                  theorem Computable₂.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_5} [Primcodable α] [Primcodable β] [Primcodable γ] [Primcodable σ] {f : βγσ} {g : αβ} {h : αγ} (hf : Computable₂ f) (hg : Computable g) (hh : Computable h) :
                  Computable fun (a : α) => f (g a) (h a)
                  theorem Computable₂.comp₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {σ : Type u_5} [Primcodable α] [Primcodable β] [Primcodable γ] [Primcodable δ] [Primcodable σ] {f : γδσ} {g : αβγ} {h : αβδ} (hf : Computable₂ f) (hg : Computable₂ g) (hh : Computable₂ h) :
                  Computable₂ fun (a : α) (b : β) => f (g a b) (h a b)
                  theorem Partrec.rfind {α : Type u_1} [Primcodable α] {p : α →. Bool} (hp : Partrec₂ p) :
                  Partrec fun (a : α) => Nat.rfind (p a)
                  theorem Partrec.rfindOpt {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {f : αOption σ} (hf : Computable₂ f) :
                  Partrec fun (a : α) => Nat.rfindOpt (f a)
                  theorem Partrec.nat_casesOn_right {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {f : α} {g : ασ} {h : α →. σ} (hf : Computable f) (hg : Computable g) (hh : Partrec₂ h) :
                  Partrec fun (a : α) => Nat.casesOn (f a) (Part.some (g a)) (h a)
                  theorem Partrec.bind_decode₂_iff {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {f : α →. σ} :
                  Partrec f Nat.Partrec fun (n : ) => (↑(Encodable.decode₂ α n)).bind fun (a : α) => Part.map Encodable.encode (f a)
                  theorem Partrec.vector_mOfFn {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {n : } {f : Fin nα →. σ} :
                  (∀ (i : Fin n), Partrec (f i))Partrec fun (a : α) => Mathlib.Vector.mOfFn fun (i : Fin n) => f i a
                  @[simp]
                  theorem Vector.mOfFn_part_some {α : Type u_1} {n : } (f : Fin nα) :
                  theorem Computable.option_some_iff {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {f : ασ} :
                  (Computable fun (a : α) => some (f a)) Computable f
                  theorem Computable.bind_decode_iff {α : Type u_1} {β : Type u_2} {σ : Type u_4} [Primcodable α] [Primcodable β] [Primcodable σ] {f : αβOption σ} :
                  (Computable₂ fun (a : α) (n : ) => (Encodable.decode n).bind (f a)) Computable₂ f
                  theorem Computable.map_decode_iff {α : Type u_1} {β : Type u_2} {σ : Type u_4} [Primcodable α] [Primcodable β] [Primcodable σ] {f : αβσ} :
                  (Computable₂ fun (a : α) (n : ) => Option.map (f a) (Encodable.decode n)) Computable₂ f
                  theorem Computable.nat_rec {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {f : α} {g : ασ} {h : α × σσ} (hf : Computable f) (hg : Computable g) (hh : Computable₂ h) :
                  Computable fun (a : α) => Nat.rec (g a) (fun (y : ) (IH : (fun (x : ) => σ) y) => h a (y, IH)) (f a)
                  theorem Computable.nat_casesOn {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {f : α} {g : ασ} {h : ασ} (hf : Computable f) (hg : Computable g) (hh : Computable₂ h) :
                  Computable fun (a : α) => Nat.casesOn (f a) (g a) (h a)
                  theorem Computable.cond {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {c : αBool} {f : ασ} {g : ασ} (hc : Computable c) (hf : Computable f) (hg : Computable g) :
                  Computable fun (a : α) => bif c a then f a else g a
                  theorem Computable.option_casesOn {α : Type u_1} {β : Type u_2} {σ : Type u_4} [Primcodable α] [Primcodable β] [Primcodable σ] {o : αOption β} {f : ασ} {g : αβσ} (ho : Computable o) (hf : Computable f) (hg : Computable₂ g) :
                  Computable fun (a : α) => Option.casesOn (o a) (f a) (g a)
                  theorem Computable.option_bind {α : Type u_1} {β : Type u_2} {σ : Type u_4} [Primcodable α] [Primcodable β] [Primcodable σ] {f : αOption β} {g : αβOption σ} (hf : Computable f) (hg : Computable₂ g) :
                  Computable fun (a : α) => (f a).bind (g a)
                  theorem Computable.option_map {α : Type u_1} {β : Type u_2} {σ : Type u_4} [Primcodable α] [Primcodable β] [Primcodable σ] {f : αOption β} {g : αβσ} (hf : Computable f) (hg : Computable₂ g) :
                  Computable fun (a : α) => Option.map (g a) (f a)
                  theorem Computable.option_getD {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {f : αOption β} {g : αβ} (hf : Computable f) (hg : Computable g) :
                  Computable fun (a : α) => (f a).getD (g a)
                  theorem Computable.subtype_mk {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {f : αβ} {p : βProp} [DecidablePred p] {h : ∀ (a : α), p (f a)} (hp : PrimrecPred p) (hf : Computable f) :
                  Computable fun (a : α) => f a,
                  theorem Computable.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 : Computable₂ g) (hh : Computable₂ h) :
                  Computable fun (a : α) => Sum.casesOn (f a) (g a) (h a)
                  theorem Computable.nat_strong_rec {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] (f : ασ) {g : αList σOption σ} (hg : Computable₂ g) (H : ∀ (a : α) (n : ), g a (List.map (f a) (List.range n)) = some (f a n)) :
                  theorem Computable.list_ofFn {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {n : } {f : Fin nασ} :
                  (∀ (i : Fin n), Computable (f i))Computable fun (a : α) => List.ofFn fun (i : Fin n) => f i a
                  theorem Computable.vector_ofFn {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {n : } {f : Fin nασ} (hf : ∀ (i : Fin n), Computable (f i)) :
                  Computable fun (a : α) => Mathlib.Vector.ofFn fun (i : Fin n) => f i a
                  theorem Partrec.option_some_iff {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {f : α →. σ} :
                  (Partrec fun (a : α) => Part.map some (f a)) Partrec f
                  theorem Partrec.option_casesOn_right {α : Type u_1} {β : Type u_2} {σ : Type u_4} [Primcodable α] [Primcodable β] [Primcodable σ] {o : αOption β} {f : ασ} {g : αβ →. σ} (ho : Computable o) (hf : Computable f) (hg : Partrec₂ g) :
                  Partrec fun (a : α) => Option.casesOn (o a) (Part.some (f a)) (g a)
                  theorem Partrec.sum_casesOn_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_4} [Primcodable α] [Primcodable β] [Primcodable γ] [Primcodable σ] {f : αβ γ} {g : αβσ} {h : αγ →. σ} (hf : Computable f) (hg : Computable₂ g) (hh : Partrec₂ h) :
                  Partrec fun (a : α) => Sum.casesOn (f a) (fun (b : β) => Part.some (g a b)) (h a)
                  theorem Partrec.sum_casesOn_left {α : 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 : Computable₂ h) :
                  Partrec fun (a : α) => Sum.casesOn (f a) (g a) fun (c : γ) => Part.some (h a c)
                  theorem Partrec.fix_aux {α : Type u_5} {σ : Type u_6} (f : α →. σ α) (a : α) (b : σ) :
                  let F := fun (a : α) (n : ) => Nat.rec (Part.some (Sum.inr a)) (fun (x : ) (IH : Part (σ α)) => IH.bind fun (s : σ α) => Sum.casesOn s (fun (x : σ) => Part.some s) f) n; (∃ (n : ), ((∃ (b' : σ), Sum.inl b' F a n) ∀ {m : }, m < n∃ (b : α), Sum.inr b F a m) Sum.inl b F a n) b f.fix a
                  theorem Partrec.fix {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {f : α →. σ α} (hf : Partrec f) :
                  Partrec f.fix