# 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 : ) (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
def Nat.rfind (p : ) :
Equations
Instances For
theorem Nat.rfind_spec {p : } {n : } (h : n ) :
true p n
theorem Nat.rfind_min {p : } {n : } (h : n ) {m : } :
m < nfalse p m
@[simp]
theorem Nat.rfind_dom {p : } :
(Nat.rfind p).Dom ∃ (n : ), true p n ∀ {m : }, m < n(p m).Dom
theorem Nat.rfind_dom' {p : } :
(Nat.rfind p).Dom ∃ (n : ), true p n ∀ {m : }, m n(p m).Dom
@[simp]
theorem Nat.mem_rfind {p : } {n : } :
n true p n ∀ {m : }, m < nfalse p m
theorem Nat.rfind_min' {p : } {m : } (pm : p m = true) :
n, n m
theorem Nat.rfind_zero_none (p : ) (p0 : p 0 = Part.none) :
= Part.none
def Nat.rfindOpt {α : Type u_1} (f : ) :
Part α
Equations
Instances For
theorem Nat.rfindOpt_spec {α : Type u_1} {f : } {a : α} (h : ) :
∃ (n : ), a f n
theorem Nat.rfindOpt_dom {α : Type u_1} {f : } :
(Nat.rfindOpt f).Dom ∃ (n : ) (a : α), a f n
theorem Nat.rfindOpt_mono {α : Type u_1} {f : } (H : ∀ {a : α} {m n : }, m na f ma f n) {a : α} :
∃ (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 : ) (H : ∀ (n : ), f n = g n) :
theorem Nat.Partrec.of_eq_tot {f : } {g : } (hf : ) (H : ∀ (n : ), g n f n) :
theorem Nat.Partrec.of_primrec {f : } (hf : ) :
theorem Nat.Partrec.none :
Nat.Partrec fun (x : ) => Part.none
theorem Nat.Partrec.prec' {f : } {g : } {h : } (hf : ) (hg : ) (hh : ) :
Nat.Partrec fun (a : ) => (f a).bind fun (n : ) => Nat.rec (g a) (fun (y : ) (IH : ) => 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} [] [] (f : α →. σ) :

Partially recursive partial functions α → σ between Primcodable types

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

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

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

Computable functions α → β → σ between Primcodable types

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