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.
Equations
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
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.

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
def Partrec₂ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable σ] (f : αβ →. σ) :

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

Equations
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
def Computable₂ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable σ] (f : αβσ) :

Computable functions α → β → σ between Primcodable types

Equations
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