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 #
Equations
- nat.rfind_x p H = (λ (this : Π (k : ℕ), (∀ (n : ℕ), n < k → bool.ff ∈ p n) → {n // bool.tt ∈ p n ∧ ∀ (m : ℕ), m < n → bool.ff ∈ p m}), this 0 _) (_.fix (λ (m : ℕ) (IH : Π (y : ℕ), lbp p y m → (∀ (n : ℕ), n < y → bool.ff ∈ p n) → {n // bool.tt ∈ p n ∧ ∀ (m : ℕ), m < n → bool.ff ∈ p m}) (al : ∀ (n : ℕ), n < m → bool.ff ∈ p n), (λ (_x : bool) (e : (p m).get _ = _x), _x.cases_on (λ (e : (p m).get _ = bool.ff), IH (m + 1) _ _) (λ (e : (p m).get _ = bool.tt), ⟨m, _⟩) e) ((p m).get _) _))
theorem
nat.rfind_opt_dom
{α : Type u_1}
{f : ℕ → option α} :
(nat.rfind_opt f).dom ↔ ∃ (n : ℕ) (a : α), a ∈ f n
- zero : nat.partrec (has_pure.pure 0)
- succ : nat.partrec ↑nat.succ
- left : nat.partrec ↑(λ (n : ℕ), (nat.unpair n).fst)
- right : nat.partrec ↑(λ (n : ℕ), (nat.unpair n).snd)
- pair : ∀ {f g : ℕ →. ℕ}, nat.partrec f → nat.partrec g → nat.partrec (λ (n : ℕ), nat.mkpair <$> f n <*> g n)
- comp : ∀ {f g : ℕ →. ℕ}, nat.partrec f → nat.partrec g → nat.partrec (λ (n : ℕ), g n >>= f)
- prec : ∀ {f g : ℕ →. ℕ}, nat.partrec f → nat.partrec g → nat.partrec (nat.unpaired (λ (a n : ℕ), nat.elim (f a) (λ (y : ℕ) (IH : part ℕ), IH >>= λ (i : ℕ), g (nat.mkpair a (nat.mkpair y i))) n))
- rfind : ∀ {f : ℕ →. ℕ}, nat.partrec f → nat.partrec (λ (a : ℕ), nat.rfind (λ (n : ℕ), (λ (m : ℕ), decidable.to_bool (m = 0)) <$> f (nat.mkpair a 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 : part ℕ), IH >>= λ (i : ℕ), h (nat.mkpair a (nat.mkpair y i))) n))
Equations
- partrec f = nat.partrec (λ (n : ℕ), ↑(encodable.decode α n).bind (λ (a : α), part.map encodable.encode (f a)))
def
partrec₂
{α : Type u_1}
{β : Type u_2}
{σ : Type u_3}
[primcodable α]
[primcodable β]
[primcodable σ]
(f : α → β →. σ) :
Prop
Equations
- computable f = partrec ↑f
def
computable₂
{α : Type u_1}
{β : Type u_2}
{σ : Type u_3}
[primcodable α]
[primcodable β]
[primcodable σ]
(f : α → β → σ) :
Prop
Equations
- computable₂ f = computable (λ (p : α × β), f p.fst p.snd)
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) :
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) :
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.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.list_concat
{α : Type u_1}
[primcodable α] :
computable₂ (λ (l : list α) (a : α), l ++ [a])
@[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) :
partrec g
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
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) :
theorem
partrec.map
{α : Type u_1}
{β : Type u_2}
{σ : Type u_4}
[primcodable α]
[primcodable β]
[primcodable σ]
{f : α →. β}
{g : α → β → σ}
(hf : partrec f)
(hg : computable₂ g) :
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) :
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 : α →. σ} :
partrec (λ (a : α), part.map encodable.encode (f a)) ↔ partrec f
theorem
partrec₂.unpaired
{α : Type u_1}
[primcodable α]
{f : ℕ → ℕ →. α} :
partrec (nat.unpaired f) ↔ partrec₂ 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_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) :
theorem
partrec.bind_decode₂_iff
{α : Type u_1}
{σ : Type u_4}
[primcodable α]
[primcodable σ]
{f : α →. σ} :
partrec f ↔ nat.partrec (λ (n : ℕ), ↑(encodable.decode₂ α n).bind (λ (a : α), part.map encodable.encode (f a)))
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 → α) :
vector.m_of_fn (λ (i : fin n), part.some (f i)) = part.some (vector.of_fn f)
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) :
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) :
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) :
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) :