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 : ), bool.tt p n (k : ), k < n (p k).dom) :
{n // bool.tt p n (m : ), m < n bool.ff p m}
Equations
def nat.rfind (p : →. bool) :
Equations
theorem nat.rfind_spec {p : →. bool} {n : } (h : n nat.rfind p) :
theorem nat.rfind_min {p : →. bool} {n : } (h : n nat.rfind p) {m : } :
m < n bool.ff p m
@[simp]
theorem nat.rfind_dom {p : →. bool} :
(nat.rfind p).dom (n : ), bool.tt p n {m : }, m < n (p m).dom
theorem nat.rfind_dom' {p : →. bool} :
(nat.rfind p).dom (n : ), bool.tt p n {m : }, m n (p m).dom
@[simp]
theorem nat.mem_rfind {p : →. bool} {n : } :
n nat.rfind p bool.tt p n {m : }, m < n bool.ff 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 n a f m a 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) :
@[protected]
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) :
@[protected]
theorem computable.partrec {α : Type u_1} {σ : Type u_2} [primcodable α] [primcodable σ] {f : α σ} (hf : computable f) :
@[protected]
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))
@[protected]
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_concat {α : Type u_1} [primcodable α] :
computable₂ (λ (l : list α) (a : α), l ++ [a])
theorem computable.fin_app {σ : Type u_4} [primcodable σ] {n : } :
@[protected]
@[protected]
@[protected]
theorem computable.encode_iff {α : Type u_1} {σ : Type u_4} [primcodable α] [primcodable σ] {f : α σ} :
computable (λ (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 (λ (a : α), part.none)
@[protected]
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)
@[protected]
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₂.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 : α), option.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)) = option.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 option.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) :