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 #
- [Mario Carneiro, Formalizing computability theory via partial recursive functions][carneiro2019]
theorem
Nat.rfindOpt_spec
{α : Type u_1}
{f : ℕ → Option α}
{a : α}
(h : a ∈ Nat.rfindOpt f)
:
∃ n, a ∈ f n
- zero: Nat.Partrec (pure 0)
- succ: Nat.Partrec ↑Nat.succ
- left: Nat.Partrec ↑fun n => (Nat.unpair n).fst
- right: Nat.Partrec ↑fun n => (Nat.unpair n).snd
- pair: ∀ {f g : ℕ →. ℕ}, Nat.Partrec f → Nat.Partrec g → Nat.Partrec fun n => Seq.seq (Nat.pair <$> f n) fun x => g n
- comp: ∀ {f g : ℕ →. ℕ}, Nat.Partrec f → Nat.Partrec g → Nat.Partrec fun n => g n >>= f
- prec: ∀ {f g : ℕ →. ℕ}, Nat.Partrec f → Nat.Partrec g → Nat.Partrec (Nat.unpaired fun a n => Nat.rec (f a) (fun y IH => do let i ← IH g (Nat.pair a (Nat.pair y i))) n)
- rfind: ∀ {f : ℕ →. ℕ}, Nat.Partrec f → Nat.Partrec fun a => Nat.rfind fun n => (fun m => decide (m = 0)) <$> f (Nat.pair a n)
Instances For
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)
:
Nat.Partrec ↑g
theorem
Nat.Partrec.prec'
{f : ℕ →. ℕ}
{g : ℕ →. ℕ}
{h : ℕ →. ℕ}
(hf : Nat.Partrec f)
(hg : Nat.Partrec g)
(hh : Nat.Partrec h)
:
Nat.Partrec fun a =>
Part.bind (f a) fun n =>
Nat.rec (g a)
(fun y IH => do
let i ← IH
h (Nat.pair a (Nat.pair y i)))
n
Instances For
def
Partrec₂
{α : Type u_1}
{β : Type u_2}
{σ : Type u_3}
[Primcodable α]
[Primcodable β]
[Primcodable σ]
(f : α → β →. σ)
:
Instances For
Instances For
def
Computable₂
{α : Type u_1}
{β : Type u_2}
{σ : Type u_3}
[Primcodable α]
[Primcodable β]
[Primcodable σ]
(f : α → β → σ)
:
Instances For
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)
:
theorem
Computable.partrec
{α : Type u_1}
{σ : Type u_2}
[Primcodable α]
[Primcodable σ]
{f : α → σ}
(hf : Computable f)
:
Partrec ↑f
theorem
Computable₂.partrec₂
{α : Type u_1}
{β : Type u_2}
{σ : Type u_3}
[Primcodable α]
[Primcodable β]
[Primcodable σ]
{f : α → β → σ}
(hf : Computable₂ f)
:
Partrec₂ fun 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 fun x => s
theorem
Computable.ofOption
{α : Type u_1}
{β : Type u_2}
[Primcodable α]
[Primcodable β]
{f : α → Option β}
(hf : Computable f)
:
Partrec fun a => ↑(f a)
theorem
Computable.to₂
{α : Type u_1}
{β : Type u_2}
{σ : Type u_4}
[Primcodable α]
[Primcodable β]
[Primcodable σ]
{f : α × β → σ}
(hf : Computable f)
:
Computable₂ fun a b => f (a, b)
theorem
Computable.fst
{α : Type u_1}
{β : Type u_2}
[Primcodable α]
[Primcodable β]
:
Computable Prod.fst
theorem
Computable.snd
{α : Type u_1}
{β : Type u_2}
[Primcodable α]
[Primcodable β]
:
Computable Prod.snd
theorem
Computable.pair
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[Primcodable α]
[Primcodable β]
[Primcodable γ]
{f : α → β}
{g : α → γ}
(hf : Computable f)
(hg : Computable g)
:
Computable fun a => (f a, g a)
theorem
Computable.sum_inl
{α : Type u_1}
{β : Type u_2}
[Primcodable α]
[Primcodable β]
:
Computable Sum.inl
theorem
Computable.sum_inr
{α : Type u_1}
{β : Type u_2}
[Primcodable α]
[Primcodable β]
:
Computable Sum.inr
theorem
Computable.encode_iff
{α : Type u_1}
{σ : Type u_4}
[Primcodable α]
[Primcodable σ]
{f : α → σ}
:
(Computable fun 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
Partrec.none
{α : Type u_1}
{σ : Type u_4}
[Primcodable α]
[Primcodable σ]
:
Partrec fun x => Part.none
theorem
Decidable.Partrec.const'
{α : Type u_1}
{σ : Type u_4}
[Primcodable α]
[Primcodable σ]
(s : Part σ)
[Decidable s.Dom]
:
Partrec fun x => s
theorem
Partrec.const'
{α : Type u_1}
{σ : Type u_4}
[Primcodable α]
[Primcodable σ]
(s : Part σ)
:
Partrec fun x => s
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₂ fun a b => f (a, b)
theorem
Partrec.nat_rec
{α : 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 fun 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 : ℕ → ℕ →. α}
:
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 fun 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₂ fun 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 fun 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₂ fun 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 fun 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₂ fun a b => f (g a b) (h a b)
theorem
Partrec.rfindOpt
{α : Type u_1}
{σ : Type u_4}
[Primcodable α]
[Primcodable σ]
{f : α → ℕ → Option σ}
(hf : Computable₂ f)
:
Partrec fun a => Nat.rfindOpt (f a)
theorem
Partrec.nat_casesOn_right
{α : Type u_1}
{σ : Type u_4}
[Primcodable α]
[Primcodable σ]
{f : α → ℕ}
{g : α → σ}
{h : α → ℕ →. σ}
(hf : Computable f)
(hg : Computable g)
(hh : Partrec₂ h)
:
Partrec fun a => Nat.casesOn (f a) (Part.some (g a)) (h a)
theorem
Partrec.bind_decode₂_iff
{α : Type u_1}
{σ : Type u_4}
[Primcodable α]
[Primcodable σ]
{f : α →. σ}
:
Partrec f ↔ Nat.Partrec fun n => Part.bind ↑(Encodable.decode₂ α n) fun a => Part.map Encodable.encode (f a)
theorem
Partrec.vector_mOfFn
{α : Type u_1}
{σ : Type u_4}
[Primcodable α]
[Primcodable σ]
{n : ℕ}
{f : Fin n → α →. σ}
:
(∀ (i : Fin n), Partrec (f i)) → Partrec fun a => Vector.mOfFn fun i => f i a
@[simp]
theorem
Vector.mOfFn_part_some
{α : Type u_1}
{n : ℕ}
(f : Fin n → α)
:
(Vector.mOfFn fun i => Part.some (f i)) = Part.some (Vector.ofFn f)
theorem
Computable.option_some_iff
{α : Type u_1}
{σ : Type u_4}
[Primcodable α]
[Primcodable σ]
{f : α → σ}
:
(Computable fun 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₂ fun a n => Option.bind (Encodable.decode n) (f a)) ↔ Computable₂ f
theorem
Computable.map_decode_iff
{α : Type u_1}
{β : Type u_2}
{σ : Type u_4}
[Primcodable α]
[Primcodable β]
[Primcodable σ]
{f : α → β → σ}
:
(Computable₂ fun a n => Option.map (f a) (Encodable.decode n)) ↔ Computable₂ f
theorem
Computable.nat_rec
{α : Type u_1}
{σ : Type u_4}
[Primcodable α]
[Primcodable σ]
{f : α → ℕ}
{g : α → σ}
{h : α → ℕ × σ → σ}
(hf : Computable f)
(hg : Computable g)
(hh : Computable₂ h)
:
Computable fun a => Nat.rec (g a) (fun y IH => h a (y, IH)) (f a)
theorem
Computable.nat_casesOn
{α : Type u_1}
{σ : Type u_4}
[Primcodable α]
[Primcodable σ]
{f : α → ℕ}
{g : α → σ}
{h : α → ℕ → σ}
(hf : Computable f)
(hg : Computable g)
(hh : Computable₂ h)
:
Computable fun a => Nat.casesOn (f a) (g a) (h 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 fun a => bif c a then f a else g a
theorem
Computable.option_casesOn
{α : 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 fun a => Option.casesOn (o a) (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 fun a => Option.bind (f a) (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 fun a => Option.map (g a) (f a)
theorem
Computable.option_getD
{α : Type u_1}
{β : Type u_2}
[Primcodable α]
[Primcodable β]
{f : α → Option β}
{g : α → β}
(hf : Computable f)
(hg : Computable g)
:
Computable fun a => Option.getD (f a) (g a)
theorem
Computable.subtype_mk
{α : Type u_1}
{β : Type u_2}
[Primcodable α]
[Primcodable β]
{f : α → β}
{p : β → Prop}
[DecidablePred p]
{h : (a : α) → p (f a)}
(hp : PrimrecPred p)
(hf : Computable f)
:
Computable fun a => { val := f a, property := h a }
theorem
Computable.sum_casesOn
{α : 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 fun a => Sum.casesOn (f a) (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)) = some (f a n))
:
theorem
Computable.list_ofFn
{α : Type u_1}
{σ : Type u_4}
[Primcodable α]
[Primcodable σ]
{n : ℕ}
{f : Fin n → α → σ}
:
(∀ (i : Fin n), Computable (f i)) → Computable fun a => List.ofFn fun i => f i a
theorem
Computable.vector_ofFn
{α : Type u_1}
{σ : Type u_4}
[Primcodable α]
[Primcodable σ]
{n : ℕ}
{f : Fin n → α → σ}
(hf : ∀ (i : Fin n), Computable (f i))
:
Computable fun a => Vector.ofFn fun i => f i a
theorem
Partrec.option_some_iff
{α : Type u_1}
{σ : Type u_4}
[Primcodable α]
[Primcodable σ]
{f : α →. σ}
:
theorem
Partrec.option_casesOn_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 fun a => Option.casesOn (o a) (Part.some (f a)) (g a)
theorem
Partrec.sum_casesOn_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 fun a => Sum.casesOn (f a) (fun b => Part.some (g a b)) (h a)
theorem
Partrec.sum_casesOn_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 fun a => Sum.casesOn (f a) (g a) fun c => Part.some (h a c)
theorem
Partrec.fix
{α : Type u_1}
{σ : Type u_4}
[Primcodable α]
[Primcodable σ]
{f : α →. σ ⊕ α}
(hf : Partrec f)
: