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
- [Mario Carneiro, Formalizing computability theory via partial recursive functions][carneiro2019]
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_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
- zero : nat.partrec (has_pure.pure 0)
- succ : nat.partrec ↑nat.succ
- left : nat.partrec ↑(λ (n : ℕ), n.unpair.fst)
- right : nat.partrec ↑(λ (n : ℕ), n.unpair.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 : roption ℕ), IH >>= λ (i : ℕ), g (a.mkpair (y.mkpair i))) n))
- rfind : ∀ {f : ℕ →. ℕ}, nat.partrec f → nat.partrec (λ (a : ℕ), nat.rfind (λ (n : ℕ), (λ (m : ℕ), decidable.to_bool (m = 0)) <$> f (a.mkpair n)))
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 f → nat.partrec g → 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))
Equations
- partrec f = nat.partrec (λ (n : ℕ), ↑(encodable.decode α n).bind (λ (a : α), roption.map encodable.encode (f a)))
def
partrec₂
{α : Type u_1}
{β : Type u_2}
{σ : Type u_3}
[primcodable α]
[primcodable β]
[primcodable σ] :
(α → β →. σ) → Prop
Equations
- computable f = partrec ↑f
def
computable₂
{α : Type u_1}
{β : Type u_2}
{σ : Type u_3}
[primcodable α]
[primcodable β]
[primcodable σ] :
(α → β → σ) → Prop
Equations
- computable₂ f = computable (λ (p : α × β), f p.fst p.snd)
theorem
primrec.to_comp
{α : Type u_1}
{σ : Type u_2}
[primcodable α]
[primcodable σ]
{f : α → σ} :
primrec f → computable f
theorem
primrec₂.to_comp
{α : Type u_1}
{β : Type u_2}
{σ : Type u_3}
[primcodable α]
[primcodable β]
[primcodable σ]
{f : α → β → σ} :
primrec₂ f → computable₂ f
theorem
computable.part
{α : Type u_1}
{σ : Type u_2}
[primcodable α]
[primcodable σ]
{f : α → σ} :
computable f → partrec ↑f
theorem
computable₂.part
{α : Type u_1}
{β : Type u_2}
{σ : Type u_3}
[primcodable α]
[primcodable β]
[primcodable σ]
{f : α → β → σ} :
computable₂ f → partrec₂ (λ (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 f → partrec (λ (a : α), ↑(f a))
theorem
computable.to₂
{α : Type u_1}
{β : Type u_2}
{σ : Type u_4}
[primcodable α]
[primcodable β]
[primcodable σ]
{f : α × β → σ} :
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 : α → γ} :
computable f → computable g → computable (λ (a : α), (f a, g a))
theorem
computable.list_concat
{α : Type u_1}
[primcodable α] :
computable₂ (λ (l : list α) (a : α), l ++ [a])
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 : α →. σ} :
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.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 : α → β →. σ} :
theorem
partrec.map
{α : Type u_1}
{β : Type u_2}
{σ : Type u_4}
[primcodable α]
[primcodable β]
[primcodable σ]
{f : α →. β}
{g : α → β → σ} :
partrec f → 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 : α × β →. σ} :
theorem
partrec.nat_elim
{α : Type u_1}
{σ : Type u_4}
[primcodable α]
[primcodable σ]
{f : α → ℕ}
{g : α →. σ}
{h : α → ℕ × σ →. σ} :
theorem
partrec.comp
{α : Type u_1}
{β : Type u_2}
{σ : Type u_4}
[primcodable α]
[primcodable β]
[primcodable σ]
{f : β →. σ}
{g : α → β} :
partrec f → computable g → partrec (λ (a : α), f (g a))
theorem
partrec.map_encode_iff
{α : Type u_1}
{σ : Type u_4}
[primcodable α]
[primcodable σ]
{f : α →. σ} :
partrec (λ (a : α), roption.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 : α → γ} :
partrec₂ f → computable g → 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 : α → β → δ} :
partrec₂ f → computable₂ g → 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 : α → β} :
computable f → 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 : α → β → γ} :
computable f → 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 : α → γ} :
computable₂ f → computable g → 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 : α → β → δ} :
computable₂ f → computable₂ g → 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 σ} :
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 : α → ℕ →. σ} :
computable f → computable g → 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 : α →. σ} :
partrec f ↔ nat.partrec (λ (n : ℕ), ↑(encodable.decode2 α n).bind (λ (a : α), roption.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_roption_some
{α : Type u_1}
{n : ℕ}
(f : fin n → α) :
vector.m_of_fn (λ (i : fin n), roption.some (f i)) = roption.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 : α → ℕ × σ → σ} :
computable f → computable g → 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 : α → ℕ → σ} :
computable f → computable g → 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 : α → σ} :
computable c → computable f → 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 : α → β → σ} :
computable o → computable f → 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 σ} :
computable f → 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 : α → β → σ} :
computable f → computable₂ g → computable (λ (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 f → computable₂ g → 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 σ} :
computable₂ g → (∀ (a : α) (n : ℕ), g a (list.map (f a) (list.range n)) = option.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 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 : α → β →. σ} :
computable o → computable f → 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 : α → γ →. σ} :
computable f → computable₂ g → 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 : α → γ → σ} :
computable f → partrec₂ g → 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 : α →. σ ⊕ α} :