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 roption 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 α) :

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.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 : roption ), IH >>= λ (i : ), h (a.mkpair (y.mkpair 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.part {α : Type u_1} {σ : Type u_2} [primcodable α] [primcodable σ] {f : α → σ} (hf : computable f) :

theorem computable₂.part {α : 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 : α), roption.none)

theorem partrec.some {α : Type u_1} [primcodable α] :

theorem partrec.const' {α : Type u_1} {σ : Type u_4} [primcodable α] [primcodable σ] (s : roption σ) :
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 : α), roption.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 : roption σ), 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 (roption.some (g a)) (h a) (f a))

theorem partrec.bind_decode2_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_roption_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 : α), roption.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 (roption.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 : β), roption.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 : γ), roption.some (h a c)))

theorem partrec.fix {α : Type u_1} {σ : Type u_4} [primcodable α] [primcodable σ] {f : α →. σ α} (hf : partrec f) :