mathlib documentation

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.rfind_x (p : →. bool) (H : ∃ (n : ), tt p n ∀ (k : ), k < n(p k).dom) :
{n // tt p n ∀ (m : ), m < nff p m}
Equations
def nat.rfind (p : →. bool) :
Equations
theorem nat.rfind_spec {p : →. bool} {n : } (h : n nat.rfind p) :
tt p n
theorem nat.rfind_min {p : →. bool} {n : } (h : n nat.rfind p) {m : } :
m < nff p m
@[simp]
theorem nat.rfind_dom {p : →. bool} :
(nat.rfind p).dom ∃ (n : ), tt p n ∀ {m : }, m < n(p m).dom
theorem nat.rfind_dom' {p : →. bool} :
(nat.rfind p).dom ∃ (n : ), tt p n ∀ {m : }, m n(p m).dom
@[simp]
theorem nat.mem_rfind {p : →. bool} {n : } :
n nat.rfind p tt p n ∀ {m : }, m < nff p m
theorem nat.rfind_min' {p : bool} {m : } (pm : (p m)) :
∃ (n : ) (H : n nat.rfind p), n m
def nat.rfind_opt {α : Type u_1} (f : option α) :
part α
Equations
theorem nat.rfind_opt_spec {α : Type u_1} {f : option α} {a : α} (h : a nat.rfind_opt f) :
∃ (n : ), a f n
theorem nat.rfind_opt_dom {α : Type u_1} {f : option α} :
(nat.rfind_opt f).dom ∃ (n : ) (a : α), a f n
theorem nat.rfind_opt_mono {α : Type u_1} {f : option α} (H : ∀ {a : α} {m n : }, m na f ma f n) {a : α} :
a nat.rfind_opt f ∃ (n : ), a f n
inductive nat.partrec  :
( →. ) → Prop
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  :
theorem nat.partrec.prec' {f g h : →. } (hf : nat.partrec f) (hg : nat.partrec g) (hh : nat.partrec h) :
nat.partrec (λ (a : ), (f a).bind (λ (n : ), nat.elim (g a) (λ (y : ) (IH : part ), IH >>= λ (i : ), h (nat.mkpair a (nat.mkpair y i))) n))
theorem nat.partrec.ppred  :
nat.partrec (λ (n : ), (n.ppred))
def partrec {α : Type u_1} {σ : Type u_2} [primcodable α] [primcodable σ] (f : α →. σ) :
Prop
Equations
def partrec₂ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [primcodable α] [primcodable β] [primcodable σ] (f : α → β →. σ) :
Prop
Equations
def computable {α : Type u_1} {σ : Type u_2} [primcodable α] [primcodable σ] (f : α → σ) :
Prop
Equations
def computable₂ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [primcodable α] [primcodable β] [primcodable σ] (f : α → β → σ) :
Prop
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) :
theorem computable₂.partrec₂ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [primcodable α] [primcodable β] [primcodable σ] {f : α → β → σ} (hf : computable₂ f) :
partrec₂ (λ (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 (λ (a : α), s)
theorem computable.of_option {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] {f : α → option β} (hf : computable f) :
partrec (λ (a : α), (f a))
theorem computable.to₂ {α : Type u_1} {β : Type u_2} {σ : Type u_4} [primcodable α] [primcodable β] [primcodable σ] {f : α × β → σ} (hf : computable f) :
computable₂ (λ (a : α) (b : β), f (a, b))
theorem computable.id {α : Type u_1} [primcodable α] :
theorem computable.fst {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] :
theorem computable.snd {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] :
theorem computable.pair {α : Type u_1} {β : Type u_2} {γ : Type u_3} [primcodable α] [primcodable β] [primcodable γ] {f : α → β} {g : α → γ} (hf : computable f) (hg : computable g) :
computable (λ (a : α), (f a, g a))
theorem computable.sum_inl {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] :
theorem computable.sum_inr {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] :
theorem computable.list_nth {α : Type u_1} [primcodable α] :
theorem computable.list_concat {α : Type u_1} [primcodable α] :
computable₂ (λ (l : list α) (a : α), l ++ [a])
theorem computable.vector_cons {α : Type u_1} [primcodable α] {n : } :
theorem computable.vector_length {α : Type u_1} [primcodable α] {n : } :
theorem computable.vector_head {α : Type u_1} [primcodable α] {n : } :
theorem computable.vector_tail {α : Type u_1} [primcodable α] {n : } :
theorem computable.vector_nth {α : Type u_1} [primcodable α] {n : } :
theorem computable.vector_nth' {α : Type u_1} [primcodable α] {n : } :
theorem computable.vector_of_fn' {α : Type u_1} [primcodable α] {n : } :
theorem computable.fin_app {σ : Type u_4} [primcodable σ] {n : } :
theorem computable.decode {α : Type u_1} [primcodable α] :
theorem computable.of_nat (α : Type u_1) [denumerable α] :
theorem computable.encode_iff {α : Type u_1} {σ : Type u_4} [primcodable α] [primcodable σ] {f : α → σ} :
computable (λ (a : α), encodable.encode (f a)) computable f
theorem computable.option_some {α : Type u_1} [primcodable α] :
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 (λ (a : α), part.none)
theorem partrec.some {α : Type u_1} [primcodable α] :
theorem decidable.partrec.const' {α : Type u_1} {σ : Type u_4} [primcodable α] [primcodable σ] (s : part σ) [decidable s.dom] :
partrec (λ (a : α), s)
theorem partrec.const' {α : Type u_1} {σ : Type u_4} [primcodable α] [primcodable σ] (s : part σ) :
partrec (λ (a : α), 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 (λ (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 (λ (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₂ (λ (a : α) (b : β), f (a, b))
theorem partrec.nat_elim {α : Type u_1} {σ : Type u_4} [primcodable α] [primcodable σ] {f : α → } {g : α →. σ} {h : α → × σ →. σ} (hf : computable f) (hg : partrec g) (hh : partrec₂ h) :
partrec (λ (a : α), nat.elim (g a) (λ (y : ) (IH : part σ), IH.bind (λ (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 (λ (a : α), f (g a))
theorem partrec.map_encode_iff {α : Type u_1} {σ : Type u_4} [primcodable α] [primcodable σ] {f : α →. σ} :
theorem partrec₂.unpaired {α : Type u_1} [primcodable α] {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 (λ (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₂ (λ (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 (λ (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₂ (λ (a : α) (b : β), f (g a b))
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 (λ (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₂ (λ (a : α) (b : β), f (g a b) (h a b))
theorem partrec.rfind {α : Type u_1} [primcodable α] {p : α → →. bool} (hp : partrec₂ p) :
partrec (λ (a : α), nat.rfind (p a))
theorem partrec.rfind_opt {α : Type u_1} {σ : Type u_4} [primcodable α] [primcodable σ] {f : α → option σ} (hf : computable₂ f) :
partrec (λ (a : α), nat.rfind_opt (f a))
theorem partrec.nat_cases_right {α : Type u_1} {σ : Type u_4} [primcodable α] [primcodable σ] {f : α → } {g : α → σ} {h : α → →. σ} (hf : computable f) (hg : computable g) (hh : partrec₂ h) :
partrec (λ (a : α), nat.cases (part.some (g a)) (h a) (f a))
theorem partrec.bind_decode₂_iff {α : Type u_1} {σ : Type u_4} [primcodable α] [primcodable σ] {f : α →. σ} :
theorem partrec.vector_m_of_fn {α : Type u_1} {σ : Type u_4} [primcodable α] [primcodable σ] {n : } {f : fin nα →. σ} :
(∀ (i : fin n), partrec (f i))partrec (λ (a : α), vector.m_of_fn (λ (i : fin n), f i a))
@[simp]
theorem vector.m_of_fn_part_some {α : Type u_1} {n : } (f : fin n → α) :
theorem computable.option_some_iff {α : Type u_1} {σ : Type u_4} [primcodable α] [primcodable σ] {f : α → σ} :
computable (λ (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₂ (λ (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₂ (λ (a : α) (n : ), option.map (f a) (encodable.decode β n)) computable₂ f
theorem computable.nat_elim {α : Type u_1} {σ : Type u_4} [primcodable α] [primcodable σ] {f : α → } {g : α → σ} {h : α → × σ → σ} (hf : computable f) (hg : computable g) (hh : computable₂ h) :
computable (λ (a : α), nat.elim (g a) (λ (y : ) (IH : σ), h a (y, IH)) (f a))
theorem computable.nat_cases {α : Type u_1} {σ : Type u_4} [primcodable α] [primcodable σ] {f : α → } {g : α → σ} {h : α → → σ} (hf : computable f) (hg : computable g) (hh : computable₂ h) :
computable (λ (a : α), nat.cases (g a) (h a) (f 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 (λ (a : α), cond (c a) (f a) (g a))
theorem computable.option_cases {α : 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 (λ (a : α), (o a).cases_on (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 (λ (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 (λ (a : α), option.map (g a) (f a))
theorem computable.option_get_or_else {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] {f : α → option β} {g : α → β} (hf : computable f) (hg : computable g) :
computable (λ (a : α), (f a).get_or_else (g a))
theorem computable.subtype_mk {α : Type u_1} {β : Type u_2} [primcodable α] [primcodable β] {f : α → β} {p : β → Prop} [decidable_pred p] {h : ∀ (a : α), p (f a)} (hp : primrec_pred p) (hf : computable f) :
computable (λ (a : α), f a, _⟩)
theorem computable.sum_cases {α : 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 (λ (a : α), (f a).cases_on (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_of_fn {α : Type u_1} {σ : Type u_4} [primcodable α] [primcodable σ] {n : } {f : fin nα → σ} :
(∀ (i : fin n), computable (f i))computable (λ (a : α), list.of_fn (λ (i : fin n), f i a))
theorem computable.vector_of_fn {α : Type u_1} {σ : Type u_4} [primcodable α] [primcodable σ] {n : } {f : fin nα → σ} (hf : ∀ (i : fin n), computable (f i)) :
computable (λ (a : α), vector.of_fn (λ (i : fin n), f i a))
theorem partrec.option_some_iff {α : Type u_1} {σ : Type u_4} [primcodable α] [primcodable σ] {f : α →. σ} :
partrec (λ (a : α), part.map some (f a)) partrec f
theorem partrec.option_cases_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 (λ (a : α), (o a).cases_on (part.some (f a)) (g a))
theorem partrec.sum_cases_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 (λ (a : α), (f a).cases_on (λ (b : β), part.some (g a b)) (h a))
theorem partrec.sum_cases_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 (λ (a : α), (f a).cases_on (g a) (λ (c : γ), part.some (h a c)))
theorem partrec.fix_aux {α : Type u_1} {σ : Type u_2} (f : α →. σ α) (a : α) (b : σ) :
let F : α → →. σ α := λ (a : α) (n : ), nat.elim (part.some (sum.inr a)) (λ (y : ) (IH : part α)), IH.bind (λ (s : σ α), s.cases_on (λ (_x : σ), part.some s) f)) n in (∃ (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) :