A simplified basis for partial recursive functions

This file defines Nat.Partrec', an inductive predicate that provides an alternative, structural basis for partial recursive functions using vectors. It establishes the equivalence between this vector-based definition and the standard Partrec definition.

inductive Nat.Partrec' {n : ℕ} : (List.Vector ℕ n →. ℕ) → Prop

A simplified basis for Partrec.

• prim {n : ℕ} {f : List.Vector ℕ n → ℕ} : Primrec' f → Partrec' ↑f
• comp {m n : ℕ} {f : List.Vector ℕ n →. ℕ} (g : Fin n → List.Vector ℕ m →. ℕ) : Partrec' f → (∀ (i : Fin n), Partrec' (g i)) → Partrec' fun (v : List.Vector ℕ m) => (List.Vector.mOfFn fun (i : Fin n) => g i v) >>= f
• rfind {n : ℕ} {f : List.Vector ℕ (n + 1) → ℕ} : Partrec' ↑f → Partrec' fun (v : List.Vector ℕ n) => Nat.rfind fun (n_1 : ℕ) => Part.some (decide (f (n_1 ::ᵥ v) = 0))

theorem Nat.Partrec'.to_part {n : ℕ} {f : List.Vector ℕ n →. ℕ} (pf : Partrec' f) : Partrec f

theorem Nat.Partrec'.of_eq {n : ℕ} {f g : List.Vector ℕ n →. ℕ} (hf : Partrec' f) (H : ∀ (i : List.Vector ℕ n), f i = g i) : Partrec' g

theorem Nat.Partrec'.of_prim {n : ℕ} {f : List.Vector ℕ n → ℕ} (hf : Primrec f) : Partrec' ↑f

theorem Nat.Partrec'.head {n : ℕ} : Partrec' ↑List.Vector.head

theorem Nat.Partrec'.tail {n : ℕ} {f : List.Vector ℕ n →. ℕ} (hf : Partrec' f) : Partrec' fun (v : List.Vector ℕ n.succ) => f v.tail

theorem Nat.Partrec'.bind {n : ℕ} {f : List.Vector ℕ n →. ℕ} {g : List.Vector ℕ (n + 1) →. ℕ} (hf : Partrec' f) (hg : Partrec' g) : Partrec' fun (v : List.Vector ℕ n) => (f v).bind fun (a : ℕ) => g (a ::ᵥ v)

theorem Nat.Partrec'.map {n : ℕ} {f : List.Vector ℕ n →. ℕ} {g : List.Vector ℕ (n + 1) → ℕ} (hf : Partrec' f) (hg : Partrec' ↑g) : Partrec' fun (v : List.Vector ℕ n) => Part.map (fun (a : ℕ) => g (a ::ᵥ v)) (f v)

def Nat.Partrec'.Vec {n m : ℕ} (f : List.Vector ℕ n → List.Vector ℕ m) : Prop

Analogous to Nat.Partrec' for ℕ-valued functions, a predicate for partial recursive vector-valued functions.

Equations

• Nat.Partrec'.Vec f = ∀ (i : Fin m), Nat.Partrec' fun (v : List.Vector ℕ n) => ↑(some ((f v).get i))

theorem Nat.Partrec'.Vec.prim {n m : ℕ} {f : List.Vector ℕ n → List.Vector ℕ m} (hf : Primrec'.Vec f) : Vec f

theorem Nat.Partrec'.nil {n : ℕ} : Vec fun (x : List.Vector ℕ n) => List.Vector.nil

theorem Nat.Partrec'.cons {n m : ℕ} {f : List.Vector ℕ n → ℕ} {g : List.Vector ℕ n → List.Vector ℕ m} (hf : Partrec' ↑f) (hg : Vec g) : Vec fun (v : List.Vector ℕ n) => f v ::ᵥ g v

theorem Nat.Partrec'.idv {n : ℕ} : Vec id

theorem Nat.Partrec'.comp' {n m : ℕ} {f : List.Vector ℕ m →. ℕ} {g : List.Vector ℕ n → List.Vector ℕ m} (hf : Partrec' f) (hg : Vec g) : Partrec' fun (v : List.Vector ℕ n) => f (g v)

theorem Nat.Partrec'.comp₁ {n : ℕ} (f : ℕ →. ℕ) {g : List.Vector ℕ n → ℕ} (hf : Partrec' fun (v : List.Vector ℕ 1) => f v.head) (hg : Partrec' ↑g) : Partrec' fun (v : List.Vector ℕ n) => f (g v)

theorem Nat.Partrec'.rfindOpt {n : ℕ} {f : List.Vector ℕ (n + 1) → ℕ} (hf : Partrec' ↑f) : Partrec' fun (v : List.Vector ℕ n) => Nat.rfindOpt fun (a : ℕ) => Denumerable.ofNat (Option ℕ) (f (a ::ᵥ v))

theorem Nat.Partrec'.of_part {n : ℕ} {f : List.Vector ℕ n →. ℕ} : Partrec f → Partrec' f

theorem Nat.Partrec'.part_iff {n : ℕ} {f : List.Vector ℕ n →. ℕ} : Partrec' f ↔ Partrec f

theorem Nat.Partrec'.part_iff₁ {f : ℕ →. ℕ} : (Partrec' fun (v : List.Vector ℕ 1) => f v.head) ↔ Partrec f

theorem Nat.Partrec'.part_iff₂ {f : ℕ → ℕ →. ℕ} : (Partrec' fun (v : List.Vector ℕ 2) => f v.head v.tail.head) ↔ Partrec₂ f

theorem Nat.Partrec'.vec_iff {m n : ℕ} {f : List.Vector ℕ m → List.Vector ℕ n} : Vec f ↔ Computable f