The partial recursive functions #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 _) _))
- 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.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)))
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.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 → α →. σ} :
@[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) :