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) :
(∃ (n : ), tt p n ∀ (k : ), k < n(p k).dom){n // tt p n ∀ (m : ), m < nff p m}

Equations
def nat.rfind  :

Equations
theorem nat.rfind_spec {p : →. bool} {n : } :
n nat.rfind ptt 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 : } :
(p m)(∃ (n : ) (H : n nat.rfind p), n m)

def nat.rfind_opt {α : Type u_1} :
(option α)roption α

Equations
theorem nat.rfind_opt_spec {α : Type u_1} {f : option α} {a : α} :
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 : →. } :
nat.partrec f(∀ (n : ), f n = g n)nat.partrec g

theorem nat.partrec.of_eq_tot {f : →. } {g : } :
nat.partrec f(∀ (n : ), g n f n)nat.partrec g

theorem nat.partrec.prec' {f g h : →. } :
nat.partrec fnat.partrec gnat.partrec hnat.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 σ] :
→. σ) → Prop

Equations
def partrec₂ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [primcodable α] [primcodable β] [primcodable σ] :
(α → β →. σ) → Prop

Equations
def computable {α : Type u_1} {σ : Type u_2} [primcodable α] [primcodable σ] :
(α → σ) → Prop

Equations
def computable₂ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [primcodable α] [primcodable β] [primcodable σ] :
(α → β → σ) → Prop

Equations
theorem primrec.to_comp {α : Type u_1} {σ : Type u_2} [primcodable α] [primcodable σ] {f : α → σ} :

theorem primrec₂.to_comp {α : Type u_1} {β : Type u_2} {σ : Type u_3} [primcodable α] [primcodable β] [primcodable σ] {f : α → β → σ} :

theorem computable.part {α : Type u_1} {σ : Type u_2} [primcodable α] [primcodable σ] {f : α → σ} :

theorem computable₂.part {α : Type u_1} {β : Type u_2} {σ : Type u_3} [primcodable α] [primcodable β] [primcodable σ] {f : α → β → σ} :
computable₂ fpartrec₂ (λ (a : α), (f a))

theorem computable.of_eq {α : Type u_1} {σ : Type u_4} [primcodable α] [primcodable σ] {f g : α → σ} :
computable f(∀ (n : α), f n = g n)computable g

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 β} :
computable fpartrec (λ (a : α), (f a))

theorem computable.to₂ {α : Type u_1} {β : Type u_2} {σ : Type u_4} [primcodable α] [primcodable β] [primcodable σ] {f : α × β → σ} :
computable fcomputable₂ (λ (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 : α → γ} :
computable fcomputable gcomputable (λ (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 : α →. σ} :
partrec f(∀ (n : α), f n = g n)partrec g

theorem partrec.of_eq_tot {α : Type u_1} {σ : Type u_4} [primcodable α] [primcodable σ] {f : α →. σ} {g : α → σ} :
partrec f(∀ (n : α), g n f n)computable g

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 : α → β →. σ} :
partrec fpartrec₂ gpartrec (λ (a : α), (f a).bind (g a))

theorem partrec.map {α : Type u_1} {β : Type u_2} {σ : Type u_4} [primcodable α] [primcodable β] [primcodable σ] {f : α →. β} {g : α → β → σ} :
partrec fcomputable₂ gpartrec (λ (a : α), roption.map (g a) (f a))

theorem partrec.to₂ {α : Type u_1} {β : Type u_2} {σ : Type u_4} [primcodable α] [primcodable β] [primcodable σ] {f : α × β →. σ} :
partrec fpartrec₂ (λ (a : α) (b : β), f (a, b))

theorem partrec.nat_elim {α : Type u_1} {σ : Type u_4} [primcodable α] [primcodable σ] {f : α → } {g : α →. σ} {h : α → × σ →. σ} :
computable fpartrec gpartrec₂ hpartrec (λ (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 : α → β} :
partrec fcomputable gpartrec (λ (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 : α → γ} :
partrec₂ fcomputable gcomputable hpartrec (λ (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 : α → β → δ} :
partrec₂ fcomputable₂ gcomputable₂ hpartrec₂ (λ (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 : α → β} :
computable fcomputable gcomputable (λ (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 : α → β → γ} :
computable fcomputable₂ gcomputable₂ (λ (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 : α → γ} :
computable₂ fcomputable gcomputable hcomputable (λ (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 : α → β → δ} :
computable₂ fcomputable₂ gcomputable₂ hcomputable₂ (λ (a : α) (b : β), f (g a b) (h a b))

theorem partrec.rfind {α : Type u_1} [primcodable α] {p : α → →. bool} :
partrec₂ ppartrec (λ (a : α), nat.rfind (p a))

theorem partrec.rfind_opt {α : Type u_1} {σ : Type u_4} [primcodable α] [primcodable σ] {f : α → option σ} :
computable₂ fpartrec (λ (a : α), nat.rfind_opt (f a))

theorem partrec.nat_cases_right {α : Type u_1} {σ : Type u_4} [primcodable α] [primcodable σ] {f : α → } {g : α → σ} {h : α → →. σ} :
computable fcomputable gpartrec₂ hpartrec (λ (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 : α → × σ → σ} :
computable fcomputable gcomputable₂ hcomputable (λ (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 : α → → σ} :
computable fcomputable gcomputable₂ hcomputable (λ (a : α), nat.cases (g a) (h a) (f a))

theorem computable.cond {α : Type u_1} {σ : Type u_4} [primcodable α] [primcodable σ] {c : α → bool} {f g : α → σ} :
computable ccomputable fcomputable gcomputable (λ (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 : α → β → σ} :
computable ocomputable fcomputable₂ gcomputable (λ (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 σ} :
computable fcomputable₂ gcomputable (λ (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 : α → β → σ} :
computable fcomputable₂ gcomputable (λ (a : α), option.map (g 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 : α → γ → σ} :
computable fcomputable₂ gcomputable₂ hcomputable (λ (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 σ} :
computable₂ g(∀ (a : α) (n : ), g a (list.map (f a) (list.range n)) = some (f a n))computable₂ f

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α → σ} :
(∀ (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 : α → β →. σ} :
computable ocomputable fpartrec₂ gpartrec (λ (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 : α → γ →. σ} :
computable fcomputable₂ gpartrec₂ hpartrec (λ (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 : α → γ → σ} :
computable fpartrec₂ gcomputable₂ hpartrec (λ (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 : α →. σ α} :