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_dom
{α : Type u_1}
{f : ℕ → Option α}
:
(Nat.rfindOpt f).Dom ↔ ∃ (n : ℕ) (a : α), a ∈ f n
PartRec f
means that the partial function f : ℕ → ℕ
is partially recursive.
- zero: Nat.Partrec (pure 0)
- succ: Nat.Partrec ↑Nat.succ
- left: Nat.Partrec ↑fun (n : ℕ) => (Nat.unpair n).1
- right: Nat.Partrec ↑fun (n : ℕ) => (Nat.unpair n).2
- pair: ∀ {f g : ℕ →. ℕ}, Nat.Partrec f → Nat.Partrec g → Nat.Partrec fun (n : ℕ) => Seq.seq (Nat.pair <$> f n) fun (x : Unit) => 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 : Part ℕ) => 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)
:
Partially recursive partial functions α → σ
between Primcodable
types
Equations
- Partrec f = Nat.Partrec fun (n : ℕ) => (↑(Encodable.decode n)).bind fun (a : α) => Part.map Encodable.encode (f a)
Instances For
def
Partrec₂
{α : Type u_1}
{β : Type u_2}
{σ : Type u_3}
[Primcodable α]
[Primcodable β]
[Primcodable σ]
(f : α → β →. σ)
:
Partially recursive partial functions α → β → σ
between Primcodable
types
Instances For
Computable functions α → σ
between Primcodable
types:
a function is computable if and only if it is partially recursive (as a partial function)
Equations
- Computable f = Partrec ↑f
Instances For
def
Computable₂
{α : Type u_1}
{β : Type u_2}
{σ : Type u_3}
[Primcodable α]
[Primcodable β]
[Primcodable σ]
(f : α → β → σ)
:
Computable functions α → β → σ
between Primcodable
types
Equations
- Computable₂ f = Computable fun (p : α × β) => f p.1 p.2
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.list_append
{α : Type u_1}
[Primcodable α]
:
Computable₂ fun (x1 x2 : List α) => x1 ++ x2
theorem
Computable.list_concat
{α : Type u_1}
[Primcodable α]
:
Computable₂ fun (l : List α) (a : α) => l ++ [a]
theorem
Computable.vector_cons
{α : Type u_1}
[Primcodable α]
{n : ℕ}
:
Computable₂ Mathlib.Vector.cons
theorem
Computable.vector_toList
{α : Type u_1}
[Primcodable α]
{n : ℕ}
:
Computable Mathlib.Vector.toList
theorem
Computable.vector_length
{α : Type u_1}
[Primcodable α]
{n : ℕ}
:
Computable Mathlib.Vector.length
theorem
Computable.vector_head
{α : Type u_1}
[Primcodable α]
{n : ℕ}
:
Computable Mathlib.Vector.head
theorem
Computable.vector_tail
{α : Type u_1}
[Primcodable α]
{n : ℕ}
:
Computable Mathlib.Vector.tail
theorem
Computable.vector_get
{α : Type u_1}
[Primcodable α]
{n : ℕ}
:
Computable₂ Mathlib.Vector.get
theorem
Computable.vector_ofFn'
{α : Type u_1}
[Primcodable α]
{n : ℕ}
:
Computable Mathlib.Vector.ofFn
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_3}
[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_3}
[Primcodable α]
[Primcodable σ]
{f : α →. σ}
{g : α → σ}
(hf : Partrec f)
(H : ∀ (n : α), g n ∈ f n)
:
theorem
Partrec.none
{α : Type u_1}
{σ : Type u_3}
[Primcodable α]
[Primcodable σ]
:
Partrec fun (x : α) => Part.none
theorem
Decidable.Partrec.const'
{α : Type u_1}
{σ : Type u_3}
[Primcodable α]
[Primcodable σ]
(s : Part σ)
[Decidable s.Dom]
:
Partrec fun (x : α) => s
theorem
Partrec.const'
{α : Type u_1}
{σ : Type u_3}
[Primcodable α]
[Primcodable σ]
(s : Part σ)
:
Partrec fun (x : α) => s
theorem
Partrec.bind
{α : Type u_1}
{β : Type u_2}
{σ : Type u_3}
[Primcodable α]
[Primcodable β]
[Primcodable σ]
{f : α →. β}
{g : α → β →. σ}
(hf : Partrec f)
(hg : Partrec₂ g)
:
Partrec fun (a : α) => (f a).bind (g a)
theorem
Partrec.map
{α : Type u_1}
{β : Type u_2}
{σ : Type u_3}
[Primcodable α]
[Primcodable β]
[Primcodable σ]
{f : α →. β}
{g : α → β → σ}
(hf : Partrec f)
(hg : Computable₂ g)
:
theorem
Partrec.to₂
{α : Type u_1}
{β : Type u_2}
{σ : Type u_3}
[Primcodable α]
[Primcodable β]
[Primcodable σ]
{f : α × β →. σ}
(hf : Partrec f)
:
Partrec₂ fun (a : α) (b : β) => f (a, b)
theorem
Partrec.nat_rec
{α : Type u_1}
{σ : Type u_3}
[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_3}
[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_3}
[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₂.mk
{α : Type u_1}
{β : Type u_2}
{σ : Type u_5}
[Primcodable α]
[Primcodable β]
[Primcodable σ]
{f : α → β → σ}
(hf : Computable fun (p : α × β) => f p.1 p.2)
:
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_2}
[Primcodable α]
[Primcodable σ]
{f : α → ℕ → Option σ}
(hf : Computable₂ f)
:
Partrec fun (a : α) => Nat.rfindOpt (f a)
theorem
Partrec.nat_casesOn_right
{α : Type u_1}
{σ : Type u_2}
[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_2}
[Primcodable α]
[Primcodable σ]
{f : α →. σ}
:
Partrec f ↔ Nat.Partrec fun (n : ℕ) => (↑(Encodable.decode₂ α n)).bind fun (a : α) => Part.map Encodable.encode (f a)
theorem
Partrec.vector_mOfFn
{α : Type u_1}
{σ : Type u_2}
[Primcodable α]
[Primcodable σ]
{n : ℕ}
{f : Fin n → α →. σ}
:
(∀ (i : Fin n), Partrec (f i)) → Partrec fun (a : α) => Mathlib.Vector.mOfFn fun (i : Fin n) => f i a
@[simp]
theorem
Vector.mOfFn_part_some
{α : Type u_1}
{n : ℕ}
(f : Fin n → α)
:
(Mathlib.Vector.mOfFn fun (i : Fin n) => Part.some (f i)) = Part.some (Mathlib.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 : ℕ) => (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₂ 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 : (fun (x : ℕ) => σ) y) => 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 : α) => (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 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 : α) => (f a).getD (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 : α) => ⟨f 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 : Fin n) => 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 : α) => Mathlib.Vector.ofFn fun (i : Fin n) => 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_aux
{α : Type u_5}
{σ : Type u_6}
(f : α →. σ ⊕ α)
(a : α)
(b : σ)
:
let F := fun (a : α) (n : ℕ) =>
Nat.rec (Part.some (Sum.inr a))
(fun (x : ℕ) (IH : Part (σ ⊕ α)) => IH.bind fun (s : σ ⊕ α) => Sum.casesOn s (fun (x : σ) => Part.some s) f) n;
(∃ (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)
:
Partrec f.fix